internlm/Lean-Github huggingface dataset:
Theorem: Minimum.submean
Proof state before:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
⊢ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Tactic:
intro t tp tr
Proof state after:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
Theorem: Minimum.submean
Proof state before:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
Tactic:
rw [average_eq]
Proof state after:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Theorem: Minimum.submean
Proof state before:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
have fg : ∀ (u) (_ : u ∈ itau), f c ≤ f (circleMap c t u) := fun _ _ ↦ fm _
Proof state after:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Theorem: Minimum.submean
Proof state before:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
have ss : closedBall c t ⊆ s :=
  _root_.trans (Metric.closedBall_subset_ball tr) (_root_.trans rs interior_subset)
Proof state after:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Theorem: Minimum.submean
Proof state before:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
have n := NiceVolume.itau
Proof state after:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Theorem: Minimum.submean
Proof state before:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
have m := setIntegral_ge_of_const_le n.measurable n.ne_top fg
  ((fc.mono ss).integrableOn_sphere tp)
Proof state after:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
m : f c * (↑volume itau).toReal ≤ ∫ (x : ℝ) in itau, f (circleMap c t x)
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Theorem: Minimum.submean
Proof state before:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
m : f c * (↑volume itau).toReal ≤ ∫ (x : ℝ) in itau, f (circleMap c t x)
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
simp only [MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, smul_eq_mul, ge_iff_le]
Proof state after:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
m : f c * (↑volume itau).toReal ≤ ∫ (x : ℝ) in itau, f (circleMap c t x)
⊢ f c ≤ (↑volume itau).toReal⁻¹ * ∫ (x : ℝ) in itau, f (circleMap c t x)
Theorem: Minimum.submean
Proof state before:
case right
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 ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
m : f c * (↑volume itau).toReal ≤ ∫ (x : ℝ) in itau, f (circleMap c t x)
⊢ f c ≤ (↑volume itau).toReal⁻¹ * ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
simpa only [mul_comm, ← div_eq_mul_inv, le_div_iff n.real_pos]
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 ∈ 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
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
⊢ ∃ 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:
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)
Proof state after:
case pos
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℂ
s : Set ℂ
fa : AnalyticOn ℂ f s
b : ℝ
c : ℂ
cs : c ∈ interior s
bf : b.exp ≥ Complex.abs (f c)
⊢ ∃ 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)))
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)
⊢ ∃ 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
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)
⊢ ∃ 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)
⊢ ∃ 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'
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
⊢ ∃ 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
⊢ ∃ 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)
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
⊢ ∃ 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
⊢ ∃ 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
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
⊢ ∃ 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)))