internlm/Lean-Github huggingface dataset:
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have i1 : (abs z)⁻¹ ≤ 1 := le_trans i8 (by norm_num)
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
simp only [term]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
⊢ Complex.abs (g (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] z⁻¹) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
⊢ Complex.abs (g (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] z⁻¹) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have wc := iterates_converge (superNearF d c) n (inv_mem_t c16 cz)
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
wc : Complex.abs ((fl (f d) ∞ c)^[n] z⁻¹) ≤ (5 / 8) ^ n * Complex.abs z⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] z⁻¹) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
wc : Complex.abs ((fl (f d) ∞ c)^[n] z⁻¹) ≤ (5 / 8) ^ n * Complex.abs z⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] z⁻¹) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
generalize hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
wc : Complex.abs ((fl (f d) ∞ c)^[n] z⁻¹) ≤ (5 / 8) ^ n * Complex.abs z⁻¹
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
wc : Complex.abs ((fl (f d) ∞ c)^[n] z⁻¹) ≤ (5 / 8) ^ n * Complex.abs z⁻¹
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
rw [hw] at wc
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * Complex.abs z⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * Complex.abs z⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
replace wc : abs w ≤ (abs z)⁻¹ := by
  rw [map_inv₀] at wc
  exact le_trans wc (mul_le_of_le_one_left (inv_nonneg.mpr (Complex.abs.nonneg _)) (by bound))
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have cw : abs (c * w ^ d) ≤ (abs z)⁻¹ := by
  simp only [Complex.abs.map_mul, Complex.abs.map_pow]
  calc abs c * abs w ^ d
    _ ≤ abs z * (abs z)⁻¹ ^ d := by bound
    _ ≤ abs z * (abs z)⁻¹ ^ 2 := by bound
    _ = (abs z)⁻¹ := by rw [pow_two]; field_simp [z0]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have cw2 : abs (c * w ^ d) ≤ 1 / 2 := le_trans cw (le_trans i8 (by norm_num))
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs (g (fl (f d) ∞ c) d w ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
simp only [gl_f, gl]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs ((1 + c * w ^ d)⁻¹ ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs ((1 + c * w ^ d)⁻¹ ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
rw [Complex.inv_cpow, ← Complex.cpow_neg]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹

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

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

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

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

case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 8 ≤ Complex.abs z
Tactic:
norm_num
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 8 ≤ Complex.abs z
Theorem: term_approx
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 8 ≤ Complex.abs z
Tactic:
exact le_trans (by norm_num) (le_trans c16.le cz)
Proof state after:
no goals
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ 8 ≤ 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ 1 / 8 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * Complex.abs z⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs w ≤ (Complex.abs z)⁻¹
Tactic:
rw [map_inv₀] at wc
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * (Complex.abs z)⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs w ≤ (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * (Complex.abs z)⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ Complex.abs w ≤ (Complex.abs z)⁻¹
Tactic:
exact le_trans wc (mul_le_of_le_one_left (inv_nonneg.mpr (Complex.abs.nonneg _)) (by bound))
Proof state after:
no goals
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
wc : Complex.abs w ≤ (5 / 8) ^ n * (Complex.abs z)⁻¹
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
⊢ (5 / 8) ^ n ≤ 1
Tactic:
bound
Proof state after:
no goals
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
Tactic:
simp only [Complex.abs.map_mul, Complex.abs.map_pow]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs c * Complex.abs w ^ d ≤ (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs c * Complex.abs w ^ d ≤ (Complex.abs z)⁻¹
Tactic:
calc abs c * abs w ^ d
  _ ≤ abs z * (abs z)⁻¹ ^ d := by bound
  _ ≤ abs z * (abs z)⁻¹ ^ 2 := by bound
  _ = (abs z)⁻¹ := by rw [pow_two]; field_simp [z0]
Proof state after:
no goals
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs c * Complex.abs w ^ d ≤ Complex.abs z * (Complex.abs z)⁻¹ ^ d
Tactic:
bound
Proof state after:
no goals
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs z * (Complex.abs z)⁻¹ ^ d ≤ Complex.abs z * (Complex.abs z)⁻¹ ^ 2
Tactic:
bound
Proof state after:
no goals
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs z * (Complex.abs z)⁻¹ ^ 2 = (Complex.abs z)⁻¹
Tactic:
rw [pow_two]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs z * ((Complex.abs z)⁻¹ * (Complex.abs z)⁻¹) = (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
⊢ Complex.abs z * ((Complex.abs z)⁻¹ * (Complex.abs z)⁻¹) = (Complex.abs z)⁻¹
Tactic:
field_simp [z0]
Proof state after:
no goals
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
⊢ 1 / 8 ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_approx
Proof state before:
case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ (1 + c * w ^ d).arg ≠ Real.pi
Tactic:
refine (lt_of_le_of_lt (le_abs_self _) (lt_of_le_of_lt ?_ (half_lt_self Real.pi_pos))).ne
Proof state after:
case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ |(1 + c * w ^ d).arg| ≤ Real.pi / 2
Theorem: term_approx
Proof state before:
case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ |(1 + c * w ^ d).arg| ≤ Real.pi / 2
Tactic:
rw [Complex.abs_arg_le_pi_div_two_iff, Complex.add_re, Complex.one_re]
Proof state after:
case hx
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 0 ≤ 1 + (c * w ^ d).re