Germ packaging of meromorphic functions (residue-calculus)

RS.meromorphicGermsAt z₀ is the ℂ-submodule of germs at 𝓝[≠] z₀ that are meromorphic; RS.laurentCoeffL z₀ k and RS.resL z₀ package laurentCoeffAt/resAt as ℂ-linear functionals on it — the currency for laurent-tails (CC8) and serre-duality-cech/tails.

Main exports: RS.MeromorphicGerm, RS.meromorphicGermsAt, RS.laurentCoeffL, RS.resL, RS.laurentCoeffL_mk.

def RS.MeromorphicGerm (z₀ : ℂ) (γ : (nhdsWithin z₀ {z₀}ᶜ).Germ ℂ) : Prop

Meromorphy is a property of the punctured germ.

Equations

• RS.MeromorphicGerm z₀ γ = γ.liftOn (fun (x : ℂ → ℂ) => MeromorphicAt x z₀) ⋯

@[simp]

theorem RS.meromorphicGerm_coe {z₀ : ℂ} {f : ℂ → ℂ} : MeromorphicGerm z₀ ↑f ↔ MeromorphicAt f z₀

def RS.meromorphicGermsAt (z₀ : ℂ) : Submodule ℂ ((nhdsWithin z₀ {z₀}ᶜ).Germ ℂ)

The ℂ-space of meromorphic germs at z₀ (a submodule of the full germ module).

Equations

• RS.meromorphicGermsAt z₀ = { carrier := {γ : (nhdsWithin z₀ {z₀}ᶜ).Germ ℂ | RS.MeromorphicGerm z₀ γ}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem RS.mem_meromorphicGermsAt {z₀ : ℂ} {f : ℂ → ℂ} : ↑f ∈ meromorphicGermsAt z₀ ↔ MeromorphicAt f z₀

noncomputable def RS.laurentCoeffL (z₀ : ℂ) (k : ℤ) : ↥(meromorphicGermsAt z₀) →ₗ[ℂ] ℂ

Laurent coefficients as ℂ-linear functionals on meromorphic germs.

Equations

• RS.laurentCoeffL z₀ k = { toFun := fun (γ : ↥(RS.meromorphicGermsAt z₀)) => (↑γ).liftOn (fun (x : ℂ → ℂ) => RS.laurentCoeffAt x z₀ k) ⋯, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def RS.resL (z₀ : ℂ) : ↥(meromorphicGermsAt z₀) →ₗ[ℂ] ℂ

The residue functional.

Equations

• RS.resL z₀ = RS.laurentCoeffL z₀ (-1)

@[simp]

theorem RS.laurentCoeffL_mk {z₀ : ℂ} {f : ℂ → ℂ} (hf : MeromorphicAt f z₀) (k : ℤ) : (laurentCoeffL z₀ k) ⟨↑f, hf⟩ = laurentCoeffAt f z₀ k