Theorem: iterates_tendsto (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)
Tactic:
by_cases z0 : z = 0
State after:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)

case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)

State before:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)

case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)
Tactic:
simp only [z0, iterates_at_zero s, tendsto_const_nhds]
State after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)

State before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)
Tactic:
rw [Metric.tendsto_atTop]
State after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f^[n] z) 0 < ε

State before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f^[n] z) 0 < ε
Tactic:
intro e ep
State after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (f^[n] z) 0 < e

State before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (f^[n] z) 0 < e
Tactic:
simp only [Complex.dist_eq, sub_zero]
State after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e

State before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Tactic:
have xp : e / abs z > 0 := div_pos ep (Complex.abs.pos z0)
State after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e

State before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Tactic:
rcases exists_pow_lt_of_lt_one xp (by norm_num : (5 / 8 : ℝ) < 1) with ⟨N, Nb⟩
State after:
case neg.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N < e / Complex.abs z
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e

State before:
case neg.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N < e / Complex.abs z
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Tactic:
simp only [lt_div_iff (Complex.abs.pos z0)] at Nb
State after:
case neg.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e

State before:
case neg.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Tactic:
use N
State after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
⊢ ∀ n ≥ N, Complex.abs (f^[n] z) < e

State before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
⊢ ∀ n ≥ N, Complex.abs (f^[n] z) < e
Tactic:
intro n nN
State after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
n : ℕ
nN : n ≥ N
⊢ Complex.abs (f^[n] z) < e

State before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
n : ℕ
nN : n ≥ N
⊢ Complex.abs (f^[n] z) < e
Tactic:
refine lt_of_le_of_lt (iterates_converge s n zt) (lt_of_le_of_lt ?_ Nb)
State after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
n : ℕ
nN : n ≥ N
⊢ (5 / 8) ^ n * Complex.abs z ≤ (5 / 8) ^ N * Complex.abs z

State before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
n : ℕ
nN : n ≥ N
⊢ (5 / 8) ^ n * Complex.abs z ≤ (5 / 8) ^ N * Complex.abs z
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
⊢ 5 / 8 < 1
Tactic:
norm_num
State after:
no goals