Theorem: term_approx (Ray/Dynamics/Multibrot/Bottcher.lean)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
set s := superF d
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have z0 : abs z ≠ 0 := (lt_of_lt_of_le (lt_trans (by norm_num) c16) cz).ne'
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have i8 : (abs z)⁻¹ ≤ 1 / 8 := by
  rw [one_div]; apply inv_le_inv_of_le; norm_num
  exact le_trans (by norm_num) (le_trans c16.le cz)
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have i1 : (abs z)⁻¹ ≤ 1 := le_trans i8 (by norm_num)
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
simp only [term]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
⊢ Complex.abs (g (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] z⁻¹) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
⊢ Complex.abs (g (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] z⁻¹) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have wc := iterates_converge (superNearF d c) n (inv_mem_t c16 cz)
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
wc : Complex.abs ((fl (f d) ∞ c)^[n] z⁻¹) ≤ (5 / 8) ^ n * Complex.abs z⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] z⁻¹) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
wc : Complex.abs ((fl (f d) ∞ c)^[n] z⁻¹) ≤ (5 / 8) ^ n * Complex.abs z⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] z⁻¹) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
generalize hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
wc : Complex.abs ((fl (f d) ∞ c)^[n] z⁻¹) ≤ (5 / 8) ^ n * Complex.abs z⁻¹
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
wc : Complex.abs ((fl (f d) ∞ c)^[n] z⁻¹) ≤ (5 / 8) ^ n * Complex.abs z⁻¹
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
rw [hw] at wc
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * Complex.abs z⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * Complex.abs z⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
replace wc : abs w ≤ (abs z)⁻¹ := by
  rw [map_inv₀] at wc
  exact le_trans wc (mul_le_of_le_one_left (inv_nonneg.mpr (Complex.abs.nonneg _)) (by bound))
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have cw : abs (c * w ^ d) ≤ (abs z)⁻¹ := by
  simp only [Complex.abs.map_mul, Complex.abs.map_pow]
  calc abs c * abs w ^ d
    _ ≤ abs z * (abs z)⁻¹ ^ d := by bound
    _ ≤ abs z * (abs z)⁻¹ ^ 2 := by bound
    _ = (abs z)⁻¹ := by rw [pow_two]; field_simp [z0]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have cw2 : abs (c * w ^ d) ≤ 1 / 2 := le_trans cw (le_trans i8 (by norm_num))
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
simp only [gl_f, gl]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs ((1 + c * w ^ d)⁻¹ ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs ((1 + c * w ^ d)⁻¹ ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
rw [Complex.inv_cpow, ← Complex.cpow_neg]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ (1 + c * w ^ d).arg ≠ Real.pi

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ (1 + c * w ^ d).arg ≠ Real.pi
Tactic:
swap
State after:
case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ (1 + c * w ^ d).arg ≠ Real.pi

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
⊢ 0 < 16
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ (Complex.abs z)⁻¹ ≤ 1 / 8
Tactic:
rw [one_div]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ (Complex.abs z)⁻¹ ≤ 8⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ (Complex.abs z)⁻¹ ≤ 8⁻¹
Tactic:
apply inv_le_inv_of_le
State after:
case ha
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 0 < 8

case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 8 ≤ Complex.abs z

State before:
case ha
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 0 < 8

case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 8 ≤ Complex.abs z
Tactic:
norm_num
State after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 8 ≤ Complex.abs z

State before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 8 ≤ Complex.abs z
Tactic:
exact le_trans (by norm_num) (le_trans c16.le cz)
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 8 ≤ 16
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ 1 / 8 ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * Complex.abs z⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs w ≤ (Complex.abs z)⁻¹
Tactic:
rw [map_inv₀] at wc
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * (Complex.abs z)⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs w ≤ (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * (Complex.abs z)⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs w ≤ (Complex.abs z)⁻¹
Tactic:
exact le_trans wc (mul_le_of_le_one_left (inv_nonneg.mpr (Complex.abs.nonneg _)) (by bound))
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * (Complex.abs z)⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ (5 / 8) ^ n ≤ 1
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
Tactic:
simp only [Complex.abs.map_mul, Complex.abs.map_pow]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs c * Complex.abs w ^ d ≤ (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs c * Complex.abs w ^ d ≤ (Complex.abs z)⁻¹
Tactic:
calc abs c * abs w ^ d
  _ ≤ abs z * (abs z)⁻¹ ^ d := by bound
  _ ≤ abs z * (abs z)⁻¹ ^ 2 := by bound
  _ = (abs z)⁻¹ := by rw [pow_two]; field_simp [z0]
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs c * Complex.abs w ^ d ≤ Complex.abs z * (Complex.abs z)⁻¹ ^ d
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs z * (Complex.abs z)⁻¹ ^ d ≤ Complex.abs z * (Complex.abs z)⁻¹ ^ 2
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs z * (Complex.abs z)⁻¹ ^ 2 = (Complex.abs z)⁻¹
Tactic:
rw [pow_two]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs z * ((Complex.abs z)⁻¹ * (Complex.abs z)⁻¹) = (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs z * ((Complex.abs z)⁻¹ * (Complex.abs z)⁻¹) = (Complex.abs z)⁻¹
Tactic:
field_simp [z0]
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
⊢ 1 / 8 ≤ 1 / 2
Tactic:
norm_num
State after:
no goals

State before:
case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ (1 + c * w ^ d).arg ≠ Real.pi
Tactic:
refine (lt_of_le_of_lt (le_abs_self _) (lt_of_le_of_lt ?_ (half_lt_self Real.pi_pos))).ne
State after:
case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ |(1 + c * w ^ d).arg| ≤ Real.pi / 2

State before:
case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ |(1 + c * w ^ d).arg| ≤ Real.pi / 2
Tactic:
rw [Complex.abs_arg_le_pi_div_two_iff, Complex.add_re, Complex.one_re]
State after:
case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 0 ≤ 1 + (c * w ^ d).re

State before:
case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 0 ≤ 1 + (c * w ^ d).re
Tactic:
calc 1 + (c * w ^ d).re
  _ ≥ 1 + -|(c * w ^ d).re| := by bound
  _ = 1 - |(c * w ^ d).re| := by ring
  _ ≥ 1 - abs (c * w ^ d) := by bound
  _ ≥ 1 - 1 / 2 := by linarith
  _ ≥ 0 := by norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 1 + (c * w ^ d).re ≥ 1 + -|(c * w ^ d).re|
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 1 + -|(c * w ^ d).re| = 1 - |(c * w ^ d).re|
Tactic:
ring
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 1 - |(c * w ^ d).re| ≥ 1 - Complex.abs (c * w ^ d)
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 1 - Complex.abs (c * w ^ d) ≥ 1 - 1 / 2
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 1 - 1 / 2 ≥ 0
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have dn : abs (-(1 / ((d ^ (n + 1) : ℕ) : ℂ))) ≤ (1 / 2 : ℝ) ^ (n + 1) := by
  simp only [Nat.cast_pow, one_div, map_neg_eq_map, map_inv₀, map_pow, Complex.abs_natCast,
    inv_pow]
  bound
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have d1 : abs (-(1 / ((d ^ (n + 1) : ℕ) : ℂ))) ≤ 1 := le_trans dn (by bound)
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
refine le_trans (pow_small ?_ d1) ?_
State after:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs (1 + c * w ^ d - 1) ≤ 1 / 2

case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * Complex.abs (1 + c * w ^ d - 1) * Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
Tactic:
simp only [Nat.cast_pow, one_div, map_neg_eq_map, map_inv₀, map_pow, Complex.abs_natCast,
  inv_pow]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ (↑d ^ (n + 1))⁻¹ ≤ (2 ^ (n + 1))⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ (↑d ^ (n + 1))⁻¹ ≤ (2 ^ (n + 1))⁻¹
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
⊢ (1 / 2) ^ (n + 1) ≤ 1
Tactic:
bound
State after:
no goals

State before:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs (1 + c * w ^ d - 1) ≤ 1 / 2
Tactic:
rw [add_sub_cancel_left]
State after:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs (c * w ^ d) ≤ 1 / 2

State before:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs (c * w ^ d) ≤ 1 / 2
Tactic:
exact cw2
State after:
no goals

State before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * Complex.abs (1 + c * w ^ d - 1) * Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
rw [add_sub_cancel_left]
State after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * Complex.abs (c * w ^ d) * Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * Complex.abs (c * w ^ d) * Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
calc 4 * abs (c * w ^ d) * abs (-(1 / ((d ^ (n + 1) : ℕ) : ℂ)))
  _ ≤ 4 * (abs z)⁻¹ * (1/2 : ℝ) ^ (n + 1) := by bound
  _ ≤ 2 * (1/2 : ℝ) ^ n * (abs z)⁻¹ := by
    simp only [pow_succ, ←mul_assoc, mul_comm _ (1/2:ℝ)]; norm_num
    simp only [mul_comm _ ((2:ℝ)^n)⁻¹, ←mul_assoc, le_refl]
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * Complex.abs (c * w ^ d) * Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 4 * (Complex.abs z)⁻¹ * (1 / 2) ^ (n + 1)
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * (Complex.abs z)⁻¹ * (1 / 2) ^ (n + 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
simp only [pow_succ, ←mul_assoc, mul_comm _ (1/2:ℝ)]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 1 / 2 * 4 * (Complex.abs z)⁻¹ * (1 / 2) ^ n ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 1 / 2 * 4 * (Complex.abs z)⁻¹ * (1 / 2) ^ n ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
norm_num
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 2 * (Complex.abs z)⁻¹ * (2 ^ n)⁻¹ ≤ 2 * (2 ^ n)⁻¹ * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 2 * (Complex.abs z)⁻¹ * (2 ^ n)⁻¹ ≤ 2 * (2 ^ n)⁻¹ * (Complex.abs z)⁻¹
Tactic:
simp only [mul_comm _ ((2:ℝ)^n)⁻¹, ←mul_assoc, le_refl]
State after:
no goals