Polar-part decompositions

A polar-part decomposition of f on U at the finite singular set S: for each s ∈ S an explicit finite Laurent tail polarPart s z = ∑ k, coeff s k / (z - s)^(k+1), such that f minus the total polar part extends to a function differentiable on all of U, and the residue at each s is the first Laurent coefficient. This bundles exactly the data the generalized residue theorem manipulates: the analytic remainder integrates to zero around any null-homologous closed curve — even one passing through the poles — so the principal value of ∮ f reduces to the polar parts.

Main definitions

• Contour.PolarPartDecomposition f S U — the decomposition data: polar parts, orders, Laurent coefficients, the residue identification, and the analytic remainder.
• Contour.meromorphicPolarPartTotal — the sum of the canonical per-point polar parts over S.
• Contour.PolarPartDecomposition.ofMeromorphic — every f differentiable on U \ S and meromorphic at each s ∈ S has a polar-part decomposition, built from the canonical Laurent data of MeromorphicLaurent.lean.

Main results

• Contour.PolarPartDecomposition.sum_ite_coeff_eq_residue_mul — a weight carried by the simple-pole coefficient alone sums to Res_s f times that weight; the last step of every term-by-term evaluation of a polar part.
• Contour.PolarPartDecomposition.intervalIntegral_deriv_smul_analyticRemainder_eq_zero — the contour integral of the analytic remainder along a closed null-homologous piecewise-C¹ curve in U vanishes, by the homology Cauchy theorem.
• Contour.PolarPartDecomposition.intervalIntegrable_polarPart_mul_deriv_truncated — the ε-truncated polar-part integrand along a measurable curve with interval-integrable derivative is interval-integrable, for every ε > 0 — the integrability clause of HasCauchyPVAt for a polar part.

Provenance

The structure is migrated from PolarPartDecomposition of HungerbuhlerWasem.lean in the AINTLIB LeanModularForms development; the remainder-integral theorem is its analyticRemainder_contourIntegral_zero, which there re-runs Dixon's argument inline and here is a direct application of Contour.homologyCauchyTheorem. The constructor is migrated from polarPartDecomposition_of_meromorphic of LaurentExtraction.lean there, with the ℂ-indexed case splits replaced by S-indexed data throughout; the truncated-integrand integrability lemma is adapted from cpvIntegrand_polarPart_intervalIntegrable of MultiPoleDCT.lean, with the Lipschitz bound on the curve replaced by interval-integrability of the derivative. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

structure TauCeti.Contour.PolarPartDecomposition (f : ℂ → ℂ) (S : Finset ℂ) (U : Set ℂ) : Type

Polar-part decomposition of f on U at the finite singular set S: explicit finite Laurent tails at the points of S whose removal from f leaves a function differentiable on all of U, with the residue at each s ∈ S read off as the first Laurent coefficient. The data is indexed by S, so a decomposition carries nothing beyond what its laws constrain; the polar part is pinned for every z (at z = s the Laurent sum takes the junk value 0, by division by zero in ℂ).

• order : ↥S → ℕ

  The order of the polar part at each pole (0 for no pole).

• coeff (s : ↥S) : Fin (self.order s) → ℂ

  The Laurent coefficients of the polar part at each pole.

• polarPart : ↥S → ℂ → ℂ

  The polar part at each pole, as a function of z.

• polarPart_eq (s : ↥S) (z : ℂ) : self.polarPart s z = ∑ k : Fin (self.order s), self.coeff s k / (z - ↑s) ^ (↑k + 1)

  The polar part at s is the explicit Laurent sum ∑ k, coeff s k / (z - s)^(k+1).

• residue_eq (s : ↥S) : residue f ↑s = if h : 0 < self.order s then self.coeff s ⟨0, h⟩ else 0

  The residue at s ∈ S is the first Laurent coefficient, or zero for an empty polar part.

• analyticRemainder : ℂ → ℂ

  The function f minus the total polar part, extended to all of U.

• analyticRemainder_differentiableOn : DifferentiableOn ℂ self.analyticRemainder U

  The analytic remainder is differentiable on all of U.

• f_eq (z : ℂ) : z ∈ U \ ↑S → f z = self.analyticRemainder z + ∑ s ∈ S.attach, self.polarPart s z

  Off the singular set, f is the analytic remainder plus the total polar part.

theorem TauCeti.Contour.PolarPartDecomposition.sum_ite_coeff_eq_residue_mul {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (s : ↥S) (c : ℂ) : (∑ k : Fin (decomp.order s), if ↑k = 0 then decomp.coeff s k * c else 0) = residue f ↑s * c

Only the simple-pole coefficient survives. Summing the Laurent coefficients at s against a weight c carried by the simple-pole term alone leaves Res_s f · c, the empty polar part included (both sides are then 0). Every evaluation of a polar part term by term — as a contour integral or as a principal value — bottoms out here, the higher-order terms having already been shown to contribute nothing.

theorem TauCeti.Contour.PolarPartDecomposition.intervalIntegral_deriv_smul_analyticRemainder_eq_zero {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (hU : IsOpen U) {γ : ℝ → ℂ} {a b : ℝ} (hγ_pc1 : IsPiecewiseC1On γ a b) (hγ : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b) (hnull : IsNullHomologous γ a b U) : ∫ (t : ℝ) in a..b, deriv γ t • decomp.analyticRemainder (γ t) = 0

The analytic remainder integrates to zero along any closed null-homologous piecewise-C¹ curve in U — even one passing through the poles of f, since the remainder extends differentiably to all of U. The homology Cauchy theorem applied to the remainder.

noncomputable def TauCeti.Contour.meromorphicPolarPartTotal {f : ℂ → ℂ} {S : Finset ℂ} (hMero : ∀ s ∈ S, MeromorphicAt f s) (z : ℂ) : ℂ

The total polar part over the singular set: the sum of the canonical per-point polar parts.

Equations

• TauCeti.Contour.meromorphicPolarPartTotal hMero z = ∑ s ∈ S.attach, TauCeti.Contour.meromorphicPolarPartAt ⋯ z

theorem TauCeti.Contour.meromorphicPolarPartTotal_eq_sum {f : ℂ → ℂ} {S : Finset ℂ} (hMero : ∀ s ∈ S, MeromorphicAt f s) (z : ℂ) : meromorphicPolarPartTotal hMero z = ∑ s ∈ S.attach, meromorphicPolarPartAt ⋯ z

The total polar part, unfolded to the sum of the canonical per-point polar parts.

noncomputable def TauCeti.Contour.PolarPartDecomposition.ofMeromorphic {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f (U \ ↑S)) (hMero : ∀ s ∈ S, MeromorphicAt f s) : PolarPartDecomposition f S U

The decomposition of a meromorphic integrand. From f differentiable on U \ S and meromorphic at each s ∈ S, the canonical Laurent data assembles into a PolarPartDecomposition f S U: the orders are the canonical polar orders — so they are evaluable by callers, in particular 1 at simple poles — and the analytic remainder is f minus the total polar part, extended across the poles by its limits.

Equations

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

@[simp]

theorem TauCeti.Contour.PolarPartDecomposition.ofMeromorphic_order {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} {hU : IsOpen U} {hf : DifferentiableOn ℂ f (U \ ↑S)} {hMero : ∀ s ∈ S, MeromorphicAt f s} (s : ↥S) : (ofMeromorphic hU hf hMero).order s = meromorphicPolarOrderAt f ↑s

The constructed order is the canonical polar order — evaluable by callers, in particular 1 at simple poles (meromorphicPolarOrderAt_eq_one).

@[simp]

theorem TauCeti.Contour.PolarPartDecomposition.ofMeromorphic_coeff {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} {hU : IsOpen U} {hf : DifferentiableOn ℂ f (U \ ↑S)} {hMero : ∀ s ∈ S, MeromorphicAt f s} (s : ↥S) (k : Fin ((ofMeromorphic hU hf hMero).order s)) : (ofMeromorphic hU hf hMero).coeff s k = meromorphicPolarCoeffAt ⋯ (Fin.cast ⋯ k)

The constructed coefficients are the canonical Laurent coefficients, along the index identification ofMeromorphic_order.

@[simp]

theorem TauCeti.Contour.PolarPartDecomposition.ofMeromorphic_polarPart {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} {hU : IsOpen U} {hf : DifferentiableOn ℂ f (U \ ↑S)} {hMero : ∀ s ∈ S, MeromorphicAt f s} (s : ↥S) (z : ℂ) : (ofMeromorphic hU hf hMero).polarPart s z = meromorphicPolarPartAt ⋯ z

The constructed polar part is the canonical polar part.

theorem TauCeti.Contour.PolarPartDecomposition.ofMeromorphic_analyticRemainder {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} {hU : IsOpen U} {hf : DifferentiableOn ℂ f (U \ ↑S)} {hMero : ∀ s ∈ S, MeromorphicAt f s} {z : ℂ} (hz : z ∉ ↑S) : (ofMeromorphic hU hf hMero).analyticRemainder z = f z - meromorphicPolarPartTotal hMero z

Off the singular set, the constructed analytic remainder is f minus the total polar part.

theorem TauCeti.Contour.PolarPartDecomposition.intervalIntegrable_polarPart_mul_deriv_truncated {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : PolarPartDecomposition f S U) (s : ↥S) {γ : ℝ → ℂ} {a b : ℝ} (hγ_meas : Measurable γ) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) {ε : ℝ} (hε : 0 < ε) : IntervalIntegrable (fun (t : ℝ) => if ‖γ t - ↑s‖ > ε then decomp.polarPart s (γ t) * deriv γ t else 0) MeasureTheory.volume a b

The truncated polar-part integrand is interval-integrable for every ε > 0: off the ε-ball around the pole, the Laurent tail is bounded by ∑ k, ‖coeff s k‖ / ε ^ (k+1), so the integrand is dominated by a constant multiple of ‖deriv γ‖ — the integrability clause of HasCauchyPVAt for a polar part along a curve crossing the pole.