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

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ 0 ≤ f_error d z
Tactic:
rw [f_error, le_neg, neg_zero]
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0
Tactic:
have d0 : 0 < d := d_pos d
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0
Tactic:
have  l1 : 1 ≤ log (abs z) := le_trans (by norm_num) (le_log_abs_z z3)
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0
Tactic:
apply Real.log_nonpos
State after:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 ≤ 1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)

case h'x
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ 1

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
⊢ 1 ≤ 1.0986
Tactic:
norm_num
State after:
no goals

State before:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 ≤ 1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
simp only [one_div, neg_div, sub_nonneg, neg_le]
State after:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -1 ≤ (1 - (Complex.abs z)⁻¹).log / (↑d * (Complex.abs z).log)

State before:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -1 ≤ (1 - (Complex.abs z)⁻¹).log / (↑d * (Complex.abs z).log)
Tactic:
rw [le_div_iff (by positivity), neg_one_mul, neg_le]
State after:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ ↑d * (Complex.abs z).log

State before:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ ↑d * (Complex.abs z).log
Tactic:
trans 2
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ 2

c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 2 ≤ ↑d * (Complex.abs z).log

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 < ↑d * (Complex.abs z).log
Tactic:
positivity
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ 2
Tactic:
refine le_trans (neg_log_one_sub_le_linear (c := 2) (by positivity) (by norm_num) ?_) ?_
State after:
case refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (Complex.abs z)⁻¹ ≤ min 1 (((2 - 1) * 2)⁻¹ + 1)⁻¹

case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 2 * (Complex.abs z)⁻¹ ≤ 2

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 ≤ (Complex.abs z)⁻¹
Tactic:
positivity
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals

State before:
case refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (Complex.abs z)⁻¹ ≤ min 1 (((2 - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
exact le_trans (inv_le_inv_of_le (by positivity) z3) (by norm_num)
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 < 3
Tactic:
positivity
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 3⁻¹ ≤ min 1 (((2 - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
norm_num
State after:
no goals

State before:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 2 * (Complex.abs z)⁻¹ ≤ 2
Tactic:
simp only [zero_lt_two, mul_le_iff_le_one_right]
State after:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (Complex.abs z)⁻¹ ≤ 1

State before:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (Complex.abs z)⁻¹ ≤ 1
Tactic:
apply inv_le_one
State after:
case refine_2.ha
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 1 ≤ Complex.abs z

State before:
case refine_2.ha
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 1 ≤ Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 2 ≤ ↑d * (Complex.abs z).log
Tactic:
exact le_trans (by norm_num) (mul_le_mul (two_le_cast_d d) l1 zero_le_one (by positivity))
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 2 ≤ 2 * 1
Tactic:
norm_num
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 ≤ ↑d
Tactic:
positivity
State after:
no goals

State before:
case h'x
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ 1
Tactic:
linarith [f_error_inner_nonneg d z3]
State after:
no goals