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

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

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
have z0' : z ≠ 0 := by exact nnnorm_pos.mp z0
State after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
have i1 : 1 / abs z ≤ 1 := by rw [one_div_le z0]; exact le_trans (by norm_num) z3; norm_num
State after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
have s1 : 1 - 1 / abs z < 1 := by rw [tsub_lt_iff_tsub_lt]; norm_num; exact z0'; exact i1; rfl
State after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
s1 : 1 - 1 / Complex.abs z < 1
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
s1 : 1 - 1 / Complex.abs z < 1
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
have l1 := le_log_abs_z z3
State after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
s1 : 1 - 1 / Complex.abs z < 1
l1 : 1.0986 ≤ (Complex.abs z).log
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
s1 : 1 - 1 / Complex.abs z < 1
l1 : 1.0986 ≤ (Complex.abs z).log
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
exact div_nonneg (neg_nonneg.mpr (Real.log_nonpos (sub_nonneg.mpr i1) s1.le)) (by positivity)
State after:
no goals

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

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
⊢ z ≠ 0
Tactic:
exact nnnorm_pos.mp z0
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 1 / Complex.abs z ≤ 1
Tactic:
rw [one_div_le z0]
State after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 1 / 1 ≤ Complex.abs z

c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 < 1

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 1 / 1 ≤ Complex.abs z

c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 < 1
Tactic:
exact le_trans (by norm_num) z3
State after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 < 1

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

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

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 - 1 / Complex.abs z < 1
Tactic:
rw [tsub_lt_iff_tsub_lt]
State after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 - 1 < 1 / Complex.abs z

case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 - 1 < 1 / Complex.abs z

case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Tactic:
norm_num
State after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ ¬z = 0

case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ ¬z = 0

case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Tactic:
exact z0'
State after:
case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1

State before:
case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Tactic:
exact i1
State after:
case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1

State before:
case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Tactic:
rfl
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
s1 : 1 - 1 / Complex.abs z < 1
l1 : 1.0986 ≤ (Complex.abs z).log
⊢ 0 ≤ ↑d * (Complex.abs z).log
Tactic:
positivity
State after:
no goals