internlm/Lean-Github huggingface dataset:
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
case neg.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 : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, dist x c < r1 → dist (f x) (f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
fg : Set.EqOn (fun z => maxLog b (Complex.abs (f z))) g (ball c r)
gs : SubharmonicOn (fun z => maxLog b (Complex.abs (f z))) (ball c r)
⊢ c ∈ ball c r
Tactic:
exact Metric.mem_ball_self (by bound)
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
case pos
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp ≥ Complex.abs (f c)
⊢ ∃ r,
    0 < r ∧
      ∀ (s : ℝ),
        0 < s → s < r → maxLog b (Complex.abs (f c)) ≤ ⨍ (t : ℝ) in itau, maxLog b (Complex.abs (f (circleMap c s t)))
Tactic:
apply Minimum.submean (fa.continuousOn.maxLog_norm b) cs
Proof state after:
case pos
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp ≥ Complex.abs (f c)
⊢ ∀ (z : ℂ), maxLog b ‖f c‖ ≤ maxLog b ‖f z‖
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
case pos
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp ≥ Complex.abs (f c)
⊢ ∀ (z : ℂ), maxLog b ‖f c‖ ≤ maxLog b ‖f z‖
Tactic:
intro z
Proof state after:
case pos
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp ≥ Complex.abs (f c)
z : ℂ
⊢ maxLog b ‖f c‖ ≤ maxLog b ‖f z‖
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
case pos
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp ≥ Complex.abs (f c)
z : ℂ
⊢ maxLog b ‖f c‖ ≤ maxLog b ‖f z‖
Tactic:
simp only [maxLog_eq_b bf, le_maxLog, Complex.norm_eq_abs]
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
⊢ AnalyticAt ℂ h c
Tactic:
rw [← hh]
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
⊢ AnalyticAt ℂ (fun z => (↑(Complex.abs (f c)) / f c * f z).log) c
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
⊢ AnalyticAt ℂ (fun z => (↑(Complex.abs (f c)) / f c * f z).log) c
Tactic:
apply (analyticAt_const.mul (fa c (interior_subset cs))).log
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
⊢ ↑(Complex.abs (f c)) / f c * f c ∈ Complex.slitPlane
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
⊢ ↑(Complex.abs (f c)) / f c * f c ∈ Complex.slitPlane
Tactic:
field_simp [Complex.abs.ne_zero_iff.mp anz]
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, dist x c < r1 → dist (f x) (f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
⊢ Set.EqOn (fun z => maxLog b (Complex.abs (f z))) g (ball c r)
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 : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, dist x c < r1 → dist (f x) (f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
z : ℂ
zs : z ∈ ball c r
⊢ (fun z => maxLog b (Complex.abs (f z))) z = g z
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, dist x c < r1 → dist (f x) (f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
z : ℂ
zs : z ∈ ball c r
⊢ (fun z => maxLog b (Complex.abs (f z))) z = g z
Tactic:
simp only [Metric.mem_ball, Complex.dist_eq] at zs r1h
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, Complex.abs (x - c) < r1 → Complex.abs (f x - f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
z : ℂ
zs : Complex.abs (z - c) < r
⊢ (fun z => maxLog b (Complex.abs (f z))) z = g z
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, Complex.abs (x - c) < r1 → Complex.abs (f x - f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
z : ℂ
zs : Complex.abs (z - c) < r
⊢ (fun z => maxLog b (Complex.abs (f z))) z = g z
Tactic:
specialize r1h (lt_of_lt_of_le zs (by bound))
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 r1
z : ℂ
zs : Complex.abs (z - c) < r
r1h : Complex.abs (f z - f c) < Complex.abs (f c) - b.exp
⊢ (fun z => maxLog b (Complex.abs (f z))) z = g z
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 r1
z : ℂ
zs : Complex.abs (z - c) < r
r1h : Complex.abs (f z - f c) < Complex.abs (f c) - b.exp
⊢ (fun z => maxLog b (Complex.abs (f z))) z = g z
Tactic:
have zp : abs (f z) > b.exp := by
  calc abs (f z)
    _ = abs (f c + (f z - f c)) := by ring_nf
    _ ≥ abs (f c) - abs (f z - f c) := by bound
    _ > abs (f c) - (abs (f c) - b.exp) := by bound
    _ = b.exp := by abel
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 r1
z : ℂ
zs : Complex.abs (z - c) < r
r1h : Complex.abs (f z - f c) < Complex.abs (f c) - b.exp
zp : Complex.abs (f z) > b.exp
⊢ (fun z => maxLog b (Complex.abs (f z))) z = g z
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 r1
z : ℂ
zs : Complex.abs (z - c) < r
r1h : Complex.abs (f z - f c) < Complex.abs (f c) - b.exp
zp : Complex.abs (f z) > b.exp
⊢ (fun z => maxLog b (Complex.abs (f z))) z = g z
Tactic:
simp only [maxLog_eq_log zp.le]
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 r1
z : ℂ
zs : Complex.abs (z - c) < r
r1h : Complex.abs (f z - f c) < Complex.abs (f c) - b.exp
zp : Complex.abs (f z) > b.exp
⊢ (Complex.abs (f z)).log = g z
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 r1
z : ℂ
zs : Complex.abs (z - c) < r
r1h : Complex.abs (f z - f c) < Complex.abs (f c) - b.exp
zp : Complex.abs (f z) > b.exp
⊢ (Complex.abs (f z)).log = g z
Tactic:
rw [←hg, ←hh]
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 ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 r1
z : ℂ
zs : Complex.abs (z - c) < r
r1h : Complex.abs (f z - f c) < Complex.abs (f c) - b.exp
zp : Complex.abs (f z) > b.exp
⊢ (Complex.abs (f z)).log = (fun z => ((fun z => (↑(Complex.abs (f c)) / f c * f z).log) z).re) z