Theorem: iter_error_le_of_z3 (Ray/Dynamics/Multibrot/Iterates.lean)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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)

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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
⊢ (1 - (t33 - 1)⁻¹) * t11 ≥ (1 - (33 - 1)⁻¹) * 11
Tactic:
bound
State after:
no goals

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
⊢ (1 - (33 - 1)⁻¹) * 11 ≥ 10.65
Tactic:
norm_num
State after:
no goals

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
⊢ 3 ≤ 3
Tactic:
norm_num
State after:
no goals

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
⊢ 0 ≤ 0.565
Tactic:
norm_num
State after:
no goals

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
⊢ 0 ≤ 0.512
Tactic:
norm_num
State after:
no goals

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
⊢ 3 ≤ 33
Tactic:
norm_num
State after:
no goals

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
⊢ 0 < 3 ^ (d - 1) - 1
Tactic:
positivity
State after:
no goals

State before:
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)⁻¹
Tactic:
exact sub_pos.mpr (inv_lt_one (by linarith))
State after:
no goals

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
⊢ 1 < ((3 ^ (d - 1) - 1) ^ d * 3 ^ (d - 1) - 1) * 3 - 1
Tactic:
linarith
State after:
no goals

State before:
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
Tactic:
simp only [hb2, hb3, hb11, hb33] at b2 b3 b6 b11 b33 ⊢
State after:
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 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0.699 + 0.565 / t2 + 0.512 / ((1 - (t33 - 1)⁻¹) * t11) ≤ 1.03

State before:
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 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0.699 + 0.565 / t2 + 0.512 / ((1 - (t33 - 1)⁻¹) * t11) ≤ 1.03
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)
State after:
no goals

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 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0 ≤ 0.565
Tactic:
norm_num
State after:
no goals

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 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

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 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0 ≤ 0.512
Tactic:
norm_num
State after:
no goals

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 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0 < 10.65
Tactic:
norm_num
State after:
no goals

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 ≤ t2
b6 : 6 ≤ t2 * 3
b11 : 11 ≤ t11
b33 : 33 ≤ t33
⊢ 0.699 + 0.565 / 2 + 0.512 / 10.65 ≤ 1.03
Tactic:
norm_num
State after:
no goals