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

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
have z3 : 3 ≤ abs z := by linarith
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
have l0 : 0 < log (abs z) := lt_of_lt_of_le (by norm_num) (le_log_abs_z z3)
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b1 : 1 < b - 1 := by linarith
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
have b0 : 0 ≤ 1 - (b - 1)⁻¹ := sub_nonneg.mpr (inv_le_one b1.le)
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ iter_error d c z ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine tsum_le_of_sum_le' ?_ ?_
State after:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ 0 ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)

case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ ∀ (s_1 : Finset ℕ),
    (s_1.sum fun i => f_error d ((f' d c)^[i] z)) ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 3 ≤ Complex.abs z
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ 0 < 1.0986
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
⊢ 1 < b - 1
Tactic:
linarith
State after:
no goals

State before:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ 0 ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
positivity
State after:
no goals

State before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
⊢ ∀ (s_1 : Finset ℕ),
    (s_1.sum fun i => f_error d ((f' d c)^[i] z)) ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
intro N
State after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
N : Finset ℕ
⊢ (N.sum fun i => f_error d ((f' d c)^[i] z)) ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)

State before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b s : ℝ
c : ℂ
b3 : 3 ≤ b
s0 : 0 ≤ s
bs : ∀ {w : ℂ}, b ≤ Complex.abs w → f_error d w ≤ s / (Complex.abs w * (Complex.abs w).log)
z : ℂ
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
l0 : 0 < (Complex.abs z).log
b1 : 1 < b - 1
b0 : 0 ≤ 1 - (b - 1)⁻¹
N : Finset ℕ
⊢ (N.sum fun i => f_error d ((f' d c)^[i] z)) ≤ s / (1 - (b - 1)⁻¹) / (Complex.abs z * (Complex.abs z).log)
Tactic:
exact iter_error_sum_weak d b3 s0 bs bz cz
State after:
no goals