internlm/Lean-Github huggingface dataset:
Theorem: continuous_to_harmonic_real
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
fc' : ContinuousOn f' (sphere c r)
g : ℂ → ℂ
gh : HarmonicOn g (closedBall c r)
b : ∀ z ∈ sphere c r, f' z = g z
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
use fun z ↦ (g z).re, gh.re
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
fc' : ContinuousOn f' (sphere c r)
g : ℂ → ℂ
gh : HarmonicOn g (closedBall c r)
b : ∀ z ∈ sphere c r, f' z = g z
⊢ ∀ z ∈ sphere c r, f z = (g z).re
Theorem: continuous_to_harmonic_real
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
fc' : ContinuousOn f' (sphere c r)
g : ℂ → ℂ
gh : HarmonicOn g (closedBall c r)
b : ∀ z ∈ sphere c r, f' z = g z
⊢ ∀ z ∈ sphere c r, f z = (g z).re
Tactic:
intro z zs
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
fc' : ContinuousOn f' (sphere c r)
g : ℂ → ℂ
gh : HarmonicOn g (closedBall c r)
b : ∀ z ∈ sphere c r, f' z = g z
z : ℂ
zs : z ∈ sphere c r
⊢ f z = (g z).re
Theorem: continuous_to_harmonic_real
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
fc' : ContinuousOn f' (sphere c r)
g : ℂ → ℂ
gh : HarmonicOn g (closedBall c r)
b : ∀ z ∈ sphere c r, f' z = g z
z : ℂ
zs : z ∈ sphere c r
⊢ f z = (g z).re
Tactic:
simp only [← b z zs, Complex.ofReal_re, ← hf']
Proof state after:
no goals
Theorem: continuous_to_harmonic_real
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 : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
⊢ ContinuousOn f' (sphere c r)
Tactic:
rw [← hf']
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 : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
⊢ ContinuousOn (fun z => ↑(f z)) (sphere c r)
Theorem: continuous_to_harmonic_real
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 : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
⊢ ContinuousOn (fun z => ↑(f z)) (sphere c r)
Tactic:
exact Complex.continuous_ofReal.comp_continuousOn fc
Proof state after:
no goals
Theorem: SubharmonicOn.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
rcases continuous_to_harmonic_real (fs.cont.mono Metric.sphere_subset_closedBall) with ⟨g, gh, fg⟩
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 : ℂ → ℝ
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
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: SubharmonicOn.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 : ℂ → ℝ
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
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
generalize hd : (fun z ↦ f z - g z) = d
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 : ℂ → ℝ
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
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: SubharmonicOn.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 : ℂ → ℝ
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
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have ds : SubharmonicOn d (closedBall c r) := by rw [← hd]; apply fs.add gh.neg.subharmonicOn
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 : ℂ → ℝ
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)
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: SubharmonicOn.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 : ℂ → ℝ
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)
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have dz : ∀ z, z ∈ sphere c r → d z = 0 := by intro z zs; rw [← hd]; simp only [fg z zs, sub_self]
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 : ℂ → ℝ
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
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: SubharmonicOn.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 : ℂ → ℝ
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
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have dz' : ∀ᵐ t, t ∈ itau → d (circleMap c r t) = 0 := by
  apply ae_of_all; intro t _; apply dz
  simp only [mem_sphere_iff_norm, circleMap_sub_center, Complex.norm_eq_abs, abs_circleMap_zero,
    abs_eq_self]
  linarith
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 : ℂ → ℝ
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
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: SubharmonicOn.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 : ℂ → ℝ
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
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
rcases ds.maximum_principle (isCompact_closedBall _ _) ⟨c, Metric.mem_closedBall_self rp.le⟩
  with ⟨w, wf, wm⟩
Proof state after:
case intro.intro.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 : ℂ → ℝ
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 ∈ frontier (closedBall c r)
wm : IsMaxOn d (closedBall c r) w
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: SubharmonicOn.submean
Proof state before:
case intro.intro.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 : ℂ → ℝ
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 ∈ frontier (closedBall c r)
wm : IsMaxOn d (closedBall c r) w
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
rw [frontier_closedBall _ rp.ne'] at wf
Proof state after:
case intro.intro.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 : ℂ → ℝ
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
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: SubharmonicOn.submean
Proof state before:
case intro.intro.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 : ℂ → ℝ
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
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have fd : f = fun z ↦ d z + g z := by funext z; rw [← hd]; simp only [sub_add_cancel]
Proof state after:
case intro.intro.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 : ℂ → ℝ
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
fd : f = fun z => d z + g z
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: SubharmonicOn.submean
Proof state before:
case intro.intro.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 : ℂ → ℝ
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
fd : f = fun z => d z + g z
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
simp_rw [fd, Average.add (ds.cont.integrableOn_sphere rp) (gh.cont.integrableOn_sphere rp)]
Proof state after:
case intro.intro.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 : ℂ → ℝ
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
fd : f = fun z => d z + g z
⊢ d c + g c ≤ (⨍ (z : ℝ) in itau, d (circleMap c r z)) + ⨍ (z : ℝ) in itau, g (circleMap c r z)