internlm/Lean-Github huggingface dataset:
Theorem: unevenLog_nonuniform_bound
Proof state before:
case intro.intro.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
z1s : z1 ∈ closedBall c1 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
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
have mp : 0 < (m : ℝ) := lt_of_lt_of_le zero_lt_one (le_trans (by bound) mb.le)
Proof state after:
case intro.intro.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
z1s : z1 ∈ closedBall c1 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
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
Proof state before:
case intro.intro.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
z1s : z1 ∈ closedBall c1 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
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
rw [Filter.eventually_atTop]
Proof state after:
case intro.intro.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
z1s : z1 ∈ closedBall c1 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
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
⊢ ∃ a, ∀ b ≥ a, unevenLog u b z1 ≤ d
Theorem: unevenLog_nonuniform_bound
Proof state before:
case intro.intro.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
z1s : z1 ∈ closedBall c1 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
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
⊢ ∃ a, ∀ b ≥ a, unevenLog u b z1 ≤ d
Tactic:
use m
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
z1s : z1 ∈ closedBall c1 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
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
⊢ ∀ b ≥ m, unevenLog u b z1 ≤ d
Theorem: unevenLog_nonuniform_bound
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
z1s : z1 ∈ closedBall c1 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
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
⊢ ∀ b ≥ m, unevenLog u b z1 ≤ d
Tactic:
intro n mn
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
z1s : z1 ∈ closedBall c1 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
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
⊢ unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
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
z1s : z1 ∈ closedBall c1 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
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
mp : 0 < ↑m
n : ℕ
mn : n ≥ m
⊢ unevenLog u n z1 ≤ d
Tactic:
specialize us n
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
z1s : z1 ∈ closedBall c1 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
us : ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
⊢ unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
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
z1s : z1 ∈ closedBall c1 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
us : ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
⊢ unevenLog u n z1 ≤ d
Tactic:
generalize ht : ‖unevenTerm u z1 n‖ = t
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
z1s : z1 ∈ closedBall c1 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
us : ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
t : ℝ
ht : ‖unevenTerm u z1 n‖ = t
⊢ unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
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
z1s : z1 ∈ closedBall c1 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
us : ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
t : ℝ
ht : ‖unevenTerm u z1 n‖ = t
⊢ unevenLog u n z1 ≤ d
Tactic:
rw [unevenSeries_norm, ht] at us
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
z1s : z1 ∈ closedBall c1 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
⊢ unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
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
z1s : z1 ∈ closedBall c1 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
⊢ unevenLog u n z1 ≤ d
Tactic:
clear z1s
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
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
⊢ unevenLog u n z1 ≤ d
Theorem: unevenLog_nonuniform_bound
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
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
⊢ unevenLog u n z1 ≤ d
Tactic:
rw [unevenLog, inv_mul_le_iff (lt_of_lt_of_le mp (Nat.cast_le.mpr mn))]
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
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
⊢ maxLog (-1) ‖r1 ^ n • unevenTerm u z1 n‖ ≤ ↑n * d
Theorem: unevenLog_nonuniform_bound
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
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
⊢ maxLog (-1) ‖r1 ^ n • unevenTerm u z1 n‖ ≤ ↑n * d
Tactic:
apply maxLog_le
Proof state after:
case h.yb
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
⊢ -1 ≤ ↑n * d

case h.xy
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
⊢ ‖r1 ^ n • unevenTerm u z1 n‖ ≤ (↑n * d).exp
Theorem: unevenLog_nonuniform_bound
Proof state before:
case h.yb
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
⊢ -1 ≤ ↑n * d

case h.xy
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
⊢ ‖r1 ^ n • unevenTerm u z1 n‖ ≤ (↑n * d).exp
Tactic:
trans (0 : ℝ)
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
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
⊢ -1 ≤ 0

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
⊢ 0 ≤ ↑n * d

case h.xy
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
⊢ ‖r1 ^ n • unevenTerm u z1 n‖ ≤ (↑n * d).exp
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
⊢ -1 ≤ 0

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
⊢ 0 ≤ ↑n * d

case h.xy
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
⊢ ‖r1 ^ n • unevenTerm u z1 n‖ ≤ (↑n * d).exp
Tactic:
norm_num
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
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
⊢ 0 ≤ ↑n * d

case h.xy
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
⊢ ‖r1 ^ n • unevenTerm u z1 n‖ ≤ (↑n * d).exp
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
⊢ 0 ≤ ↑n * d

case h.xy
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
⊢ ‖r1 ^ n • unevenTerm u z1 n‖ ≤ (↑n * d).exp
Tactic:
bound
Proof state after:
case h.xy
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
⊢ ‖r1 ^ n • unevenTerm u z1 n‖ ≤ (↑n * d).exp
Theorem: unevenLog_nonuniform_bound
Proof state before:
case h.xy
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
⊢ ‖r1 ^ n • unevenTerm u z1 n‖ ≤ (↑n * d).exp
Tactic:
have nb : c.log / (d - e) ≤ n := le_trans (le_trans (by bound) mb.le) (Nat.cast_le.mpr mn)
Proof state after:
case h.xy
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 • unevenTerm u z1 n‖ ≤ (↑n * d).exp
Theorem: unevenLog_nonuniform_bound
Proof state before:
case h.xy
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 • unevenTerm u z1 n‖ ≤ (↑n * d).exp
Tactic:
calc ‖r1 ^ n • unevenTerm u z1 n‖
  _ = r1 ^ n * t := by
    simp only [← ht, norm_smul, abs_of_pos u.r1p, norm_pow, Real.norm_eq_abs, mul_eq_mul_left_iff,
      eq_self_iff_true, true_or_iff, abs_pow]
  _ ≤ r1 ^ n * (c * s⁻¹ ^ n) := by bound
  _ = r1 ^ n * (c * (e.exp ^ n / r1 ^ n)) := by rw [inv_div, div_pow]
  _ = r1 ^ n / r1 ^ n * c * e.exp ^ n := by ring
  _ = c * e.exp ^ n := by field_simp [(pow_pos u.r1p _).ne']
  _ = c * (↑n * e).exp := by rw [Real.exp_nat_mul]
  _ = c * (↑n * d - ↑n * (d - e)).exp := by ring_nf
  _ = c.log.exp * ((↑n * d).exp / (↑n * (d - e)).exp) := by rw [Real.exp_sub, Real.exp_log cp]
  _ = c.log.exp / (↑n * (d - e)).exp * (↑n * d).exp := by ring_nf
  _ = (c.log - ↑n * (d - e)).exp * (↑n * d).exp := by rw [Real.exp_sub]
  _ ≤ (c.log - c.log / (d - e) * (d - e)).exp * (↑n * d).exp := by bound
  _ ≤ (↑n * d).exp := by field_simp [(sub_pos.mpr ed).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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
⊢ s > 0
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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
⊢ s < r1
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
z1s : z1 ∈ closedBall c1 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
us : ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ c * s⁻¹ ^ n
m : ℕ
mb : max 1 (c.log / (d - e)) < ↑m
⊢ 1 ≤ max 1 (c.log / (d - e))
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
⊢ c.log / (d - e) ≤ max 1 (c.log / (d - e))
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 • unevenTerm u z1 n‖ = r1 ^ n * t
Tactic:
simp only [← ht, norm_smul, abs_of_pos u.r1p, norm_pow, Real.norm_eq_abs, mul_eq_mul_left_iff,
  eq_self_iff_true, true_or_iff, abs_pow]
Proof state after:
no goals