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

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ Tendsto (fun z => ⋯.potential c ↑z * Complex.abs z) atInf (𝓝 1)
Tactic:
set s := superF d
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun z => s.potential c ↑z * Complex.abs z) atInf (𝓝 1)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun z => s.potential c ↑z * Complex.abs z) atInf (𝓝 1)
Tactic:
simp only [← s.abs_bottcher, ← Complex.abs.map_mul, ← Complex.abs.map_one]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun z => Complex.abs (s.bottcher c ↑z * z)) atInf (𝓝 (Complex.abs 1))

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun z => Complex.abs (s.bottcher c ↑z * z)) atInf (𝓝 (Complex.abs 1))
Tactic:
exact Complex.continuous_abs.continuousAt.tendsto.comp (bottcher_large_approx d c)
State after:
no goals