internlm/Lean-Github huggingface dataset:
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 r1
z : ℂ
zs : Complex.abs (z - c) < r
r1h : Complex.abs (f z - f c) < Complex.abs (f c) - b.exp
zp : Complex.abs (f z) > b.exp
⊢ (Complex.abs (f z)).log = (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
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : 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
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : 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]
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, 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
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
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
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
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
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
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
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
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
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
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
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, dist x c < r1 → dist (f x) (f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
fg : Set.EqOn (fun z => maxLog b (Complex.abs (f z))) g (ball c r)
⊢ SubharmonicOn g (ball c r)
Tactic:
rw [← hg]
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, dist x c < r1 → dist (f x) (f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
fg : Set.EqOn (fun z => maxLog b (Complex.abs (f z))) g (ball c r)
⊢ SubharmonicOn (fun z => (h z).re) (ball c r)
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, dist x c < r1 → dist (f x) (f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
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
Proof 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)
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof 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
Proof 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
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof 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)
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, dist x c < r1 → dist (f x) (f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
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
Proof state after:
no goals
Theorem: AnalyticOn.maxLogAbsSubharmonicOn
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp < Complex.abs (f c)
anz : ‖f c‖ ≠ 0
fac : ContinuousAt f c
h : ℂ → ℂ
hh : (fun z => (↑(Complex.abs (f c)) / f c * f z).log) = h
g : ℂ → ℝ
hg : (fun z => (h z).re) = g
ha : AnalyticAt ℂ h c
r0 : ℝ
r0p : r0 > 0
r0a : ball c r0 ⊆ {x | AnalyticAt ℂ h x}
r1 : ℝ
r1p : r1 > 0
r1h : ∀ {x : ℂ}, dist x c < r1 → dist (f x) (f c) < Complex.abs (f c) - b.exp
r : ℝ := min r0 r1
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
Proof state after:
no goals
Theorem: SubharmonicOn.maximum_principle_ball
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ IsMaxOn f (closedBall c r) c → ∀ z ∈ closedBall c r, f c = f z
Tactic:
intro cm g gs
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
⊢ f c = f g
Theorem: SubharmonicOn.maximum_principle_ball
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
⊢ f c = f g
Tactic:
by_cases gc : g = c
Proof state after:
case pos
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : g = c
⊢ f c = f g

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
cm : IsMaxOn f (closedBall c r) c
g : ℂ
gs : g ∈ closedBall c r
gc : ¬g = c
⊢ f c = f g