internlm/Lean-Github huggingface dataset:
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof 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
Proof 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)))
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof 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]
Proof 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)))
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof 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⟩
Proof 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)))
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof 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⟩
Proof 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)))
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,
    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
Proof 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)))
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
⊢ ∃ 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]
Proof 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)))
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)
⊢ ∃ 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)
Proof 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)))
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 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
Proof 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)))
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)
⊢ ∃ 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 ?_
Proof 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)
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 ∈ interior (ball c r)
Tactic:
rw [Metric.isOpen_ball.interior_eq]
Proof 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