Complex limits at infinity #
If z * ψ z has a finite limit along a filter approaching infinity, then ψ z tends to zero.
theorem
TauCeti.tendsto_zero_of_tendsto_mul_cobounded
{l : Filter ℂ}
(hl : l ≤ Bornology.cobounded ℂ)
{ψ : ℂ → ℂ}
{c : ℂ}
(h : Filter.Tendsto (fun (z : ℂ) => z * ψ z) l (nhds c))
:
Filter.Tendsto ψ l (nhds 0)
If z * ψ z has a finite limit at infinity, then ψ z tends to zero.