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

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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b3 : (4:ℝ) ≤ 4^(d-1) := by
  calc (4:ℝ)^(d-1)
    _ ≥ 4^(2-1) := by bound
    _ = 4 := by norm_num
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
b3 : 4 ≤ 4 ^ (d - 1)
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
b3 : 4 ≤ 4 ^ (d - 1)
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hb3 : (4:ℝ)^(d-1) = t3 at b3
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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b2 : (3:ℝ) ≤ t3 - 1 := by linarith
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
b2 : 3 ≤ t3 - 1
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
b2 : 3 ≤ t3 - 1
⊢ iter_error d c z ≤ 0.8095 / (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 : ℂ
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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
⊢ iter_error d c z ≤ 0.8095 / (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 : ℂ
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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b6 : (12:ℝ) ≤ t2 * 4 := by linarith
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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b11 : (35:ℝ) ≤ t2^d * t3 - 1 := by
  calc t2^d * t3 - 1
    _ ≥ 3^d * 4 - 1 := by bound
    _ ≥ 3^2 * 4 - 1 := by bound
    _ = 35 := by norm_num
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
b11 : 35 ≤ t2 ^ d * t3 - 1
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
b11 : 35 ≤ t2 ^ d * t3 - 1
⊢ iter_error d c z ≤ 0.8095 / (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 : ℂ
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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b33 : (140:ℝ) ≤ t11 * 4 := by linarith
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
b33 : 140 ≤ t11 * 4
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
b33 : 140 ≤ t11 * 4
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
generalize hb33 : t11 * 4 = t33 at b33
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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11 := by
  have h : 1 ≤ t33 - 1 := by linarith
  calc (1 - (t33 - 1)⁻¹) * t11
    _ ≥ (1 - (140 - 1)⁻¹) * 35 := by bound
    _ ≥ 34.748 := by norm_num
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
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
b10 : 34.748 ≤ (1 - (t33 - 1)⁻¹) * t11
⊢ iter_error d c z ≤ 0.8095 / (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 : ℂ
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
⊢ iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)

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
⊢ iter_error d c z ≤ 0.8095 / (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_z4 d)
  (bs1 := fun {_} bz ↦ f_error_le_of_z12 d (le_trans b6 bz))
  (bs2 := fun {_} bz ↦ f_error_le_of_z140 d (le_trans b33 bz))
  (le_trans (by norm_num) b11) (le_trans (by norm_num) b33) (by positivity) ?_ ?_ z4 cz
State after:
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)⁻¹

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

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
⊢ 4 ≤ 4 ^ (d - 1)
Tactic:
calc (4:ℝ)^(d-1)
  _ ≥ 4^(2-1) := by bound
  _ = 4 := by norm_num
State after:
no goals

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
⊢ 4 ^ (d - 1) ≥ 4 ^ (2 - 1)
Tactic:
bound
State after:
no goals

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
⊢ 4 ^ (2 - 1) = 4
Tactic:
norm_num
State after:
no goals

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

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

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
⊢ 12 ≤ t2 * 4
Tactic:
linarith
State after:
no goals

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
⊢ 35 ≤ t2 ^ d * t3 - 1
Tactic:
calc t2^d * t3 - 1
  _ ≥ 3^d * 4 - 1 := by bound
  _ ≥ 3^2 * 4 - 1 := by bound
  _ = 35 := by norm_num
State after:
no goals

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
⊢ t2 ^ d * t3 - 1 ≥ 3 ^ d * 4 - 1
Tactic:
bound
State after:
no goals

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 ^ d * 4 - 1 ≥ 3 ^ 2 * 4 - 1
Tactic:
bound
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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