The principal part of a meromorphic germ

Let 𝕜 be a nontrivially normed field and a : 𝕜. A meromorphic germ φ at a splits uniquely as φ = P((z - a)⁻¹) + g, where P is a polynomial without constant term and g is the germ of a function analytic at a. The polynomial P is the principal part TauCeti.meromorphicGerms.principalPart φ; writing P = Σ_{k ≥ 1} P_k X ^ k, the germ φ has the finite principal part Σ_k P_k (z - a) ^ (-k) and a regular remainder.

Concretely, if φ is represented by (z - a)⁻ᴺ h z with h analytic at a, Taylor's formula with divided-difference remainder TauCeti.sum_add_pow_sub_smul_iterate_dslope splits h z = Σ_{j<N} c_j (z - a) ^ j + (z - a) ^ N q z, where c_j are the Taylor coefficients of h at a and q = (swap dslope a)^[N] h is analytic at a. Dividing by (z - a) ^ N gives the principal part Σ_{j<N} c_j X ^ (N - j) and the regular remainder q (TauCeti.meromorphicGerms.principalPart_eq_sum_coeff and TauCeti.meromorphicGerms.coe_sub_evalInvSub_principalPart).

Uniqueness rests on the order computation TauCeti.meromorphicOrderAt_eval_inv_sub: a nonzero polynomial P in (z - a)⁻¹ has order -P.natDegree at a, so when P has no constant term it has a pole at a and is not the germ of an analytic function. Hence the principal part depends only on the germ, not on the exponent N, the representative or the neighbourhood used to compute it, and it is linear over 𝕜.

Over ℂ the regular remainder is a germ of the holomorphic structure sheaf; that version of the splitting is TauCeti.holomorphicStructureSheaf.regularPart in TauCeti.Geometry.Manifold.Complex.StructureSheaf.MeromorphicGerm.

Main declarations

• Polynomial.meromorphicAt_eval_inv_sub: a polynomial in (z - a)⁻¹ is meromorphic at a.
• TauCeti.meromorphicOrderAt_eval_inv_sub: the order at a of z ↦ P((z - a)⁻¹).
• TauCeti.meromorphicGerms.evalInvSub: the ring homomorphism P ↦ P((z - a)⁻¹) into the meromorphic germs at a; it is injective (evalInvSub_injective).
• TauCeti.meromorphicGerms.principalPart: the principal part, a 𝕜-linear map to polynomials.
• TauCeti.meromorphicGerms.principalPart_eq_iff: its characterization: principalPart φ = P exactly when P has no constant term and φ - P((z - a)⁻¹) has an analytic representative.
• TauCeti.meromorphicGerms.principalPart_eq_zero_iff: the principal part vanishes exactly on the germs of analytic functions.
• TauCeti.meromorphicGerms.natDegree_principalPart_mk_le: a pole bound bounds the degree of the principal part.
• TauCeti.meromorphicGerms.principalPart_eq_sum_coeff: the principal part of (z - a)⁻ᴺ h z through the Taylor coefficients of h.

References

• Lars V. Ahlfors, Complex Analysis, 3rd edition, McGraw-Hill, 1979, Chapter 4, Section 3.

Polynomials in the inverse coordinate

theorem Polynomial.meromorphicAt_eval_inv_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (P : Polynomial 𝕜) (a : 𝕜) : MeromorphicAt (fun (z : 𝕜) => eval (z - a)⁻¹ P) a

A polynomial in the inverse coordinate (z - a)⁻¹ is meromorphic at a.

theorem TauCeti.meromorphicOrderAt_eval_inv_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {P : Polynomial 𝕜} (hP : P ≠ 0) (a : 𝕜) : meromorphicOrderAt (fun (z : 𝕜) => Polynomial.eval (z - a)⁻¹ P) a = ↑(-↑P.natDegree)

A nonzero polynomial P in the inverse coordinate has order -P.natDegree at a: off a it is (z - a) ^ (-P.natDegree) times the reversed polynomial P.reverse evaluated at z - a, whose value at a is the leading coefficient of P.

theorem TauCeti.eq_zero_of_eval_inv_sub_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {P : Polynomial 𝕜} (hP : P.coeff 0 = 0) {g : 𝕜 → 𝕜} (hg : AnalyticAt 𝕜 g a) (h : (fun (z : 𝕜) => Polynomial.eval (z - a)⁻¹ P) =ᶠ[nhdsWithin a {a}ᶜ] g) : P = 0

A polynomial without constant term in the inverse coordinate (z - a)⁻¹ agrees with a function analytic at a on a punctured neighbourhood of a only if it is zero: otherwise it has a pole at a.

theorem TauCeti.inv_pow_sub_mul_eq_eval_inv_sub_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (h : 𝕜 → 𝕜) (N : ℕ) {z : 𝕜} (hz : z ≠ a) : ((z - a) ^ N)⁻¹ * h z = Polynomial.eval (z - a)⁻¹ (∑ j ∈ Finset.range N, Polynomial.C ((Function.swap dslope a)^[j] h a) * Polynomial.X ^ (N - j)) + (Function.swap dslope a)^[N] h z

Principal part splitting of (z - a)⁻ᴺ h. For every function h and every N, off a, (z - a)⁻ᴺ h z = P((z - a)⁻¹) + q z with P = Σ_{j<N} c_j X ^ (N - j), where c_j = (swap dslope a)^[j] h a and q = (swap dslope a)^[N] h.

Evaluation at the inverse coordinate

noncomputable def TauCeti.meromorphicGerms.evalInvSub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (a : 𝕜) : Polynomial 𝕜 →+* ↥(meromorphicGerms 𝕜 a)

Evaluation at the inverse coordinate: the polynomial P gives the meromorphic germ of z ↦ P((z - a)⁻¹) at a.

@[simp]

theorem Polynomial.coe_evalInvSub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (P : Polynomial 𝕜) : ↑((TauCeti.meromorphicGerms.evalInvSub a) P) = ↑fun (z : 𝕜) => eval (z - a)⁻¹ P

theorem TauCeti.meromorphicGerms.evalInvSub_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} : Function.Injective ⇑(evalInvSub a)

Distinct polynomials in the inverse coordinate have distinct germs at a.

The principal part

noncomputable def TauCeti.meromorphicGerms.principalPart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} : ↥(meromorphicGerms 𝕜 a) →ₗ[𝕜] Polynomial 𝕜

The principal part of a meromorphic germ φ at a: the unique polynomial P without constant term such that φ - P((z - a)⁻¹) is the germ of a function analytic at a. It is linear over 𝕜.

@[simp]

theorem TauCeti.meromorphicGerms.coeff_zero_principalPart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (φ : ↥(meromorphicGerms 𝕜 a)) : (principalPart φ).coeff 0 = 0

The principal part has no constant term.

theorem TauCeti.meromorphicGerms.exists_analyticAt_coe_sub_evalInvSub_principalPart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} (φ : ↥(meromorphicGerms 𝕜 a)) : ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g a ∧ ↑(φ - (evalInvSub a) (principalPart φ)) = ↑g

Subtracting its principal part from a meromorphic germ leaves the germ of an analytic function.

theorem TauCeti.meromorphicGerms.principalPart_eq_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {φ : ↥(meromorphicGerms 𝕜 a)} {P : Polynomial 𝕜} : principalPart φ = P ↔ P.coeff 0 = 0 ∧ ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g a ∧ ↑(φ - (evalInvSub a) P) = ↑g

Characterization of the principal part. principalPart φ = P exactly when P has no constant term and φ - P((z - a)⁻¹) is the germ of a function analytic at a.

@[simp]

theorem TauCeti.meromorphicGerms.principalPart_evalInvSub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {P : Polynomial 𝕜} : principalPart ((evalInvSub a) P) = P - Polynomial.C (P.coeff 0)

The principal part of a polynomial in the inverse coordinate is the polynomial with its constant term removed.

theorem TauCeti.meromorphicGerms.principalPart_evalInvSub_of_coeff_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {P : Polynomial 𝕜} (hP : P.coeff 0 = 0) : principalPart ((evalInvSub a) P) = P

A polynomial without constant term in the inverse coordinate is its own principal part.

theorem TauCeti.meromorphicGerms.principalPart_eq_zero_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {φ : ↥(meromorphicGerms 𝕜 a)} : principalPart φ = 0 ↔ ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g a ∧ ↑φ = ↑g

The principal part of a meromorphic germ vanishes exactly when the germ is that of a function analytic at a.

theorem TauCeti.meromorphicGerms.principalPart_mk_eq_zero_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicAt f a) : principalPart (mk f hf) = 0 ↔ 0 ≤ meromorphicOrderAt f a

The principal part of the germ of a function meromorphic at a vanishes exactly when the function has nonnegative order at a.

theorem TauCeti.meromorphicGerms.natDegree_principalPart_mk_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicAt f a) {N : ℕ} (hN : ↑(-↑N) ≤ meromorphicOrderAt f a) : (principalPart (mk f hf)).natDegree ≤ N

A pole bound bounds the degree of the principal part. The constant term of the principal part is zero, so a removable singularity contributes the zero polynomial.

theorem TauCeti.meromorphicGerms.principalPart_eq_sum_coeff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {φ : ↥(meromorphicGerms 𝕜 a)} {h : 𝕜 → 𝕜} {p : FormalMultilinearSeries 𝕜 𝕜 𝕜} (hp : HasFPowerSeriesAt h p a) {N : ℕ} (hφ : ↑φ = ↑fun (z : 𝕜) => ((z - a) ^ N)⁻¹ * h z) : principalPart φ = ∑ j ∈ Finset.range N, Polynomial.C (p.coeff j) * Polynomial.X ^ (N - j)

The principal part through Taylor coefficients. If φ is the germ of (z - a)⁻ᴺ h z, where h has the power series p at a, then the principal part of φ is Σ_{j<N} p.coeff j • X ^ (N - j): the Taylor coefficients of h of degree below N.

theorem TauCeti.meromorphicGerms.coe_sub_evalInvSub_principalPart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {a : 𝕜} {φ : ↥(meromorphicGerms 𝕜 a)} {h : 𝕜 → 𝕜} (hh : AnalyticAt 𝕜 h a) {N : ℕ} (hφ : ↑φ = ↑fun (z : 𝕜) => ((z - a) ^ N)⁻¹ * h z) : ↑(φ - (evalInvSub a) (principalPart φ)) = ↑((Function.swap dslope a)^[N] h)

The regular remainder through divided differences. If φ is the germ of (z - a)⁻ᴺ h z with h analytic at a, then φ minus its principal part is the germ of the analytic function (swap dslope a)^[N] h, the remainder in Taylor's formula h z = Σ_{j<N} c_j (z - a) ^ j + (z - a) ^ N (swap dslope a)^[N] h z.