internlm/Lean-Github huggingface dataset:
Theorem: f_approx
Proof 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
Proof 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
Theorem: f_approx
Proof 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']
Proof 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
Theorem: f_approx
Proof 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
Proof 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
Theorem: f_approx
Proof 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
Proof 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
Theorem: f_approx
Proof 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
Proof 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
Theorem: f_approx
Proof 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)
Proof 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
Theorem: f_approx
Proof 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))
Proof 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
Theorem: f_approx
Proof 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)
Proof 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
Theorem: f_approx
Proof 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]
Proof state after:
no goals
Theorem: f_approx
Proof 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
Proof state after:
no goals
Theorem: f_approx
Proof 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
Proof state after:
no goals
Theorem: f_approx
Proof 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
Proof state after:
no goals
Theorem: f_approx
Proof 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)]
Proof 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
Theorem: f_approx
Proof 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]
Proof 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
Theorem: f_approx
Proof 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
Proof state after:
no goals
Theorem: f_approx
Proof 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)]
Proof state after:
no goals
Theorem: f_approx
Proof 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']
Proof 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
Theorem: f_approx
Proof 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
Proof state after:
no goals
Theorem: f_approx
Proof 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
Proof state after:
no goals
Theorem: f_approx
Proof 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
Proof state after:
no goals
Theorem: f_approx
Proof 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']
Proof 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
Theorem: f_approx
Proof 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
Proof state after:
no goals
Theorem: f_approx
Proof 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]
Proof 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
Theorem: f_approx
Proof 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 _)
Proof 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
Theorem: f_approx
Proof 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))
Proof 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
Theorem: f_approx
Proof 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
Proof state after:
no goals