Partial fractions for functions with finitely many simple poles

A function on ℂ that is holomorphic away from a finite set S, has at most simple poles at the points of S, and tends to 0 at infinity is the sum of its principal parts:

f z = ∑ s ∈ S, residue f s / (z - s) for z ∉ S.

The residues can be prescribed through the elementary limits (z - s) * f z → c s. A punctured limit of this kind already makes f meromorphic with at most a simple pole at s (TauCeti.Contour.meromorphicAt_of_tendsto_sub_mul), so the identification needs no meromorphy hypothesis. Conversely, every such sum is holomorphic off S, has these limits and tends to 0 at infinity. This gives the characterization eqOn_sum_div_sub_iff. The same limits show that the coefficients of such a sum are determined by its values on any set accumulating at every pole.

This is how one identifies a function from its singularities and its behaviour at infinity. For example, the pre-Schwarzian derivative F'' / F' of a conformal map F from the upper half-plane onto a polygon continues by reflection to ℂ minus the prevertices. There it has simple poles whose residues are determined by the interior angles, and it tends to 0 at infinity. So the characterization identifies it with the Schwarz--Christoffel expression ∑ i, e i / (z - a i), which is the derivation of the Schwarz--Christoffel formula.

Main results

• Finset.differentiableOn_sum_div_sub, Finset.tendsto_sum_div_sub_cobounded and TauCeti.Contour.tendsto_sub_mul_sum_div_sub -- the sum z ↦ ∑ s ∈ S, c s / (z - s) is holomorphic off S, tends to 0 at infinity and has the limit c s of (z - s) * _ at s.
• TauCeti.Contour.eqOn_sum_residue_div_sub -- a function with finitely many at most simple poles that tends to 0 at infinity is the sum of its principal parts.
• TauCeti.Contour.eqOn_sum_div_sub_of_tendsto -- the same with prescribed residues, stated through the limits of (z - s) * f z.
• TauCeti.Contour.eqOn_sum_div_sub_iff -- the resulting characterization of the functions z ↦ ∑ s ∈ S, c s / (z - s) off S.
• TauCeti.Contour.eq_of_eqOn_sum_div_sub -- two such sums with the same distinct poles that agree on a set accumulating at every pole have the same coefficients.

References

• L. Ahlfors, Complex Analysis, Ch. 4, Section 3.1 (Liouville's theorem), and Ch. 6, Section 2 (the derivation of the Schwarz--Christoffel formula).

The partial-fraction sum

theorem Finset.differentiableOn_sum_div_sub (S : Finset ℂ) (c : ℂ → ℂ) : DifferentiableOn ℂ (fun (z : ℂ) => ∑ s ∈ S, c s / (z - s)) (↑S)ᶜ

The partial-fraction sum z ↦ ∑ s ∈ S, c s / (z - s) is holomorphic off S.

theorem Finset.tendsto_sum_div_sub_cobounded (S : Finset ℂ) (c : ℂ → ℂ) : Filter.Tendsto (fun (z : ℂ) => ∑ s ∈ S, c s / (z - s)) (Bornology.cobounded ℂ) (nhds 0)

The partial-fraction sum z ↦ ∑ s ∈ S, c s / (z - s) tends to 0 at infinity.

theorem TauCeti.tendsto_mul_sum_div_sub_cobounded {ι : Type u_1} {S : Finset ι} (a c : ι → ℂ) : Filter.Tendsto (fun (z : ℂ) => z * ∑ i ∈ S, c i / (z - a i)) (Bornology.cobounded ℂ) (nhds (∑ i ∈ S, c i))

Multiplying a finite partial-fraction sum by z at infinity recovers the sum of its coefficients. The poles may be indexed with repetitions.

theorem TauCeti.Contour.tendsto_sub_mul_sum_div_sub {S : Finset ℂ} (c : ℂ → ℂ) {s : ℂ} (hs : s ∈ S) : Filter.Tendsto (fun (z : ℂ) => (z - s) * ∑ t ∈ S, c t / (z - t)) (nhdsWithin s {s}ᶜ) (nhds (c s))

At a point s ∈ S, the partial-fraction sum z ↦ ∑ t ∈ S, c t / (z - t) has residue c s in the sense of the elementary limit: (z - s) * ∑ t ∈ S, c t / (z - t) → c s.

theorem TauCeti.Contour.tendsto_sub_mul_sum_div_sub_of_injective {ι : Type u_1} [Fintype ι] {a : ι → ℂ} (ha : Function.Injective a) (c : ι → ℂ) (j : ι) : Filter.Tendsto (fun (z : ℂ) => (z - a j) * ∑ i : ι, c i / (z - a i)) (nhdsWithin (a j) {a j}ᶜ) (nhds (c j))

For a sum indexed by an injective family of poles a i, the product (z - a j) * ∑ i, c i / (z - a i) tends to c j as z → a j.

theorem TauCeti.Contour.eq_of_eqOn_sum_div_sub {ι : Type u_1} [Fintype ι] {a : ι → ℂ} (ha : Function.Injective a) {c d : ι → ℂ} {s : Set ℂ} (hs : ∀ (i : ι), AccPt (a i) (Filter.principal s)) (h : Set.EqOn (fun (z : ℂ) => ∑ i : ι, c i / (z - a i)) (fun (z : ℂ) => ∑ i : ι, d i / (z - a i)) s) : c = d

Uniqueness of partial-fraction coefficients. Two partial-fraction sums with the same distinct poles a i that agree on a set accumulating at every pole have the same coefficients.

Identification by Liouville's theorem

theorem TauCeti.Contour.eqOn_sum_residue_div_sub {f : ℂ → ℂ} {S : Finset ℂ} (hf : DifferentiableOn ℂ f (↑S)ᶜ) (hmero : ∀ s ∈ S, MeromorphicAt f s) (horder : ∀ s ∈ S, ↑(-1) ≤ meromorphicOrderAt f s) (hlim : Filter.Tendsto f (Bornology.cobounded ℂ) (nhds 0)) : Set.EqOn f (fun (z : ℂ) => ∑ s ∈ S, residue f s / (z - s)) (↑S)ᶜ

Partial fractions for simple poles. If f is holomorphic off a finite set S, has at most a simple pole at each point of S and tends to 0 at infinity, then off S it is the sum of its principal parts, f z = ∑ s ∈ S, residue f s / (z - s).

Points of S at which f is analytic are allowed; their residues vanish.

theorem TauCeti.Contour.eqOn_sum_div_sub_of_tendsto {f : ℂ → ℂ} {S : Finset ℂ} {c : ℂ → ℂ} (hf : DifferentiableOn ℂ f (↑S)ᶜ) (hpole : ∀ s ∈ S, Filter.Tendsto (fun (z : ℂ) => (z - s) * f z) (nhdsWithin s {s}ᶜ) (nhds (c s))) (hlim : Filter.Tendsto f (Bornology.cobounded ℂ) (nhds 0)) : Set.EqOn f (fun (z : ℂ) => ∑ s ∈ S, c s / (z - s)) (↑S)ᶜ

Partial fractions with prescribed residues. If f is holomorphic off a finite set S, (z - s) * f z → c s as z → s for each s ∈ S, and f tends to 0 at infinity, then f z = ∑ s ∈ S, c s / (z - s) for every z ∉ S.

theorem TauCeti.Contour.eqOn_sum_div_sub_iff {f : ℂ → ℂ} {S : Finset ℂ} {c : ℂ → ℂ} : Set.EqOn f (fun (z : ℂ) => ∑ s ∈ S, c s / (z - s)) (↑S)ᶜ ↔ DifferentiableOn ℂ f (↑S)ᶜ ∧ (∀ s ∈ S, Filter.Tendsto (fun (z : ℂ) => (z - s) * f z) (nhdsWithin s {s}ᶜ) (nhds (c s))) ∧ Filter.Tendsto f (Bornology.cobounded ℂ) (nhds 0)

Characterization of partial-fraction sums. Off a finite set S, a function f agrees with z ↦ ∑ s ∈ S, c s / (z - s) if and only if it is holomorphic off S, satisfies (z - s) * f z → c s as z → s for each s ∈ S, and tends to 0 at infinity.