internlm/Lean-Github huggingface dataset:
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
⊢ 3 ^ 2 * 4 - 1 = 35
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
⊢ 140 ≤ t11 * 4
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
t33 : ℝ
hb33 : t11 * 4 = t33
b33 : 140 ≤ t33
⊢ 34.748 ≤ (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 : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
t33 : ℝ
hb33 : t11 * 4 = t33
b33 : 140 ≤ t33
h : 1 ≤ t33 - 1
⊢ 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
t33 : ℝ
hb33 : t11 * 4 = t33
b33 : 140 ≤ t33
h : 1 ≤ t33 - 1
⊢ 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
Tactic:
calc (1 - (t33 - 1)⁻¹) * t11
  _ ≥ (1 - (140 - 1)⁻¹) * 35 := by bound
  _ ≥ 34.748 := by norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
t33 : ℝ
hb33 : t11 * 4 = t33
b33 : 140 ≤ t33
⊢ 1 ≤ t33 - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
t33 : ℝ
hb33 : t11 * 4 = t33
b33 : 140 ≤ t33
h : 1 ≤ t33 - 1
⊢ (1 - (t33 - 1)⁻¹) * t11 ≥ (1 - (140 - 1)⁻¹) * 35
Tactic:
bound
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
b2 : 3 ≤ t2
t2p : 0 ≤ t2
b6 : 12 ≤ t2 * 4
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
b11 : 35 ≤ t11
t33 : ℝ
hb33 : t11 * 4 = t33
b33 : 140 ≤ t33
h : 1 ≤ t33 - 1
⊢ (1 - (140 - 1)⁻¹) * 35 ≥ 34.748
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 3 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 0 ≤ 0.528
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 0 ≤ 0.5023
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 11 ≤ 35
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 3 ≤ 140
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 0 < 4 ^ (d - 1) - 1
Tactic:
positivity
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 0 < 1 - (((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4 - 1)⁻¹
Tactic:
exact sub_pos.mpr (inv_lt_one (by linarith))
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 1 < ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4 - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ 4 ^ (d - 1) - 1
b6 : 12 ≤ (4 ^ (d - 1) - 1) * 4
b11 : 35 ≤ (4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1
b33 : 140 ≤ ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4
⊢ 0.619 + 0.528 / (4 ^ (d - 1) - 1) +
      0.5023 /
        ((1 - (((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1) * 4 - 1)⁻¹) * ((4 ^ (d - 1) - 1) ^ d * 4 ^ (d - 1) - 1)) ≤
    0.8095
Tactic:
simp only [hb2, hb3, hb11, hb33] at b2 b3 b6 b11 b33 ⊢
Proof state after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ t2
b6 : 12 ≤ t2 * 4
b11 : 35 ≤ t11
b33 : 140 ≤ t33
⊢ 0.619 + 0.528 / t2 + 0.5023 / ((1 - (t33 - 1)⁻¹) * t11) ≤ 0.8095
Theorem: iter_error_le_of_z4
Proof state before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ t2
b6 : 12 ≤ t2 * 4
b11 : 35 ≤ t11
b33 : 140 ≤ t33
⊢ 0.619 + 0.528 / t2 + 0.5023 / ((1 - (t33 - 1)⁻¹) * t11) ≤ 0.8095
Tactic:
exact le_trans (add_le_add (add_le_add_left
  (div_le_div_of_nonneg_left (by norm_num) (by norm_num) b2) _)
  (div_le_div_of_nonneg_left (by norm_num) (by norm_num) b10)) (by norm_num)
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ t2
b6 : 12 ≤ t2 * 4
b11 : 35 ≤ t11
b33 : 140 ≤ t33
⊢ 0 ≤ 0.528
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ t2
b6 : 12 ≤ t2 * 4
b11 : 35 ≤ t11
b33 : 140 ≤ t33
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ t2
b6 : 12 ≤ t2 * 4
b11 : 35 ≤ t11
b33 : 140 ≤ t33
⊢ 0 ≤ 0.5023
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ t2
b6 : 12 ≤ t2 * 4
b11 : 35 ≤ t11
b33 : 140 ≤ t33
⊢ 0 < 34.748
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_error_le_of_z4
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z4 : 4 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
t3 : ℝ
hb3 : 4 ^ (d - 1) = t3
b3 : 4 ≤ t3
t2 : ℝ
hb2 : t3 - 1 = t2
t2p : 0 ≤ t2
t11 : ℝ
hb11 : t2 ^ d * t3 - 1 = t11
t33 : ℝ
hb33 : t11 * 4 = t33
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
b2 : 3 ≤ t2
b6 : 12 ≤ t2 * 4
b11 : 35 ≤ t11
b33 : 140 ≤ t33
⊢ 0.619 + 0.528 / 3 + 0.5023 / 34.748 ≤ 0.8095
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
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have dp : 0 < d := d_pos d
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have d2 : 2 ≤ (d : ℝ) := two_le_cast_d d
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have z1' : 1 < abs z := lt_of_lt_of_le (by norm_num) z3
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
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have z0' : 0 < abs z := by positivity
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
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have iz1 : 1 / abs z < 1 := (div_lt_one z0').mpr z1'
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
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have z0 : z ≠ 0 := Complex.abs.ne_zero_iff.mp (by positivity)
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
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have cz_le : abs (c / z ^ d) ≤ 1 / abs z := by
  have d1 : z^d = z^(d - 1 + 1) := by rw [Nat.sub_add_cancel (d_ge_one d)]
  simp only [d1, map_div₀, Complex.abs.map_pow, pow_succ', Complex.abs.map_mul,
    div_mul_eq_div_div]
  bound
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
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l0s : 1 ≤ log (abs z) := by
  rw [Real.le_log_iff_exp_le z0']; exact le_trans Real.exp_one_lt_3.le z3
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
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l0 : 0 < log (abs z) := by positivity
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
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l1 : 0 < ↑d * log (abs z) := by positivity
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
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l1' : 1 < log (abs z) := by
  rw [Real.lt_log_iff_exp_lt z0']; exact lt_of_lt_of_le Real.exp_one_lt_3 z3
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have l2 : |log (abs (1 + c / z ^ d))| ≤ -log (1 - 1 / abs z) := by
  nth_rw 1 [← Complex.log_re]
  apply le_trans (Complex.abs_re_le_abs _)
  apply le_trans (Complex.abs_log_one_add_le (trans cz_le iz1))
  exact Real.neg_log_one_sub_mono cz_le iz1
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Theorem: f_approx
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
dp : 0 < d
d2 : 2 ≤ ↑d
z1' : 1 < Complex.abs z
z0' : 0 < Complex.abs z
iz1 : 1 / Complex.abs z < 1
z0 : z ≠ 0
cz_le : Complex.abs (c / z ^ d) ≤ 1 / Complex.abs z
l0s : 1 ≤ (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
l1 : 0 < ↑d * (Complex.abs z).log
l1' : 1 < (Complex.abs z).log
l2 : |(Complex.abs (1 + c / z ^ d)).log| ≤ -(1 - 1 / Complex.abs z).log
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z
Tactic:
have dl2 : 2 < d * log (abs z) := by
  calc ↑d * log (abs z)
    _ ≥ 2 * log (abs z) := by gcongr
    _ > 2 * 1 := by gcongr
    _ = 2 := by norm_num
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
⊢ |(Complex.abs (z ^ d + c)).log.log - (Complex.abs z).log.log - (↑d).log| ≤ f_error d z