internlm/Lean-Github huggingface dataset:
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 < (1 - (bb * b - 1)⁻¹) * bb * Complex.abs z * (Complex.abs z).log
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 ≤ (Complex.abs z).log
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 ≤ (1 - (bb * b - 1)⁻¹) * Complex.abs (f' d c (f' d c z))
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 ≤ 1 - (bb * b - 1)⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
i b s0 s1 s2 : ℝ
c : ℂ
b3 : 3 ≤ b
s1p : 0 ≤ s1
s2p : 0 ≤ s2
bs0 : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s0 / (Complex.abs w * (Complex.abs w).log)
bs1 : ∀ {w : ℂ}, (b ^ (d - 1) - 1) * b ≤ Complex.abs w → f_error d w ≤ s1 / (Complex.abs w * (Complex.abs w).log)
b0' : 0 < b ^ (d - 1) - 1
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
b0 : 0 < b
z0 : 0 < Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 1 < (Complex.abs z).log
bb : ℝ
hbb : (b ^ (d - 1) - 1) ^ d * b ^ (d - 1) - 1 = bb
b11 : 11 ≤ bb
bb3 : 3 ≤ bb * b
bs2 : ∀ {w : ℂ}, bb * b ≤ Complex.abs w → f_error d w ≤ s2 / (Complex.abs w * (Complex.abs w).log)
b0'' : 0 < 1 - (bb * b - 1)⁻¹
si : s0 + s1 / (b ^ (d - 1) - 1) + s2 / ((1 - (bb * b - 1)⁻¹) * bb) ≤ i
fz : Complex.abs z ^ d - Complex.abs c ≤ Complex.abs (f' d c z)
fz' : (b ^ (d - 1) - 1) * Complex.abs z ≤ Complex.abs (f' d c z)
zfz : Complex.abs z ≤ Complex.abs (f' d c z)
zffz : Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
bfz : b ≤ Complex.abs (f' d c z)
ffz : bb * Complex.abs z ≤ Complex.abs (f' d c (f' d c z))
e0 : f_error d z ≤ s0 / (Complex.abs z * (Complex.abs z).log)
e1 : f_error d (f' d c z) ≤ s1 / (b ^ (d - 1) - 1) / (Complex.abs z * (Complex.abs z).log)
e2 : iter_error d c (f' d c (f' d c z)) ≤ s2 / ((1 - (bb * b - 1)⁻¹) * bb) / (Complex.abs z * (Complex.abs z).log)
⊢ 0 ≤ Complex.abs z * (Complex.abs z).log
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b3 : (3:ℝ) ≤ 3^(d-1) := by
  calc (3:ℝ)^(d-1)
    _ ≥ 3^(2-1) := by bound
    _ = 3 := by norm_num
Proof state after:
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
b3 : 3 ≤ 3 ^ (d - 1)
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
b3 : 3 ≤ 3 ^ (d - 1)
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hb3 : (3:ℝ)^(d-1) = t3 at b3
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b2 : (2:ℝ) ≤ t3 - 1 := by linarith
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
b2 : 2 ≤ t3 - 1
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
b2 : 2 ≤ t3 - 1
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hb2 : t3 - 1 = t2 at b2
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have t2p : 0 ≤ t2 := by positivity
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b6 : (6:ℝ) ≤ t2 * 3 := by linarith
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b11 : (11:ℝ) ≤ t2^d * t3 - 1 := by
  calc t2^d * t3 - 1
    _ ≥ 2^d * 3 - 1 := by bound
    _ ≥ 2^2 * 3 - 1 := by bound
    _ = 11 := by norm_num
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t2 ^ d * t3 - 1
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t2 ^ d * t3 - 1
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hb11 : t2^d * t3 - 1 = t11 at b11
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b33 : (33:ℝ) ≤ t11 * 3 := by linarith
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
b33 : 33 ≤ t11 * 3
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
b33 : 33 ≤ t11 * 3
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hb33 : t11 * 3 = t33 at b33
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
t33 : ℝ
hb33 : t11 * 3 = t33
b33 : 33 ≤ t33
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
t33 : ℝ
hb33 : t11 * 3 = t33
b33 : 33 ≤ t33
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11 := by
  have h : 1 ≤ t33 - 1 := by linarith
  calc (1 - (t33 - 1)⁻¹) * t11
    _ ≥ (1 - (33 - 1)⁻¹) * 11 := by bound
    _ ≥ 10.65 := by norm_num
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
t33 : ℝ
hb33 : t11 * 3 = t33
b33 : 33 ≤ t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
t33 : ℝ
hb33 : t11 * 3 = t33
b33 : 33 ≤ t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
simp only [←hb2, ←hb3, ←hb11, ←hb33] at b2 b6 b11 b33
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ iter_error d c z ≤ 1.03 / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine iter_error_le _ (by norm_num) (by norm_num) (by norm_num)
  (bs0 := f_error_le_of_z3 d)
  (bs1 := fun {_} bz ↦ f_error_le_of_z6 d (le_trans b6 bz))
  (bs2 := fun {_} bz ↦ f_error_le_of_z33 d (le_trans b33 bz))
  b11 (le_trans (by norm_num) b33) (by positivity) ?_ ?_ z3 cz
Proof state after:
case refine_1
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ 0 < 1 - (((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3 - 1)⁻¹

case refine_2
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 3 = t33
b10 : 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 2 ≤ 3 ^ (d - 1) - 1
b6 : 6 ≤ (3 ^ (d - 1) - 1) * 3
b11 : 11 ≤ (3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1
b33 : 33 ≤ ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3
⊢ 0.699 + 0.565 / (3 ^ (d - 1) - 1) +
      0.512 /
        ((1 - (((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3 - 1)⁻¹) * ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1)) ≤
    1.03
Theorem: iter_error_le_of_z3
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
⊢ 3 ≤ 3 ^ (d - 1)
Tactic:
calc (3:ℝ)^(d-1)
  _ ≥ 3^(2-1) := by bound
  _ = 3 := by norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
⊢ 3 ^ (d - 1) ≥ 3 ^ (2 - 1)
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
⊢ 3 ^ (2 - 1) = 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
⊢ 2 ≤ t3 - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
⊢ 0 ≤ t2
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
⊢ 6 ≤ t2 * 3
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
⊢ 11 ≤ t2 ^ d * t3 - 1
Tactic:
calc t2^d * t3 - 1
  _ ≥ 2^d * 3 - 1 := by bound
  _ ≥ 2^2 * 3 - 1 := by bound
  _ = 11 := by norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
⊢ t2 ^ d * t3 - 1 ≥ 2 ^ d * 3 - 1
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
⊢ 2 ^ d * 3 - 1 ≥ 2 ^ 2 * 3 - 1
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
⊢ 2 ^ 2 * 3 - 1 = 11
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
⊢ 33 ≤ t11 * 3
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
t33 : ℝ
hb33 : t11 * 3 = t33
b33 : 33 ≤ t33
⊢ 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
Tactic:
have h : 1 ≤ t33 - 1 := by linarith
Proof state after:
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
t33 : ℝ
hb33 : t11 * 3 = t33
b33 : 33 ≤ t33
h : 1 ≤ t33 - 1
⊢ 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
t33 : ℝ
hb33 : t11 * 3 = t33
b33 : 33 ≤ t33
h : 1 ≤ t33 - 1
⊢ 10.65 ≤ (1 - (t33 - 1)⁻¹) * t11
Tactic:
calc (1 - (t33 - 1)⁻¹) * t11
  _ ≥ (1 - (33 - 1)⁻¹) * 11 := by bound
  _ ≥ 10.65 := by norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z3
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
t3 : ℝ
hb3 : 3 ^ (d - 1) = t3
b3 : 3 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 2 ≤ t2
t2p : 0 ≤ t2
b6 : 6 ≤ t2 * 3
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 11 ≤ t11
t33 : ℝ
hb33 : t11 * 3 = t33
b33 : 33 ≤ t33
⊢ 1 ≤ t33 - 1
Tactic:
linarith
Proof state after:
no goals