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
⊢ 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
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
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
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
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
⊢ 2 * (Complex.abs z).log > 2 * 1
Tactic:
gcongr
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
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
⊢ 2 * 1 = 2
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
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)
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
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ 0 < ↑d * (Complex.abs z).log + (Complex.abs (1 + c / z ^ d)).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
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
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
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ -(Complex.abs (1 + c / z ^ d)).log < ↑d * (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
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)
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
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ - - -(1 - 1 / Complex.abs z).log < ↑d * (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
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]
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
i2 : 1 / Complex.abs z ≤ 1 / 2
⊢ -(1 - 1 / Complex.abs z).log < ↑d * (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
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
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
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
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
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
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
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
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
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]
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
⊢ |(Complex.abs (1 + c / z ^ d)).log| ≤
    -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) * (↑d * (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
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
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 - 1 / Complex.abs z).log ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) * (↑d * (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
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
Proof 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)
Theorem: f_approx
Proof 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
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
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]
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 - 1 / Complex.abs z).log < ↑d * (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
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
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 / Complex.abs z ≤ 1 / 2
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 / Complex.abs z ≤ 1 / 2
Tactic:
exact one_div_le_one_div_of_le (by norm_num) (by linarith)
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
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
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
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
Proof state after:
no goals
Theorem: iter_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
Tactic:
induction' n with n h generalizing z
Proof state after:
case zero
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[0] z)).log.log - (Complex.abs z).log.log - ↑0 * (↑d).log| ≤ iter_error d c z

case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[n + 1] z)).log.log - (Complex.abs z).log.log - ↑(n + 1) * (↑d).log| ≤ iter_error d c z
Theorem: iter_approx
Proof state before:
case zero
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[0] z)).log.log - (Complex.abs z).log.log - ↑0 * (↑d).log| ≤ iter_error d c z
Tactic:
simp only [Nat.zero_eq, Function.iterate_zero, id_eq, sub_self, CharP.cast_eq_zero, zero_mul,
  abs_zero, iter_error_nonneg d z3 cz]
Proof state after:
no goals
Theorem: iter_approx
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[n + 1] z)).log.log - (Complex.abs z).log.log - ↑(n + 1) * (↑d).log| ≤ iter_error d c z
Tactic:
simp only [Finset.sum_range_succ, Function.iterate_succ_apply, Nat.succ_eq_add_one,
  Nat.cast_add_one]
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
h :
  ∀ {z : ℂ},
    3 ≤ Complex.abs z →
      Complex.abs c ≤ Complex.abs z →
        |(Complex.abs ((f' d c)^[n] z)).log.log - (Complex.abs z).log.log - ↑n * (↑d).log| ≤ iter_error d c z
z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ |(Complex.abs ((f' d c)^[n] (f' d c z))).log.log - (Complex.abs z).log.log - (↑n + 1) * (↑d).log| ≤ iter_error d c z