Theorem: potential_error_le_of_z6 (Ray/Dynamics/Multibrot/Potential.lean)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ 1.927
Tactic:
apply potential_error_le' d _ (j := 0.0753) (b := 6) (by norm_num) z6 cz (by norm_num)
State after:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1.927 - 1 ≤ (-753e-4).exp

case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (0.8095 / 6 / 753e-4).exp ≤ 6

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 4 ≤ 6
Tactic:
norm_num
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < 753e-4
Tactic:
norm_num
State after:
no goals

State before:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1.927 - 1 ≤ (-753e-4).exp
Tactic:
norm_num
State after:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 927 / 1000 ≤ (-(753 / 10000)).exp

State before:
case ij
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 927 / 1000 ≤ (-(753 / 10000)).exp
Tactic:
exact (lt_exp_neg_div).le
State after:
no goals

State before:
case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (0.8095 / 6 / 753e-4).exp ≤ 6
Tactic:
norm_num
State after:
case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (8095 / 4518).exp ≤ 6

State before:
case bj
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z6 : 6 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (8095 / 4518).exp ≤ 6
Tactic:
exact (exp_div_lt).le
State after:
no goals