Theorem: AnalyticOn.maxLogAbsSubharmonicOn (Ray/Hartogs/Subharmonic.lean)

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 ∈ interior s,
    ∃ 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:
intro c cs
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
⊢ ∃ 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)))

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
⊢ ∃ 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:
by_cases bf : b.exp ≥ abs (f c)
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)
⊢ ∃ 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)))

case neg
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)))

State before:
case neg
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:
simp only [not_le] at bf
State after:
case neg
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)))

State before:
case neg
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:
have anz : ‖f c‖ ≠ 0 := (lt_trans (Real.exp_pos _) bf).ne'
State after:
case neg
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
⊢ ∃ 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)))

State before:
case neg
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
⊢ ∃ 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:
have fac : ContinuousAt f c :=
  fa.continuousOn.continuousAt (mem_interior_iff_mem_nhds.mp cs)
State after:
case neg
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
⊢ ∃ 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)))

State before:
case neg
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
⊢ ∃ 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:
generalize hh : (fun z ↦ Complex.log (Complex.abs (f c) / f c * f z)) = h
State after:
case neg
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
⊢ ∃ 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)))

State before:
case neg
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
⊢ ∃ 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:
generalize hg : (fun z ↦ (h z).re) = g
State after:
case neg
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
⊢ ∃ 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)))

State before:
case neg
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
⊢ ∃ 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:
have ha : AnalyticAt ℂ h c := by
  rw [← hh]
  apply (analyticAt_const.mul (fa c (interior_subset cs))).log
  field_simp [Complex.abs.ne_zero_iff.mp anz]
State after:
case neg
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
⊢ ∃ 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)))

State before:
case neg
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
⊢ ∃ 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:
rcases Metric.isOpen_iff.mp (isOpen_analyticAt ℂ h) c ha with ⟨r0, r0p, r0a⟩
State after:
case neg.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}
⊢ ∃ 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)))

State before:
case neg.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}
⊢ ∃ 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:
rcases Metric.continuousAt_iff.mp fac (abs (f c) - b.exp) (sub_pos.mpr bf) with
  ⟨r1, r1p, r1h⟩
State after:
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,
    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)))

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,
    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:
set r := min r0 r1
State after:
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
⊢ ∃ 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)))

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
⊢ ∃ 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:
have fg : Set.EqOn (fun z ↦ maxLog b (Complex.abs (f z))) g (ball c r) := by
  intro z zs
  simp only [Metric.mem_ball, Complex.dist_eq] at zs r1h
  specialize r1h (lt_of_lt_of_le zs (by bound))
  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
  simp only [maxLog_eq_log zp.le]
  rw [←hg, ←hh]
  simp only [Complex.norm_eq_abs] at anz
  simp only [Complex.log_re, AbsoluteValue.map_mul, map_div₀, Complex.abs_ofReal,
    Complex.abs_abs, div_self anz, one_mul]
State after:
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)
⊢ ∃ 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)))

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)
⊢ ∃ 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:
have gs : SubharmonicOn g (ball c r) := by
  rw [← hg]; apply AnalyticOn.reSubharmonicOn; intro z zs
  exact r0a (Metric.ball_subset_ball (by bound) zs)
State after:
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 g (ball c r)
⊢ ∃ 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)))

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 g (ball c r)
⊢ ∃ 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:
rw [subharmonicOn_congr fg.symm] at gs
State after:
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)
⊢ ∃ 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)))

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)
⊢ ∃ 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:
refine gs.submean' c ?_
State after:
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 ∈ interior (ball c r)

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 ∈ interior (ball c r)
Tactic:
rw [Metric.isOpen_ball.interior_eq]
State after:
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

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)
State after:
no goals

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
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‖

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
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‖

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]
State after:
no goals

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]
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

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
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

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]
State after:
no goals

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
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

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
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

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))
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

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
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

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]
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

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]
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

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 = (fun z => ((fun z => (↑(Complex.abs (f c)) / f c * f z).log) z).re) z
Tactic:
simp only [Complex.norm_eq_abs] at anz
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 : Complex.abs (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

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 : Complex.abs (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
Tactic:
simp only [Complex.log_re, AbsoluteValue.map_mul, map_div₀, Complex.abs_ofReal,
  Complex.abs_abs, div_self anz, one_mul]
State after:
no goals

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
⊢ r ≤ r1
Tactic:
bound
State after:
no goals

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
⊢ Complex.abs (f z) > b.exp
Tactic:
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
State after:
no goals

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
⊢ Complex.abs (f z) = Complex.abs (f c + (f z - f c))
Tactic:
ring_nf
State after:
no goals

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
⊢ Complex.abs (f c + (f z - f c)) ≥ Complex.abs (f c) - Complex.abs (f z - f c)
Tactic:
bound
State after:
no goals

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
⊢ Complex.abs (f c) - Complex.abs (f z - f c) > Complex.abs (f c) - (Complex.abs (f c) - b.exp)
Tactic:
bound
State after:
no goals

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
⊢ Complex.abs (f c) - (Complex.abs (f c) - b.exp) = b.exp
Tactic:
abel
State after:
no goals

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
fg : Set.EqOn (fun z => maxLog b (Complex.abs (f z))) g (ball c r)
⊢ SubharmonicOn g (ball c r)
Tactic:
rw [← hg]
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
fg : Set.EqOn (fun z => maxLog b (Complex.abs (f z))) g (ball c r)
⊢ SubharmonicOn (fun z => (h z).re) (ball c r)

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
fg : Set.EqOn (fun z => maxLog b (Complex.abs (f z))) g (ball c r)
⊢ SubharmonicOn (fun z => (h z).re) (ball c r)
Tactic:
apply AnalyticOn.reSubharmonicOn
State after:
case fa
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)
⊢ AnalyticOn ℂ (fun z => h z) (ball c r)

State before:
case fa
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)
⊢ AnalyticOn ℂ (fun z => h z) (ball c r)
Tactic:
intro z zs
State after:
case fa
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)
z : ℂ
zs : z ∈ ball c r
⊢ AnalyticAt ℂ (fun z => h z) z

State before:
case fa
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)
z : ℂ
zs : z ∈ ball c r
⊢ AnalyticAt ℂ (fun z => h z) z
Tactic:
exact r0a (Metric.ball_subset_ball (by bound) zs)
State after:
no goals

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
fg : Set.EqOn (fun z => maxLog b (Complex.abs (f z))) g (ball c r)
z : ℂ
zs : z ∈ ball c r
⊢ r ≤ r0
Tactic:
bound
State after:
no goals

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
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)
⊢ 0 < r
Tactic:
bound
State after:
no goals