Mittag-Leffler principal-part distributions (residue-calculus)

RS.PrincipalPartData U is a Mittag-Leffler datum: at finitely many points of U ⊆ ℂ, a finite tail of negative-exponent Laurent coefficients. Implemented as a Submodule ℂ (ℂ → (ℤ →₀ ℂ)) subtype (so the AddCommGroup/Module ℂ structure comes for free), with named accessors coeff/coeff_neg/mem_of_ne_zero/finite_support matching the design's structure fields.

RS.PrincipalPartData.Realizes f D says f is meromorphic on U with exactly the principal parts D. RS.PrincipalPartData.ofMeromorphicOn extracts the datum from a meromorphic function with finitely many poles on U.

Main exports: RS.PrincipalPartData, RS.PrincipalPartData.Realizes, RS.PrincipalPartData.toFun, RS.PrincipalPartData.totalRes, RS.PrincipalPartData.ofMeromorphicOn, RS.PrincipalPartData.realizes_ofMeromorphicOn, RS.PrincipalPartData.Realizes.add, RS.PrincipalPartData.Realizes.smul, RS.PrincipalPartData.Realizes.sub_orderAt_nonneg, RS.PrincipalPartData.realizes_zero_iff.

Semi-frozen (per the design doc): laurent-tails' designer may extend, not change, this interface.

def RS.principalPartCarrier (U : Set ℂ) : Submodule ℂ (ℂ → ℤ →₀ ℂ)

The underlying submodule of coefficient assignments: pure principal parts (negative exponents only), supported in U, with finitely many nonzero points.

Equations

• One or more equations did not get rendered due to their size.

def RS.PrincipalPartData (U : Set ℂ) : Type

A Mittag-Leffler datum of principal parts on U ⊆ ℂ: at finitely many points, a finite tail of negative-exponent Laurent coefficients.

Equations

• RS.PrincipalPartData U = ↥(RS.principalPartCarrier U)

@[instance_reducible]

noncomputable instance RS.PrincipalPartData.instAddCommGroup {U : Set ℂ} : AddCommGroup (PrincipalPartData U)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RS.PrincipalPartData.instModuleComplex {U : Set ℂ} : Module ℂ (PrincipalPartData U)

Equations

• RS.PrincipalPartData.instModuleComplex = { smul := RS.PrincipalPartData.instModuleComplex._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

def RS.PrincipalPartData.coeff {U : Set ℂ} (D : PrincipalPartData U) : ℂ → ℤ →₀ ℂ

Coefficient tail at each point.

Equations

• D.coeff = ↑D

theorem RS.PrincipalPartData.coeff_neg {U : Set ℂ} (D : PrincipalPartData U) (p : ℂ) (k : ℤ) : k ∈ (D.coeff p).support → k < 0

theorem RS.PrincipalPartData.mem_of_ne_zero {U : Set ℂ} (D : PrincipalPartData U) (p : ℂ) : D.coeff p ≠ 0 → p ∈ U

theorem RS.PrincipalPartData.finite_support {U : Set ℂ} (D : PrincipalPartData U) : {p : ℂ | D.coeff p ≠ 0}.Finite

def RS.PrincipalPartData.mk' {U : Set ℂ} (coeff : ℂ → ℤ →₀ ℂ) (coeff_neg : ∀ (p : ℂ), ∀ k ∈ (coeff p).support, k < 0) (mem_of_ne_zero : ∀ (p : ℂ), coeff p ≠ 0 → p ∈ U) (finite_support : {p : ℂ | coeff p ≠ 0}.Finite) : PrincipalPartData U

Constructor matching the structure-literal API.

Equations

• RS.PrincipalPartData.mk' coeff coeff_neg mem_of_ne_zero finite_support = ⟨coeff, ⋯⟩

@[simp]

theorem RS.PrincipalPartData.coeff_mk' {U : Set ℂ} (coeff : ℂ → ℤ →₀ ℂ) (coeff_neg : ∀ (p : ℂ), ∀ k ∈ (coeff p).support, k < 0) (mem_of_ne_zero : ∀ (p : ℂ), coeff p ≠ 0 → p ∈ U) (finite_support : {p : ℂ | coeff p ≠ 0}.Finite) : (mk' coeff coeff_neg mem_of_ne_zero finite_support).coeff = coeff

@[simp]

theorem RS.PrincipalPartData.coeff_zero {U : Set ℂ} : coeff 0 = 0

@[simp]

theorem RS.PrincipalPartData.coeff_add {U : Set ℂ} (D E : PrincipalPartData U) : (D + E).coeff = D.coeff + E.coeff

@[simp]

theorem RS.PrincipalPartData.coeff_neg_fun {U : Set ℂ} (D : PrincipalPartData U) : (-D).coeff = -D.coeff

@[simp]

theorem RS.PrincipalPartData.coeff_smul {U : Set ℂ} (c : ℂ) (D : PrincipalPartData U) : (c • D).coeff = c • D.coeff

def RS.PrincipalPartData.Realizes {U : Set ℂ} (f : ℂ → ℂ) (D : PrincipalPartData U) : Prop

f realizes the datum on U: meromorphic with exactly these principal parts.

Equations

• RS.PrincipalPartData.Realizes f D = (MeromorphicOn f U ∧ ∀ p ∈ U, ∀ k < 0, RS.laurentCoeffAt f p k = (D.coeff p) k)

noncomputable def RS.PrincipalPartData.toFun {U : Set ℂ} (D : PrincipalPartData U) : ℂ → ℂ

The associated function: sum of the finite tails (junk-free honest function).

Equations

• D.toFun z = ∑ᶠ (p : ℂ), ∑ k ∈ (D.coeff p).support, (D.coeff p) k * (z - p) ^ k

noncomputable def RS.PrincipalPartData.totalRes {U : Set ℂ} (D : PrincipalPartData U) : ℂ

Total residue of the datum.

Equations

• D.totalRes = ∑ᶠ (p : ℂ), (D.coeff p) (-1)

noncomputable def RS.PrincipalPartData.mlCoeff (f : ℂ → ℂ) (U : Set ℂ) (p : ℂ) : ℤ →₀ ℂ

The raw coefficient assignment underlying ofMeromorphicOn: at each p ∈ U, the negative Laurent tail of f at p (as a Finsupp on Finset.Icc (order.untop₀) (-1)); 0 off U.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.PrincipalPartData.mlCoeff_apply {f : ℂ → ℂ} {U : Set ℂ} (p : ℂ) (k : ℤ) : (mlCoeff f U p) k = if p ∈ U ∧ k < 0 then laurentCoeffAt f p k else 0

theorem RS.PrincipalPartData.mlCoeff_coeff_neg (f : ℂ → ℂ) (U : Set ℂ) (p : ℂ) (k : ℤ) : k ∈ (mlCoeff f U p).support → k < 0

theorem RS.PrincipalPartData.mlCoeff_mem_of_ne_zero (f : ℂ → ℂ) (U : Set ℂ) (p : ℂ) : mlCoeff f U p ≠ 0 → p ∈ U

theorem RS.PrincipalPartData.mlCoeff_finite_support {f : ℂ → ℂ} {U : Set ℂ} (hfin : {p : ℂ | p ∈ U ∧ meromorphicOrderAt f p < 0}.Finite) : {p : ℂ | mlCoeff f U p ≠ 0}.Finite

noncomputable def RS.PrincipalPartData.ofMeromorphicOn {U : Set ℂ} {f : ℂ → ℂ} (_hf : MeromorphicOn f U) (hfin : {p : ℂ | p ∈ U ∧ meromorphicOrderAt f p < 0}.Finite) : PrincipalPartData U

Extraction from a meromorphic function with finitely many poles.

Equations

• RS.PrincipalPartData.ofMeromorphicOn _hf hfin = RS.PrincipalPartData.mk' (RS.PrincipalPartData.mlCoeff f U) ⋯ ⋯ ⋯

theorem RS.PrincipalPartData.realizes_ofMeromorphicOn {U : Set ℂ} {f : ℂ → ℂ} (hf : MeromorphicOn f U) (hfin : {p : ℂ | p ∈ U ∧ meromorphicOrderAt f p < 0}.Finite) : Realizes f (ofMeromorphicOn hf hfin)

theorem RS.PrincipalPartData.Realizes.add {U : Set ℂ} {f g : ℂ → ℂ} {D E : PrincipalPartData U} (hf : Realizes f D) (hg : Realizes g E) : Realizes (f + g) (D + E)

theorem RS.PrincipalPartData.Realizes.smul {U : Set ℂ} {f : ℂ → ℂ} {D : PrincipalPartData U} (c : ℂ) (hf : Realizes f D) : Realizes (fun (z : ℂ) => c * f z) (c • D)

theorem RS.PrincipalPartData.Realizes.sub_orderAt_nonneg {U : Set ℂ} {f g : ℂ → ℂ} {D : PrincipalPartData U} (hf : Realizes f D) (hg : Realizes g D) (p : ℂ) : p ∈ U → 0 ≤ meromorphicOrderAt (fun (z : ℂ) => f z - g z) p

Two realizations differ by a pole-free function (the ML gluing atom: differences of solutions are holomorphic-after-repair).

theorem RS.PrincipalPartData.realizes_zero_iff {U : Set ℂ} {f : ℂ → ℂ} (hf : MeromorphicOn f U) : Realizes f 0 ↔ ∀ p ∈ U, 0 ≤ meromorphicOrderAt f p

Realizing the zero datum = no poles on U.