Theorem: f_approx (Ray/Dynamics/Multibrot/Iterates.lean)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have dp : 0 < d := d_pos d
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have d2 : 2 ≤ (d : ℝ) := two_le_cast_d d
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have z1' : 1 < abs z := lt_of_lt_of_le (by norm_num) z3
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have z0' : 0 < abs z := by positivity
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have iz1 : 1 / abs z < 1 := (div_lt_one z0').mpr z1'
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have z0 : z ≠ 0 := Complex.abs.ne_zero_iff.mp (by positivity)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have cz_le : abs (c / z ^ d) ≤ 1 / abs z := by
  have d1 : z^d = z^(d - 1 + 1) := by rw [Nat.sub_add_cancel (d_ge_one d)]
  simp only [d1, map_div₀, Complex.abs.map_pow, pow_succ', Complex.abs.map_mul,
    div_mul_eq_div_div]
  bound
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l0s : 1 ≤ log (abs z) := by
  rw [Real.le_log_iff_exp_le z0']; exact le_trans Real.exp_one_lt_3.le z3
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l0 : 0 < log (abs z) := by positivity
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l1 : 0 < ↑d * log (abs z) := by positivity
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l1' : 1 < log (abs z) := by
  rw [Real.lt_log_iff_exp_lt z0']; exact lt_of_lt_of_le Real.exp_one_lt_3 z3
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l2 : |log (abs (1 + c / z ^ d))| ≤ -log (1 - 1 / abs z) := by
  nth_rw 1 [← Complex.log_re]
  apply le_trans (Complex.abs_re_le_abs _)
  apply le_trans (Complex.abs_log_one_add_le (trans cz_le iz1))
  exact Real.neg_log_one_sub_mono cz_le iz1
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have dl2 : 2 < d * log (abs z) := by
  calc ↑d * log (abs z)
    _ ≥ 2 * log (abs z) := by gcongr
    _ > 2 * 1 := by gcongr
    _ = 2 := by norm_num
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l3 : 0 < ↑d * log (abs z) + log (abs (1 + c / z ^ d)) := by
  have i2 : 1/abs z ≤ 1/2 := one_div_le_one_div_of_le (by norm_num) (by linarith)
  suffices h : -log (abs (1 + c / z ^ d)) < ↑d * log (abs z) by linarith
  apply lt_of_le_of_lt (neg_le_neg_iff.mpr (abs_le.mp l2).1); simp only [neg_neg]
  exact lt_of_le_of_lt (neg_log_one_sub_le_two i2) dl2
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
rw [log_abs_add (z ^ d) c (pow_ne_zero _ z0) (f_ne_zero cz z3), Complex.abs.map_pow, Real.log_pow,
  log_add _ _ l1 l3, Real.log_mul (Nat.cast_ne_zero.mpr (d_ne_zero d)) l0.ne']
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
⊢ |(↑d).log + (Complex.abs z).log.log + (1 + (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log)).log -
          (Complex.abs z).log.log -
        (↑d).log| ≤
    f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
⊢ |(↑d).log + (Complex.abs z).log.log + (1 + (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log)).log -
          (Complex.abs z).log.log -
        (↑d).log| ≤
    f_error d z
Tactic:
generalize hu : log (abs (1 + c / z ^ d)) / (d * log (abs z)) = u
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ |(↑d).log + (Complex.abs z).log.log + (1 + u).log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ |(↑d).log + (Complex.abs z).log.log + (1 + u).log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
ring_nf
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ |(1 + u).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ |(1 + u).log| ≤ f_error d z
Tactic:
have inner : |u| ≤ -log (1 - 1/abs z) / (d * log (abs z)) := by
  simp only [←hu, abs_div, abs_of_pos l1, div_le_iff l1]
  apply le_trans l2; apply le_of_eq; field_simp
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
⊢ |(1 + u).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
⊢ |(1 + u).log| ≤ f_error d z
Tactic:
have weak : -log (1 - 1/abs z) / (d * log (abs z)) < 1 := by
  rw [div_lt_one l1]
  refine lt_of_le_of_lt (neg_log_one_sub_le_two ?_) dl2
  exact one_div_le_one_div_of_le (by norm_num) (by linarith)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
weak : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) < 1
⊢ |(1 + u).log| ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
weak : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) < 1
⊢ |(1 + u).log| ≤ f_error d z
Tactic:
apply le_trans (Real.abs_log_one_add_le (trans inner weak))
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
weak : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) < 1
⊢ -(1 - |u|).log ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
weak : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) < 1
⊢ -(1 - |u|).log ≤ f_error d z
Tactic:
apply le_trans (Real.neg_log_one_sub_mono inner weak)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
weak : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) < 1
⊢ -(1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ f_error d z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
weak : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) < 1
⊢ -(1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ f_error d z
Tactic:
rw [f_error]
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
⊢ 1 < 3
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
⊢ 0 < Complex.abs z
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
⊢ Complex.abs z ≠ 0
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
⊢ Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
Tactic:
have d1 : z^d = z^(d - 1 + 1) := by rw [Nat.sub_add_cancel (d_ge_one d)]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
d1 : z ^ d = z ^ (d - 1 + 1)
⊢ Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
d1 : z ^ d = z ^ (d - 1 + 1)
⊢ Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
Tactic:
simp only [d1, map_div₀, Complex.abs.map_pow, pow_succ', Complex.abs.map_mul,
  div_mul_eq_div_div]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
d1 : z ^ d = z ^ (d - 1 + 1)
⊢ Complex.abs c / Complex.abs z / Complex.abs z ^ (d - 1) ≤ 1 / Complex.abs z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
d1 : z ^ d = z ^ (d - 1 + 1)
⊢ Complex.abs c / Complex.abs z / Complex.abs z ^ (d - 1) ≤ 1 / Complex.abs z
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
⊢ z ^ d = z ^ (d - 1 + 1)
Tactic:
rw [Nat.sub_add_cancel (d_ge_one d)]
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
⊢ 1 ≤ (Complex.abs z).log
Tactic:
rw [Real.le_log_iff_exp_le z0']
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
⊢ exp 1 ≤ Complex.abs z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
⊢ exp 1 ≤ Complex.abs z
Tactic:
exact le_trans Real.exp_one_lt_3.le z3
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
⊢ 0 < (Complex.abs z).log
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0 < ↑d * (Complex.abs z).log
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
⊢ 1 < (Complex.abs z).log
Tactic:
rw [Real.lt_log_iff_exp_lt z0']
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
⊢ exp 1 < Complex.abs z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
⊢ exp 1 < Complex.abs z
Tactic:
exact lt_of_lt_of_le Real.exp_one_lt_3 z3
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
Tactic:
nth_rw 1 [← Complex.log_re]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ |(1 + c / z ^ d).log.re| ≤ -(1 - 1 / Complex.abs z).log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ |(1 + c / z ^ d).log.re| ≤ -(1 - 1 / Complex.abs z).log
Tactic:
apply le_trans (Complex.abs_re_le_abs _)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ Complex.abs (1 + c / z ^ d).log ≤ -(1 - 1 / Complex.abs z).log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ Complex.abs (1 + c / z ^ d).log ≤ -(1 - 1 / Complex.abs z).log
Tactic:
apply le_trans (Complex.abs_log_one_add_le (trans cz_le iz1))
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ -(1 - Complex.abs (c / z ^ d)).log ≤ -(1 - 1 / Complex.abs z).log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ -(1 - Complex.abs (c / z ^ d)).log ≤ -(1 - 1 / Complex.abs z).log
Tactic:
exact Real.neg_log_one_sub_mono cz_le iz1
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
⊢ 2 < ↑d * (Complex.abs z).log
Tactic:
calc ↑d * log (abs z)
  _ ≥ 2 * log (abs z) := by gcongr
  _ > 2 * 1 := by gcongr
  _ = 2 := by norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
⊢ ↑d * (Complex.abs z).log ≥ 2 * (Complex.abs z).log
Tactic:
gcongr
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
⊢ 2 * (Complex.abs z).log > 2 * 1
Tactic:
gcongr
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
⊢ 2 * 1 = 2
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
⊢ 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
Tactic:
have i2 : 1/abs z ≤ 1/2 := one_div_le_one_div_of_le (by norm_num) (by linarith)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
Tactic:
suffices h : -log (abs (1 + c / z ^ d)) < ↑d * log (abs z) by linarith
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ -(Complex.abs (1 + c / z ^ d)).log < ↑d * (Complex.abs z).log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ -(Complex.abs (1 + c / z ^ d)).log < ↑d * (Complex.abs z).log
Tactic:
apply lt_of_le_of_lt (neg_le_neg_iff.mpr (abs_le.mp l2).1)
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ - - -(1 - 1 / Complex.abs z).log < ↑d * (Complex.abs z).log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ - - -(1 - 1 / Complex.abs z).log < ↑d * (Complex.abs z).log
Tactic:
simp only [neg_neg]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ -(1 - 1 / Complex.abs z).log < ↑d * (Complex.abs z).log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ -(1 - 1 / Complex.abs z).log < ↑d * (Complex.abs z).log
Tactic:
exact lt_of_le_of_lt (neg_log_one_sub_le_two i2) dl2
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
⊢ 2 ≤ Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
i2 : 1 / Complex.abs z ≤ 1 / 2
h : -(Complex.abs (1 + c / z ^ d)).log < ↑d * (Complex.abs z).log
⊢ 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
simp only [←hu, abs_div, abs_of_pos l1, div_le_iff l1]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ |(Complex.abs (1 + c / z ^ d)).log| ≤
    -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) * (↑d * (Complex.abs z).log)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ |(Complex.abs (1 + c / z ^ d)).log| ≤
    -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) * (↑d * (Complex.abs z).log)
Tactic:
apply le_trans l2
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ -(1 - 1 / Complex.abs z).log ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) * (↑d * (Complex.abs z).log)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ -(1 - 1 / Complex.abs z).log ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) * (↑d * (Complex.abs z).log)
Tactic:
apply le_of_eq
State after:
case a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ -(1 - 1 / Complex.abs z).log = -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) * (↑d * (Complex.abs z).log)

State before:
case a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
⊢ -(1 - 1 / Complex.abs z).log = -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) * (↑d * (Complex.abs z).log)
Tactic:
field_simp
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
⊢ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) < 1
Tactic:
rw [div_lt_one l1]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
⊢ -(1 - 1 / Complex.abs z).log < ↑d * (Complex.abs z).log

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
⊢ -(1 - 1 / Complex.abs z).log < ↑d * (Complex.abs z).log
Tactic:
refine lt_of_le_of_lt (neg_log_one_sub_le_two ?_) dl2
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
⊢ 1 / Complex.abs z ≤ 1 / 2

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
⊢ 1 / Complex.abs z ≤ 1 / 2
Tactic:
exact one_div_le_one_div_of_le (by norm_num) (by linarith)
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
dl2 : 2 < ↑d * (Complex.abs z).log
l3 : 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).log
u : ℝ
hu : (Complex.abs (1 + c / z ^ d)).log / (↑d * (Complex.abs z).log) = u
inner : |u| ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
⊢ 2 ≤ Complex.abs z
Tactic:
linarith
State after:
no goals