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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), z ∈ t → Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
intro n zt
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
rw [term]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 1 / 2 * (1 / 2) ^ n

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
trans 4 * abs (g f d (f^[n] z) - 1) * abs (1 / (d ^ (n + 1) : ℕ) : ℂ)
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1)))

f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1)))
Tactic:
apply pow_small
State after:
case zs
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 2

case ws
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1

State before:
case zs
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 2
Tactic:
exact le_trans (s.gs (s.mapsTo n zt)) (by norm_num)
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 1 / 4 ≤ 1 / 2
Tactic:
norm_num
State after:
no goals

State before:
case ws
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1
Tactic:
simp only [one_div, map_inv₀, Complex.abs_pow, Complex.abs_natCast, Nat.cast_pow]
State after:
case ws
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ (↑d ^ (n + 1))⁻¹ ≤ 1

State before:
case ws
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ (↑d ^ (n + 1))⁻¹ ≤ 1
Tactic:
apply inv_le_one
State after:
case ws.ha
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 1 ≤ ↑d ^ (n + 1)

State before:
case ws.ha
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 1 ≤ ↑d ^ (n + 1)
Tactic:
have hd : 1 ≤ (d : ℝ) := le_trans (by norm_num) s.dr2
State after:
case ws.ha
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
hd : 1 ≤ ↑d
⊢ 1 ≤ ↑d ^ (n + 1)

State before:
case ws.ha
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
hd : 1 ≤ ↑d
⊢ 1 ≤ ↑d ^ (n + 1)
Tactic:
exact one_le_pow_of_one_le hd _
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 1 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
have gs : abs (g f d (f^[n] z) - 1) ≤ 1 / 4 := s.gs (s.mapsTo n zt)
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
have ps : abs (1 / (d:ℂ) ^ (n + 1) : ℂ) ≤ 1/2 * (1/2 : ℝ) ^ n := by
  have nn : (1/2:ℝ) * (1/2 : ℝ) ^ n = (1/2 : ℝ) ^ (n + 1) := (pow_succ' _ _).symm
  rw [nn]
  simp only [one_div, map_inv₀, map_pow, Complex.abs_natCast, inv_pow, ge_iff_le]
  bound
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
ps : Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
ps : Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
calc (4:ℝ) * abs (g f d (f^[n] z) - 1) * abs ((1:ℂ) / (d ^ (n + 1) : ℕ) : ℂ)
  _ = (4:ℝ) * abs (g f d (f^[n] z) - 1) * abs ((1:ℂ) / (d:ℂ) ^ (n + 1) : ℂ) := by
    rw [Nat.cast_pow]
  _ ≤ 4 * (1 / 4) * (1 / 2 * (1 / 2 : ℝ) ^ n) := by bound
  _ = 1 / 2 * (1 / 2 : ℝ) ^ n := by ring
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
⊢ Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
have nn : (1/2:ℝ) * (1/2 : ℝ) ^ n = (1/2 : ℝ) ^ (n + 1) := (pow_succ' _ _).symm
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
rw [nn]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ Complex.abs (1 / ↑d ^ (n + 1)) ≤ (1 / 2) ^ (n + 1)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ Complex.abs (1 / ↑d ^ (n + 1)) ≤ (1 / 2) ^ (n + 1)
Tactic:
simp only [one_div, map_inv₀, map_pow, Complex.abs_natCast, inv_pow, ge_iff_le]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ (↑d ^ (n + 1))⁻¹ ≤ (2 ^ (n + 1))⁻¹

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ (↑d ^ (n + 1))⁻¹ ≤ (2 ^ (n + 1))⁻¹
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
ps : Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) =
    4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑d ^ (n + 1))
Tactic:
rw [Nat.cast_pow]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
ps : Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑d ^ (n + 1)) ≤ 4 * (1 / 4) * (1 / 2 * (1 / 2) ^ n)
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
ps : Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 4 * (1 / 4) * (1 / 2 * (1 / 2) ^ n) = 1 / 2 * (1 / 2) ^ n
Tactic:
ring
State after:
no goals