Theorem: potential_error_le' (Ray/Dynamics/Multibrot/Potential.lean)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ i
Tactic:
have z0 : 0 < abs z := by linarith
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ i

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ i
Tactic:
have l1 : 1.386 < log (abs z) :=
  lt_of_lt_of_le lt_log_4 (Real.log_le_log (by linarith) (by linarith))
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ i

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ i
Tactic:
have l0 : 0 < log (abs z) := lt_trans (by norm_num) l1
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ i

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ i
Tactic:
refine le_trans (potential_error_le d b4 bz cz) (div_le_div_of_nonneg_left (by norm_num)
  (by positivity) ?_)
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ Complex.abs z ^ i ≤ Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ Complex.abs z ^ i ≤ Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
refine Real.rpow_le_rpow_of_exponent_le (by linarith) ?_
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ i ≤ 1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ i ≤ 1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp
Tactic:
simp only [add_comm (1:ℝ), ←sub_le_iff_le_add]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ i - 1 ≤ (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ i - 1 ≤ (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp
Tactic:
refine le_trans ij (Real.exp_le_exp.mpr ?_)
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ -j ≤ -0.8095 / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ -j ≤ -0.8095 / (Complex.abs z * (Complex.abs z).log)
Tactic:
simp only [neg_div, neg_le_neg_iff, div_mul_eq_div_div]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / (Complex.abs z).log ≤ j

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / (Complex.abs z).log ≤ j
Tactic:
rw [div_le_iff l0, mul_comm j, ←div_le_iff j0]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / j ≤ (Complex.abs z).log

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / j ≤ (Complex.abs z).log
Tactic:
trans 0.8095 / b / j
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / j ≤ 0.8095 / b / j

c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / b / j ≤ (Complex.abs z).log

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
⊢ 0 < Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
⊢ 0 < 4
Tactic:
linarith
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
⊢ 4 ≤ Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
⊢ 0 < 1.386
Tactic:
norm_num
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0 ≤ 0.8095
Tactic:
norm_num
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0 < Complex.abs z ^ i
Tactic:
positivity
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 1 ≤ Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / Complex.abs z / j ≤ 0.8095 / b / j
Tactic:
gcongr
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ 0.8095 / b / j ≤ (Complex.abs z).log
Tactic:
rw [Real.le_log_iff_exp_le z0]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ (0.8095 / b / j).exp ≤ Complex.abs z

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
i j b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
j0 : 0 < j
ij : i - 1 ≤ (-j).exp
bj : (0.8095 / b / j).exp ≤ b
z0 : 0 < Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ (0.8095 / b / j).exp ≤ Complex.abs z
Tactic:
exact le_trans bj bz
State after:
no goals