Theorem: bottcher_tendsto_zero (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Tendsto (bottcher' d) atInf (𝓝 0)
Tactic:
rw [Metric.tendsto_nhds]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ ε > 0, ∀ᶠ (x : ℂ) in atInf, dist (bottcher' d x) 0 < ε

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ ε > 0, ∀ᶠ (x : ℂ) in atInf, dist (bottcher' d x) 0 < ε
Tactic:
intro r rp
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∀ᶠ (x : ℂ) in atInf, dist (bottcher' d x) 0 < r

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∀ᶠ (x : ℂ) in atInf, dist (bottcher' d x) 0 < r
Tactic:
rw [atInf_basis.eventually_iff]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∃ i, True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | i < ‖x‖} → dist (bottcher' d x) 0 < r

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∃ i, True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | i < ‖x‖} → dist (bottcher' d x) 0 < r
Tactic:
use max 16 (3 / r)
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | max 16 (3 / r) < ‖x‖} → dist (bottcher' d x) 0 < r

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | max 16 (3 / r) < ‖x‖} → dist (bottcher' d x) 0 < r
Tactic:
simp only [true_and_iff, mem_setOf, Complex.dist_eq, sub_zero, Complex.norm_eq_abs, max_lt_iff]
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∀ ⦃x : ℂ⦄, 16 < Complex.abs x ∧ 3 / r < Complex.abs x → Complex.abs (bottcher' d x) < r

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∀ ⦃x : ℂ⦄, 16 < Complex.abs x ∧ 3 / r < Complex.abs x → Complex.abs (bottcher' d x) < r
Tactic:
intro z ⟨lo, rz⟩
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 / r < Complex.abs z
⊢ Complex.abs (bottcher' d z) < r

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 / r < Complex.abs z
⊢ Complex.abs (bottcher' d z) < r
Tactic:
apply lt_of_le_of_lt (bottcher_bound lo)
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 / r < Complex.abs z
⊢ 3 * Complex.abs z⁻¹ < r

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 / r < Complex.abs z
⊢ 3 * Complex.abs z⁻¹ < r
Tactic:
rw [div_lt_iff rp] at rz
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 < Complex.abs z * r
⊢ 3 * Complex.abs z⁻¹ < r

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 < Complex.abs z * r
⊢ 3 * Complex.abs z⁻¹ < r
Tactic:
rw [map_inv₀, mul_inv_lt_iff (lt_trans (by norm_num) lo)]
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 < Complex.abs z * r
⊢ 3 < Complex.abs z * r

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 < Complex.abs z * r
⊢ 3 < Complex.abs z * r
Tactic:
exact rz
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 < Complex.abs z * r
⊢ 0 < 16
Tactic:
norm_num
State after:
no goals