Theorem: unevenLog_nonuniform_bound (Ray/Hartogs/Hartogs.lean)

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 > 0, ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
intro d dp
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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d

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
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
rcases exists_between dp with ⟨e, ep, ed⟩
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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d

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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
set s := r1 / e.exp
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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d

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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
have sp : s > 0 := by bound
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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d

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
z1s : z1 ∈ closedBall c1 r1
d : ℝ
dp : d > 0
e : ℝ
ep : 0 < e
ed : e < d
s : ℝ := r1 / e.exp
sp : s > 0
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
have sr : s < r1 := by bound
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
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
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d

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
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
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
rcases unevenSeries_nonuniform_bound u sp sr z1s with ⟨c, cp, us⟩
State after:
case 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
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d

State before:
case 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
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d
Tactic:
rcases exists_nat_gt (max 1 (c.log / (d - e))) with ⟨m, mb⟩
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
⊢ ∀ᶠ (n : ℕ) in atTop, unevenLog u n z1 ≤ d

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)
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

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]
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

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
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

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
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

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
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

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
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

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
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

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
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

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))]
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

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
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

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 : ℝ)
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

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
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

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
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

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)
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

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']
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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']
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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']
State after:
no goals