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

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
have z1 : 1 < abs z := by linarith
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / 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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
have z4 : 4 ≤ abs z := by linarith
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / 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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
have l1 : 1.386 < log (abs z) := lt_of_lt_of_le lt_log_4 (Real.log_le_log (by linarith) z4)
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
⊢ potential_error d c z ≤ 0.8095 / 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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
⊢ potential_error d c z ≤ 0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ 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 ^ (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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ 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 ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
simp only [potential_error, dene_eq z1]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ (-iter_error d c z).exp * (Complex.abs z).log * Complex.abs z ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    0.8095 / 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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
⊢ (-iter_error d c z).exp * (Complex.abs z).log * Complex.abs z ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
have ie := iter_error_le_of_z4 d z4 cz
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie : iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
⊢ (-iter_error d c z).exp * (Complex.abs z).log * Complex.abs z ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    0.8095 / 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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie : iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
⊢ (-iter_error d c z).exp * (Complex.abs z).log * Complex.abs z ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
have ie0 := iter_error_nonneg d (by linarith) cz
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie : iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
ie0 : 0 ≤ iter_error d c z
⊢ (-iter_error d c z).exp * (Complex.abs z).log * Complex.abs z ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    0.8095 / 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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie : iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
ie0 : 0 ≤ iter_error d c z
⊢ (-iter_error d c z).exp * (Complex.abs z).log * Complex.abs z ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    0.8095 / Complex.abs z ^ (1 + (-0.8095 / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
generalize hk : (0.8095 : ℝ) = k at ie
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie0 : 0 ≤ iter_error d c z
k : ℝ
hk : 0.8095 = k
ie : iter_error d c z ≤ k / (Complex.abs z * (Complex.abs z).log)
⊢ (-iter_error d c z).exp * (Complex.abs z).log * Complex.abs z ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    k / Complex.abs z ^ (1 + (-k / (Complex.abs z * (Complex.abs z).log)).exp)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie0 : 0 ≤ iter_error d c z
k : ℝ
hk : 0.8095 = k
ie : iter_error d c z ≤ k / (Complex.abs z * (Complex.abs z).log)
⊢ (-iter_error d c z).exp * (Complex.abs z).log * Complex.abs z ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    k / Complex.abs z ^ (1 + (-k / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
have k0 : 0 < k := by rw [← hk]; norm_num
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie0 : 0 ≤ iter_error d c z
k : ℝ
hk : 0.8095 = k
ie : iter_error d c z ≤ k / (Complex.abs z * (Complex.abs z).log)
k0 : 0 < k
⊢ (-iter_error d c z).exp * (Complex.abs z).log * Complex.abs z ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    k / Complex.abs z ^ (1 + (-k / (Complex.abs z * (Complex.abs z).log)).exp)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie0 : 0 ≤ iter_error d c z
k : ℝ
hk : 0.8095 = k
ie : iter_error d c z ≤ k / (Complex.abs z * (Complex.abs z).log)
k0 : 0 < k
⊢ (-iter_error d c z).exp * (Complex.abs z).log * Complex.abs z ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    k / Complex.abs z ^ (1 + (-k / (Complex.abs z * (Complex.abs z).log)).exp)
Tactic:
generalize hx : abs z = x at ie z1 l0 l1 z4
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
ie0 : 0 ≤ iter_error d c z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
ie : iter_error d c z ≤ k / (x * x.log)
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
⊢ (-iter_error d c z).exp * x.log * x ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    k / x ^ (1 + (-k / (x * x.log)).exp)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
ie0 : 0 ≤ iter_error d c z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
ie : iter_error d c z ≤ k / (x * x.log)
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
⊢ (-iter_error d c z).exp * x.log * x ^ (-(-iter_error d c z).exp) * iter_error d c z ≤
    k / x ^ (1 + (-k / (x * x.log)).exp)
Tactic:
generalize iter_error d c z = i at ie ie0
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
⊢ (-i).exp * x.log * x ^ (-(-i).exp) * i ≤ k / x ^ (1 + (-k / (x * x.log)).exp)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
⊢ (-i).exp * x.log * x ^ (-(-i).exp) * i ≤ k / x ^ (1 + (-k / (x * x.log)).exp)
Tactic:
have x0 : 0 < x := by rw [←hx]; linarith
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ (-i).exp * x.log * x ^ (-(-i).exp) * i ≤ k / x ^ (1 + (-k / (x * x.log)).exp)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ (-i).exp * x.log * x ^ (-(-i).exp) * i ≤ k / x ^ (1 + (-k / (x * x.log)).exp)
Tactic:
refine le_trans (mul_le_mul_of_nonneg_left ie (by positivity)) ?_
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ (-i).exp * x.log * x ^ (-(-i).exp) * (k / (x * x.log)) ≤ k / x ^ (1 + (-k / (x * x.log)).exp)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ (-i).exp * x.log * x ^ (-(-i).exp) * (k / (x * x.log)) ≤ k / x ^ (1 + (-k / (x * x.log)).exp)
Tactic:
simp only [←mul_assoc, div_eq_inv_mul, mul_inv, mul_comm _ (log x)]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ x.log * (-i).exp * x ^ (-(-i).exp) * x.log⁻¹ * x⁻¹ * k ≤ (x ^ (1 + (x.log⁻¹ * x⁻¹ * -k).exp))⁻¹ * k

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ x.log * (-i).exp * x ^ (-(-i).exp) * x.log⁻¹ * x⁻¹ * k ≤ (x ^ (1 + (x.log⁻¹ * x⁻¹ * -k).exp))⁻¹ * k
Tactic:
simp only [←mul_assoc, mul_comm _ (log x)⁻¹, inv_mul_cancel l0.ne', one_mul]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ (-i).exp * x ^ (-(-i).exp) * x⁻¹ * k ≤ (x ^ (1 + (x.log⁻¹ * x⁻¹ * -k).exp))⁻¹ * k

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ (-i).exp * x ^ (-(-i).exp) * x⁻¹ * k ≤ (x ^ (1 + (x.log⁻¹ * x⁻¹ * -k).exp))⁻¹ * k
Tactic:
simp only [mul_assoc]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ (-i).exp * (x ^ (-(-i).exp) * (x⁻¹ * k)) ≤ (x ^ (1 + (x.log⁻¹ * (x⁻¹ * -k)).exp))⁻¹ * k

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ (-i).exp * (x ^ (-(-i).exp) * (x⁻¹ * k)) ≤ (x ^ (1 + (x.log⁻¹ * (x⁻¹ * -k)).exp))⁻¹ * k
Tactic:
refine le_trans (mul_le_of_le_one_left (by positivity) (Real.exp_le_one_iff.mpr (by linarith))) ?_
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ x ^ (-(-i).exp) * (x⁻¹ * k) ≤ (x ^ (1 + (x.log⁻¹ * (x⁻¹ * -k)).exp))⁻¹ * k

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ x ^ (-(-i).exp) * (x⁻¹ * k) ≤ (x ^ (1 + (x.log⁻¹ * (x⁻¹ * -k)).exp))⁻¹ * k
Tactic:
simp only [←mul_assoc, ←Real.rpow_neg_one x, ←Real.rpow_add (lt_trans zero_lt_one z1),
  ←Real.rpow_neg x0.le]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ x ^ (-(-i).exp + -1) * k ≤ x ^ (-(1 + (x.log⁻¹ * x ^ (-1) * -k).exp)) * k

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ x ^ (-(-i).exp + -1) * k ≤ x ^ (-(1 + (x.log⁻¹ * x ^ (-1) * -k).exp)) * k
Tactic:
refine mul_le_mul_of_nonneg_right (Real.rpow_le_rpow_of_exponent_le z1.le ?_) k0.le
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ -(-i).exp + -1 ≤ -(1 + (x.log⁻¹ * x ^ (-1) * -k).exp)

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ -(-i).exp + -1 ≤ -(1 + (x.log⁻¹ * x ^ (-1) * -k).exp)
Tactic:
simp only [Real.rpow_neg_one, mul_neg, neg_add_rev, le_add_neg_iff_add_le, neg_add_cancel_right,
  neg_le_neg_iff, Real.exp_le_exp, ←mul_inv, ←div_eq_inv_mul k, mul_comm _ x, ie]
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1 < Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < 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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ 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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ 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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie : iter_error d c z ≤ 0.8095 / (Complex.abs z * (Complex.abs z).log)
⊢ 3 ≤ Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie0 : 0 ≤ iter_error d c z
k : ℝ
hk : 0.8095 = k
ie : iter_error d c z ≤ k / (Complex.abs z * (Complex.abs z).log)
⊢ 0 < k
Tactic:
rw [← hk]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie0 : 0 ≤ iter_error d c z
k : ℝ
hk : 0.8095 = k
ie : iter_error d c z ≤ k / (Complex.abs z * (Complex.abs z).log)
⊢ 0 < 0.8095

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z1 : 1 < Complex.abs z
z4 : 4 ≤ Complex.abs z
l1 : 1.386 < (Complex.abs z).log
l0 : 0 < (Complex.abs z).log
ie0 : 0 ≤ iter_error d c z
k : ℝ
hk : 0.8095 = k
ie : iter_error d c z ≤ k / (Complex.abs z * (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)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
⊢ 0 < x
Tactic:
rw [←hx]
State after:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
⊢ 0 < Complex.abs z

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
⊢ 0 < Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ 0 ≤ (-i).exp * x.log * x ^ (-(-i).exp)
Tactic:
positivity
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ 0 ≤ x ^ (-(-i).exp) * (x⁻¹ * k)
Tactic:
positivity
State after:
no goals

State before:
c✝ z✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b4 : 4 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
k : ℝ
hk : 0.8095 = k
k0 : 0 < k
x : ℝ
hx : Complex.abs z = x
z1 : 1 < x
l0 : 0 < x.log
l1 : 1.386 < x.log
z4 : 4 ≤ x
i : ℝ
ie : i ≤ k / (x * x.log)
ie0 : 0 ≤ i
x0 : 0 < x
⊢ -i ≤ 0
Tactic:
linarith
State after:
no goals