Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.residue_mul_eq_of_sub_principal_isBigO_one

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Foundations · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Foundations.lean:571 to 584

Mathematical statement

Exact Lean statement

lemma residue_mul_eq_of_sub_principal_isBigO_one
    {f Ψ : ℂ → ℂ} {p c : ℂ}
    (h : (f - fun z : ℂ => c / (z - p)) =O[𝓝[≠] p] (1 : ℂ → ℂ))
    (hΨ : ContinuousAt Ψ p) :
    residue (fun z : ℂ => f z * Ψ z) p = c * Ψ p

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma residue_mul_eq_of_sub_principal_isBigO_one    {f Ψ : ℂ → ℂ} {p c : ℂ}    (h : (f - fun z : ℂ => c / (z - p)) =O[𝓝[≠] p] (1 : ℂ → ℂ))    (hΨ : ContinuousAt Ψ p) :    residue (fun z : ℂ => f z * Ψ z) p = c * Ψ p := by  refine residue_eq_of_tendsto ?_  have hf := tendsto_mul_self_of_sub_principal_isBigO_one h  have hprod := hf.mul hΨ.continuousWithinAt.tendsto  have hcongr :      (fun z : ℂ => (z - p) * (f z * Ψ z)) =ᶠ[𝓝[≠] p]        fun z : ℂ => ((z - p) * f z) * Ψ z := by    filter_upwards with z    ring  simpa [mul_assoc] using hprod.congr' hcongr.symm