internlm/Lean-Github huggingface dataset:
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ r1 ^ n * t ≤ r1 ^ n * (c * s⁻¹ ^ n)
Tactic:
bound
Proof state after:
no goals
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ r1 ^ n * (c * s⁻¹ ^ n) = r1 ^ n * (c * (e.exp ^ n / r1 ^ n))
Tactic:
rw [inv_div, div_pow]
Proof state after:
no goals
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ r1 ^ n * (c * (e.exp ^ n / r1 ^ n)) = r1 ^ n / r1 ^ n * c * e.exp ^ n
Tactic:
ring
Proof state after:
no goals
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ r1 ^ n / r1 ^ n * c * e.exp ^ n = c * e.exp ^ n
Tactic:
field_simp [(pow_pos u.r1p _).ne']
Proof state after:
no goals
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ c * e.exp ^ n = c * (↑n * e).exp
Tactic:
rw [Real.exp_nat_mul]
Proof state after:
no goals
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ c * (↑n * e).exp = c * (↑n * d - ↑n * (d - e)).exp
Tactic:
ring_nf
Proof state after:
no goals
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ c * (↑n * d - ↑n * (d - e)).exp = c.log.exp * ((↑n * d).exp / (↑n * (d - e)).exp)
Tactic:
rw [Real.exp_sub, Real.exp_log cp]
Proof state after:
no goals
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ c.log.exp * ((↑n * d).exp / (↑n * (d - e)).exp) = c.log.exp / (↑n * (d - e)).exp * (↑n * d).exp
Tactic:
ring_nf
Proof state after:
no goals
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ c.log.exp / (↑n * (d - e)).exp * (↑n * d).exp = (c.log - ↑n * (d - e)).exp * (↑n * d).exp
Tactic:
rw [Real.exp_sub]
Proof state after:
no goals
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ (c.log - ↑n * (d - e)).exp * (↑n * d).exp ≤ (c.log - c.log / (d - e) * (d - e)).exp * (↑n * d).exp
Tactic:
bound
Proof state after:
no goals
Theorem: unevenLog_nonuniform_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
sr : s < r1
c : ℝ
cp : c > 0
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
t : ℝ
us : t ≤ c * s⁻¹ ^ n
ht : ‖unevenTerm u z1 n‖ = t
nb : c.log / (d - e) ≤ ↑n
⊢ (c.log - c.log / (d - e) * (d - e)).exp * (↑n * d).exp ≤ (↑n * d).exp
Tactic:
field_simp [(sub_pos.mpr ed).ne']
Proof state after:
no goals
Theorem: uneven_nonuniform_subharmonic
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ SubharmonicOn (unevenLog u n) (ball c1 r1)
Tactic:
refine SubharmonicOn.constMul ?_ (by bound)
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ SubharmonicOn (fun z => maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖) (ball c1 r1)
Theorem: uneven_nonuniform_subharmonic
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ SubharmonicOn (fun z => maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖) (ball c1 r1)
Tactic:
apply AnalyticOn.maxLog_norm_subharmonicOn _ (-1)
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ AnalyticOn ℂ (fun z => r1 ^ n • unevenTerm u z n) (ball c1 r1)
Theorem: uneven_nonuniform_subharmonic
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ AnalyticOn ℂ (fun z => r1 ^ n • unevenTerm u z n) (ball c1 r1)
Tactic:
rw [analyticOn_iff_differentiableOn Metric.isOpen_ball]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ DifferentiableOn ℂ (fun z => r1 ^ n • unevenTerm u z n) (ball c1 r1)
Theorem: uneven_nonuniform_subharmonic
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ DifferentiableOn ℂ (fun z => r1 ^ n • unevenTerm u z n) (ball c1 r1)
Tactic:
apply DifferentiableOn.const_smul
Proof state after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ DifferentiableOn ℂ (fun y => unevenTerm u y n) (ball c1 r1)
Theorem: uneven_nonuniform_subharmonic
Proof state before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ DifferentiableOn ℂ (fun y => unevenTerm u y n) (ball c1 r1)
Tactic:
rw [← analyticOn_iff_differentiableOn Metric.isOpen_ball]
Proof state after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ AnalyticOn ℂ (fun y => unevenTerm u y n) (ball c1 r1)
Theorem: uneven_nonuniform_subharmonic
Proof state before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ AnalyticOn ℂ (fun y => unevenTerm u y n) (ball c1 r1)
Tactic:
apply unevenTerm.analytic u
Proof state after:
no goals
Theorem: uneven_nonuniform_subharmonic
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ 0 ≤ (↑n)⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_strong_bound
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
rcases exists_between sr with ⟨t, ts, tr⟩
Proof state after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
have tp : t > 0 := _root_.trans ts sp
Proof state after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
have trs : closedBall c1 t ⊆ ball c1 r1 := Metric.closedBall_subset_ball tr
Proof state after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
have cs : closedBall c1 t ⊆ closedBall c1 r1 :=
  Metric.closedBall_subset_closedBall tr.le
Proof state after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
have ks : closedBall c1 s ⊆ interior (closedBall c1 t) := by
  rw [interior_closedBall _ tp.ne']; exact Metric.closedBall_subset_ball ts
Proof state after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
rcases unevenLog_uniform_bound u tr with ⟨b, fb⟩
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
have H := SubharmonicOn.hartogs (fun n ↦ (uneven_nonuniform_subharmonic u n).mono trs) fb
    (fun z zs ↦ unevenLog_nonuniform_bound u (cs zs)) (isCompact_closedBall _ _) ks
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ d > 0, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ d
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ d > 0, ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ d
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
specialize H (r1 / s).log (by bound)
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ s⁻¹ ^ n
Tactic:
refine H.mp ((Filter.eventually_gt_atTop 0).mp (Filter.eventually_of_forall ?_))
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
⊢ ∀ (x : ℕ),
    0 < x →
      (∀ z ∈ closedBall c1 s, unevenLog u x z ≤ (r1 / s).log) → ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 x‖ ≤ s⁻¹ ^ x
Theorem: unevenSeries_strong_bound
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
⊢ ∀ (x : ℕ),
    0 < x →
      (∀ z ∈ closedBall c1 s, unevenLog u x z ≤ (r1 / s).log) → ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 x‖ ≤ s⁻¹ ^ x
Tactic:
intro n np h z zs
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : 0 < s
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
trs : closedBall c1 t ⊆ ball c1 r1
cs : closedBall c1 t ⊆ closedBall c1 r1
ks : closedBall c1 s ⊆ interior (closedBall c1 t)
b : ℝ
fb : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, unevenLog u n z1 ≤ b
H : ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
n : ℕ
np : 0 < n
h : ∀ z ∈ closedBall c1 s, unevenLog u n z ≤ (r1 / s).log
z : ℂ
zs : z ∈ closedBall c1 s
⊢ ‖unevenSeries u z n‖ ≤ s⁻¹ ^ n