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

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

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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (z ^ d * g f d z) ≤ 5 / 8 * Complex.abs z
Tactic:
simp
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z
Tactic:
have gs : abs (g f d z) ≤ 5 / 4 := by
  calc abs (g f d z)
    _ = abs (g f d z - 1 + 1) := by ring_nf
    _ ≤ abs (g f d z - 1) + abs (1 : ℂ) := by bound
    _ ≤ 1 / 4 + abs (1 : ℂ) := by linarith [s.gs zt]
    _ ≤ 5 / 4 := by norm_num
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z
Tactic:
have az1 : abs z ≤ 1 := le_trans (s.t2 zt) (by norm_num)
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z
Tactic:
calc abs z ^ d * abs (g f d z)
  _ ≤ abs z ^ 2 * (5 / 4) := by bound
  _ = abs z * abs z * (5 / 4) := by ring_nf
  _ ≤ 1 / 2 * abs z * (5 / 4) := by bound [s.t2 zt]
  _ = 5 / 8 * abs z := by ring
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (g f d z) ≤ 5 / 4
Tactic:
calc abs (g f d z)
  _ = abs (g f d z - 1 + 1) := by ring_nf
  _ ≤ abs (g f d z - 1) + abs (1 : ℂ) := by bound
  _ ≤ 1 / 4 + abs (1 : ℂ) := by linarith [s.gs zt]
  _ ≤ 5 / 4 := by norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (g f d z) = Complex.abs (g f d z - 1 + 1)
Tactic:
ring_nf
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (g f d z - 1 + 1) ≤ Complex.abs (g f d z - 1) + Complex.abs 1
Tactic:
bound
State after:
no goals

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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ 1 / 4 + Complex.abs 1 ≤ 5 / 4
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
⊢ 1 / 2 ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ Complex.abs z ^ 2 * (5 / 4)
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ Complex.abs z ^ 2 * (5 / 4) = Complex.abs z * Complex.abs z * (5 / 4)
Tactic:
ring_nf
State after:
no goals

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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ 1 / 2 * Complex.abs z * (5 / 4) = 5 / 8 * Complex.abs z
Tactic:
ring
State after:
no goals