internlm/Lean-Github huggingface dataset:
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
⊢ d c + g c ≤ (⨍ (z : ℝ) in itau, d (circleMap c r z)) + ⨍ (z : ℝ) in itau, g (circleMap c r z)
Tactic:
simp only [← gh.mean c r rp (subset_refl _), add_le_add_iff_right]
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 ≤ ⨍ (z : ℝ) in itau, d (circleMap c r z)
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
⊢ d c ≤ ⨍ (z : ℝ) in itau, d (circleMap c r z)
Tactic:
simp only [average_congr_on NiceVolume.itau dz', average_zero]
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 ≤ 0
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
⊢ d c ≤ 0
Tactic:
rw [← dz w 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
fd : f = fun z => d z + g z
⊢ d c ≤ d w
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
⊢ d c ≤ d w
Tactic:
apply wm (Metric.mem_closedBall_self rp.le)
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
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
⊢ SubharmonicOn d (closedBall c r)
Tactic:
rw [← hd]
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
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
⊢ SubharmonicOn (fun z => f z - g z) (closedBall c r)
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
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
⊢ SubharmonicOn (fun z => f z - g z) (closedBall c r)
Tactic:
apply fs.add gh.neg.subharmonicOn
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
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)
⊢ ∀ z ∈ sphere c r, d z = 0
Tactic:
intro z zs
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
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)
z : ℂ
zs : z ∈ sphere c r
⊢ d z = 0
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
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)
z : ℂ
zs : z ∈ sphere c r
⊢ d z = 0
Tactic:
rw [← hd]
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
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)
z : ℂ
zs : z ∈ sphere c r
⊢ (fun z => f z - g z) z = 0
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
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)
z : ℂ
zs : z ∈ sphere c r
⊢ (fun z => f z - g z) z = 0
Tactic:
simp only [fg z zs, sub_self]
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
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
⊢ ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
Tactic:
apply ae_of_all
Proof state after:
case a
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
⊢ ∀ a ∈ itau, d (circleMap c r a) = 0
Theorem: SubharmonicOn.submean
Proof state before:
case a
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
⊢ ∀ a ∈ itau, d (circleMap c r a) = 0
Tactic:
intro t _
Proof state after:
case a
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
t : ℝ
a✝ : t ∈ itau
⊢ d (circleMap c r t) = 0
Theorem: SubharmonicOn.submean
Proof state before:
case a
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
t : ℝ
a✝ : t ∈ itau
⊢ d (circleMap c r t) = 0
Tactic:
apply dz
Proof state after:
case a.a
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
t : ℝ
a✝ : t ∈ itau
⊢ circleMap c r t ∈ sphere c r
Theorem: SubharmonicOn.submean
Proof state before:
case a.a
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
t : ℝ
a✝ : t ∈ itau
⊢ circleMap c r t ∈ sphere c r
Tactic:
simp only [mem_sphere_iff_norm, circleMap_sub_center, Complex.norm_eq_abs, abs_circleMap_zero,
  abs_eq_self]
Proof state after:
case a.a
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
t : ℝ
a✝ : t ∈ itau
⊢ 0 ≤ r
Theorem: SubharmonicOn.submean
Proof state before:
case a.a
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
t : ℝ
a✝ : t ∈ itau
⊢ 0 ≤ r
Tactic:
linarith
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
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 = fun z => d z + g z
Tactic:
funext z
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 = d z + g z