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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), z ∈ t → Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
Tactic:
intro n zt
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
Tactic:
induction' n with n nh
State after:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (f^[0] z) ≤ (5 / 8) ^ 0 * Complex.abs z

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs (f^[n + 1] z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z

State before:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (f^[0] z) ≤ (5 / 8) ^ 0 * Complex.abs z
Tactic:
simp only [Function.iterate_zero, id, pow_zero, one_mul, Nat.cast_one, le_refl]
State after:
no goals

State before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs (f^[n + 1] z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z
Tactic:
rw [Function.iterate_succ']
State after:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs ((f ∘ f^[n]) z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z

State before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs ((f ∘ f^[n]) z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z
Tactic:
trans (5/8 : ℝ) * abs (f^[n] z)
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs ((f ∘ f^[n]) z) ≤ 5 / 8 * Complex.abs (f^[n] z)

f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ 5 / 8 * Complex.abs (f^[n] z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs ((f ∘ f^[n]) z) ≤ 5 / 8 * Complex.abs (f^[n] z)
Tactic:
exact f_converges s (s.mapsTo n zt)
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ 5 / 8 * Complex.abs (f^[n] z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z
Tactic:
calc (5/8 : ℝ) * abs (f^[n] z)
  _ ≤ (5/8 : ℝ) * ((5/8 : ℝ) ^ n * abs z) := by bound
  _ = 5/8 * (5/8 : ℝ) ^ n * abs z := by ring
  _ = (5/8 : ℝ) ^ (n + 1) * abs z := by rw [← pow_succ']
  _ = (5/8 : ℝ) ^ n.succ * abs z := rfl
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ 5 / 8 * Complex.abs (f^[n] z) ≤ 5 / 8 * ((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
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ 5 / 8 * ((5 / 8) ^ n * Complex.abs z) = 5 / 8 * (5 / 8) ^ n * Complex.abs z
Tactic:
ring
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ 5 / 8 * (5 / 8) ^ n * Complex.abs z = (5 / 8) ^ (n + 1) * Complex.abs z
Tactic:
rw [← pow_succ']
State after:
no goals