internlm/Lean-Github huggingface dataset:
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
⊢ 0 ≤ 1 + (c * w ^ d).re
Tactic:
calc 1 + (c * w ^ d).re
  _ ≥ 1 + -|(c * w ^ d).re| := by bound
  _ = 1 - |(c * w ^ d).re| := by ring
  _ ≥ 1 - abs (c * w ^ d) := by bound
  _ ≥ 1 - 1 / 2 := by linarith
  _ ≥ 0 := by norm_num
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)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 1 + (c * w ^ d).re ≥ 1 + -|(c * w ^ d).re|
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)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 1 + -|(c * w ^ d).re| = 1 - |(c * w ^ d).re|
Tactic:
ring
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)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 1 - |(c * w ^ d).re| ≥ 1 - Complex.abs (c * w ^ 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)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 1 - Complex.abs (c * w ^ d) ≥ 1 - 1 / 2
Tactic:
linarith
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)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ 1 - 1 / 2 ≥ 0
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 : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have dn : abs (-(1 / ((d ^ (n + 1) : ℕ) : ℂ))) ≤ (1 / 2 : ℝ) ^ (n + 1) := by
  simp only [Nat.cast_pow, one_div, map_neg_eq_map, map_inv₀, map_pow, Complex.abs_natCast,
    inv_pow]
  bound
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
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
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
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have d1 : abs (-(1 / ((d ^ (n + 1) : ℕ) : ℂ))) ≤ 1 := le_trans dn (by bound)
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
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
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
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs ((1 + c * w ^ d) ^ (-(1 / ↑(d ^ (n + 1)))) - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
refine le_trans (pow_small ?_ d1) ?_
Proof state after:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs (1 + c * w ^ d - 1) ≤ 1 / 2

case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * Complex.abs (1 + c * w ^ d - 1) * Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
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 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
Tactic:
simp only [Nat.cast_pow, one_div, map_neg_eq_map, map_inv₀, map_pow, Complex.abs_natCast,
  inv_pow]
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
⊢ (↑d ^ (n + 1))⁻¹ ≤ (2 ^ (n + 1))⁻¹
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
⊢ (↑d ^ (n + 1))⁻¹ ≤ (2 ^ (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)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
⊢ (1 / 2) ^ (n + 1) ≤ 1
Tactic:
bound
Proof state after:
no goals
Theorem: term_approx
Proof state before:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs (1 + c * w ^ d - 1) ≤ 1 / 2
Tactic:
rw [add_sub_cancel_left]
Proof state after:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs (c * w ^ d) ≤ 1 / 2
Theorem: term_approx
Proof state before:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ Complex.abs (c * w ^ d) ≤ 1 / 2
Tactic:
exact cw2
Proof state after:
no goals
Theorem: term_approx
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * Complex.abs (1 + c * w ^ d - 1) * Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
rw [add_sub_cancel_left]
Proof state after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * Complex.abs (c * w ^ d) * Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
i1 : (Complex.abs z)⁻¹ ≤ 1
w : ℂ
hw : (fl (f d) ∞ c)^[n] z⁻¹ = w
wc : Complex.abs w ≤ (Complex.abs z)⁻¹
cw : Complex.abs (c * w ^ d) ≤ (Complex.abs z)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * Complex.abs (c * w ^ d) * Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
calc 4 * abs (c * w ^ d) * abs (-(1 / ((d ^ (n + 1) : ℕ) : ℂ)))
  _ ≤ 4 * (abs z)⁻¹ * (1/2 : ℝ) ^ (n + 1) := by bound
  _ ≤ 2 * (1/2 : ℝ) ^ n * (abs z)⁻¹ := by
    simp only [pow_succ, ←mul_assoc, mul_comm _ (1/2:ℝ)]; norm_num
    simp only [mul_comm _ ((2:ℝ)^n)⁻¹, ←mul_assoc, le_refl]
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)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * Complex.abs (c * w ^ d) * Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 4 * (Complex.abs z)⁻¹ * (1 / 2) ^ (n + 1)
Tactic:
bound
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)⁻¹
cw2 : Complex.abs (c * w ^ d) ≤ 1 / 2
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 4 * (Complex.abs z)⁻¹ * (1 / 2) ^ (n + 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
simp only [pow_succ, ←mul_assoc, mul_comm _ (1/2:ℝ)]
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
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 1 / 2 * 4 * (Complex.abs z)⁻¹ * (1 / 2) ^ n ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
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
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 1 / 2 * 4 * (Complex.abs z)⁻¹ * (1 / 2) ^ n ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
norm_num
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
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 2 * (Complex.abs z)⁻¹ * (2 ^ n)⁻¹ ≤ 2 * (2 ^ n)⁻¹ * (Complex.abs z)⁻¹
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
dn : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ (1 / 2) ^ (n + 1)
d1 : Complex.abs (-(1 / ↑(d ^ (n + 1)))) ≤ 1
⊢ 2 * (Complex.abs z)⁻¹ * (2 ^ n)⁻¹ ≤ 2 * (2 ^ n)⁻¹ * (Complex.abs z)⁻¹
Tactic:
simp only [mul_comm _ ((2:ℝ)^n)⁻¹, ←mul_assoc, le_refl]
Proof state after:
no goals
Theorem: bottcher_approx_z
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
⊢ Complex.abs (⋯.bottcher c ↑z - z⁻¹) ≤ 16 * (Complex.abs z)⁻¹ ^ 2
Tactic:
set s := superF d
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
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (s.bottcher c ↑z - z⁻¹) ≤ 16 * (Complex.abs z)⁻¹ ^ 2
Theorem: bottcher_approx_z
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
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (s.bottcher c ↑z - z⁻¹) ≤ 16 * (Complex.abs z)⁻¹ ^ 2
Tactic:
have i8 : (abs z)⁻¹ ≤ 1 / 8 := by
  rw [one_div]; apply inv_le_inv_of_le; norm_num
  exact le_trans (by norm_num) (le_trans c16.le cz)
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (s.bottcher c ↑z - z⁻¹) ≤ 16 * (Complex.abs z)⁻¹ ^ 2
Theorem: bottcher_approx_z
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (s.bottcher c ↑z - z⁻¹) ≤ 16 * (Complex.abs z)⁻¹ ^ 2
Tactic:
simp only [bottcher_eq_bottcherNear_z c16 cz, bottcherNear, Complex.abs.map_mul, ← mul_sub_one,
  pow_two, ← mul_assoc, map_inv₀, mul_comm (abs z)⁻¹]
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) * (Complex.abs z)⁻¹ ≤
    16 * (Complex.abs z)⁻¹ * (Complex.abs z)⁻¹
Theorem: bottcher_approx_z
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) * (Complex.abs z)⁻¹ ≤
    16 * (Complex.abs z)⁻¹ * (Complex.abs z)⁻¹
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (inv_nonneg.mpr (Complex.abs.nonneg _))
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 16 * (Complex.abs z)⁻¹
Theorem: bottcher_approx_z
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 16 * (Complex.abs z)⁻¹
Tactic:
rcases term_prod_exists (superNearF d c) _ (inv_mem_t c16 cz) with ⟨p, h⟩
Proof state after:
case intro
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : HasProd (fun n => term (fl (f d) ∞ c) d n z⁻¹) p
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 16 * (Complex.abs z)⁻¹
Theorem: bottcher_approx_z
Proof state before:
case intro
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : HasProd (fun n => term (fl (f d) ∞ c) d n z⁻¹) p
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 16 * (Complex.abs z)⁻¹
Tactic:
rw [h.tprod_eq]
Proof state after:
case intro
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : HasProd (fun n => term (fl (f d) ∞ c) d n z⁻¹) p
⊢ Complex.abs (p - 1) ≤ 16 * (Complex.abs z)⁻¹
Theorem: bottcher_approx_z
Proof state before:
case intro
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : HasProd (fun n => term (fl (f d) ∞ c) d n z⁻¹) p
⊢ Complex.abs (p - 1) ≤ 16 * (Complex.abs z)⁻¹
Tactic:
simp only [HasProd] at h
Proof state after:
case intro
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
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : Tendsto (fun s => s.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) Filter.atTop (𝓝 p)
⊢ Complex.abs (p - 1) ≤ 16 * (Complex.abs z)⁻¹