internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.submean
Proof state before:
case h
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
z : ℂ
⊢ f z = d z + g z
Tactic:
rw [← hd]
Proof state after:
case h
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
z : ℂ
⊢ f z = (fun z => f z - g z) z + g z
Theorem: SubharmonicOn.submean
Proof state before:
case h
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
z : ℂ
⊢ f z = (fun z => f z - g z) z + g z
Tactic:
simp only [sub_add_cancel]
Proof state after:
no goals
Theorem: subharmonicOn_iff_submean
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
⊢ SubharmonicOn f s ↔ ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
constructor
Proof state after:
case mp
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
⊢ SubharmonicOn f s → ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)

case mpr
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
⊢ (∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)) → SubharmonicOn f s
Theorem: subharmonicOn_iff_submean
Proof state before:
case mp
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
⊢ SubharmonicOn f s → ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
intro fs c r rp cs
Proof state after:
case mp
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
fs : SubharmonicOn f s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: subharmonicOn_iff_submean
Proof state before:
case mp
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
fs : SubharmonicOn f s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
exact (fs.mono cs).submean rp
Proof state after:
no goals
Theorem: subharmonicOn_iff_submean
Proof state before:
case mpr
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
⊢ (∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)) → SubharmonicOn f s
Tactic:
intro sm
Proof state after:
case mpr
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
⊢ SubharmonicOn f s
Theorem: subharmonicOn_iff_submean
Proof state before:
case mpr
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
⊢ SubharmonicOn f s
Tactic:
exact
  { cont := fc
    submean' := by
      intro c ci
      rcases Metric.isOpen_iff.mp isOpen_interior c ci with ⟨r, rp, rs⟩
      use r, rp; intro t tp tr; apply sm c t tp
      exact _root_.trans (Metric.closedBall_subset_ball tr) (_root_.trans rs interior_subset) }
Proof state after:
no goals
Theorem: subharmonicOn_iff_submean
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
⊢ ∀ c ∈ interior s, ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Tactic:
intro c ci
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
c : ℂ
ci : c ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Theorem: subharmonicOn_iff_submean
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
c : ℂ
ci : c ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Tactic:
rcases Metric.isOpen_iff.mp isOpen_interior c ci with ⟨r, rp, rs⟩
Proof state after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
c : ℂ
ci : c ∈ interior s
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Theorem: subharmonicOn_iff_submean
Proof state before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
c : ℂ
ci : c ∈ interior s
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Tactic:
use r, rp
Proof state after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
c : ℂ
ci : c ∈ interior s
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
⊢ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Theorem: subharmonicOn_iff_submean
Proof state before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
c : ℂ
ci : c ∈ interior s
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
⊢ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Tactic:
intro t tp tr
Proof state after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
c : ℂ
ci : c ∈ interior s
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
Theorem: subharmonicOn_iff_submean
Proof state before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
c : ℂ
ci : c ∈ interior s
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
Tactic:
apply sm c t tp
Proof state after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
c : ℂ
ci : c ∈ interior s
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall c t ⊆ s
Theorem: subharmonicOn_iff_submean
Proof state before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
fc : ContinuousOn f s
sm : ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
c : ℂ
ci : c ∈ interior s
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall c t ⊆ s
Tactic:
exact _root_.trans (Metric.closedBall_subset_ball tr) (_root_.trans rs interior_subset)
Proof state after:
no goals
Theorem: SubharmonicOn.submean_disk
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ ⨍ (z : ℂ) in closedBall c r, f z
Tactic:
simp only [average_eq, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, smul_eq_mul]
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ (↑volume (closedBall c r)).toReal⁻¹ * ∫ (z : ℂ) in closedBall c r, f z
Theorem: SubharmonicOn.submean_disk
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ (↑volume (closedBall c r)).toReal⁻¹ * ∫ (z : ℂ) in closedBall c r, f z
Tactic:
rw [Complex.volume_closedBall' rp.le, fubini_ball fs.cont]
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ (π * r ^ 2)⁻¹ * ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Theorem: SubharmonicOn.submean_disk
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ (π * r ^ 2)⁻¹ * ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
have m : (fun s ↦ (2 * π * s) • f c) ≤ᵐ[volume.restrict (Ioc 0 r)] fun s ↦
    s • ∫ t : ℝ in Set.Ioc 0 (2 * π), f (circleMap c s t) := by
  rw [Filter.EventuallyLE]; rw [ae_restrict_iff' measurableSet_Ioc]; apply ae_of_all; intro s sr
  simp only [Set.mem_Ioc] at sr
  have e := (fs.mono (Metric.closedBall_subset_closedBall sr.2)).submean sr.1
  rw [smul_eq_mul, ← itau]
  simp only [average_eq, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
    itau_real_volume, smul_eq_mul] at e
  generalize hi : ∫ t in itau, f (circleMap c s t) = i
  rw [hi] at e
  calc 2 * π * s * f c
    _ ≤ 2 * π * s * ((2 * π)⁻¹ * i) := by bound
    _ = s * (2 * π * (2 * π)⁻¹) * i := by ring_nf
    _ ≤ s * i := by field_simp [Real.two_pi_pos.ne']
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ f c ≤ (π * r ^ 2)⁻¹ * ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)