Hopf problem: threefold · special periods 5

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.SpecialPeriods.TauCusp.exists_simplePole_normalized_limit_mo1973_17415 {Fc : ℂ → ℂ} (hFc : MeromorphicAt Fc 0) (horder : meromorphicOrderAt Fc 0 = ↑(-1)) : ∃ (c : ℂ), c ≠ 0 ∧ Filter.Tendsto (fun (t : ℂ) => t * Fc t) (nhdsWithin 0 {0}ᶜ) (nhds c)