Divisors and orders of meromorphic functions

Divisor values record finite meromorphic orders, while local finiteness controls sums over their support.

At a point z ∈ U, Mathlib's MeromorphicOn.divisor f U evaluates to (meromorphicOrderAt f z).untop₀, while zero counts of analytic functions are stated in terms of analyticOrderNatAt f z. The comparison identifies the local multiplicity. Local finiteness also gives finite divisor support on subsets of compact sets and bounded regions whose closures lie in the meromorphic domain. For whole-space divisors, it makes norm sublevels of support finite and bounds sums over their subsets by the corresponding closed-ball count.

Main results

• MeromorphicOn.divisor_eq_analyticOrderNatAt — at a point where f is analytic, the divisor reads analyticOrderNatAt f z.
• MeromorphicOn.divisor_norm_sublevel_finite — finitely many support points occur in each norm sublevel over a proper normed field.
• AnalyticOnNhd.tsum_divisor_subtype_le_sum_closedBall — a support-subset multiplicity sum is bounded by the containing closed-ball count.
• MeromorphicOn.meromorphicOrderAt_eq_of_divisor_eq — equal divisors determine equal finite meromorphic orders.
• MeromorphicOn.divisor_finite_inter_support_of_isCompact — finite divisor support on a subset of a compact set in the meromorphic domain.
• MeromorphicOn.divisor_finite_inter_support — finite divisor support on a bounded region whose closure lies in the meromorphic domain.

theorem MeromorphicOn.divisor_norm_sublevel_finite {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (R : ℝ) : {ρ : ↑(divisor f Set.univ).support | ‖↑ρ‖ ≤ R}.Finite

The divisor of a whole-space function has finitely many support points in every norm sublevel set over a proper normed field. No meromorphy hypothesis on the representative is needed because its divisor is zero when it is not meromorphic.

theorem AnalyticOnNhd.tsum_divisor_subtype_le_sum_closedBall {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {R : ℝ} (hf : AnalyticOnNhd 𝕜 f Set.univ) (s : Set ↑(MeromorphicOn.divisor f Set.univ).support) (hs : ∀ ρ ∈ s, ‖↑ρ‖ ≤ R) : ∑' (ρ : ↑s), ↑((MeromorphicOn.divisor f Set.univ) ↑↑ρ) ≤ ↑(∑ᶠ (z : 𝕜), (MeromorphicOn.divisor f (Metric.closedBall 0 R)) z)

Summing divisor multiplicities over a bounded subset of whole-space support is bounded by the divisor count on the containing closed ball.

theorem MeromorphicOn.divisor_eq_analyticOrderNatAt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} {z : 𝕜} (hm : MeromorphicOn f U) (hf : AnalyticAt 𝕜 f z) (hz : z ∈ U) : (divisor f U) z = ↑(analyticOrderNatAt f z)

At a point z ∈ U where a function meromorphic on U is analytic, its divisor on U equals its order of vanishing analyticOrderNatAt f z. This includes a point near which f vanishes identically: there the analytic order is infinite and both sides read 0.

The divisor is defined through meromorphicOrderAt, while zero counts of analytic functions are stated through analyticOrderNatAt; this lemma translates between the two, so that a statement about divisor values of a function analytic on U becomes one about its orders of vanishing. It says nothing at a pole, where f is not analytic.

theorem MeromorphicOn.meromorphicOrderAt_eq_of_divisor_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {U : Set 𝕜} {f : 𝕜 → E} {g : 𝕜 → F} (hf : MeromorphicOn f U) (hg : MeromorphicOn g U) (hd : divisor f U = divisor g U) {z : 𝕜} (hz : z ∈ U) (hfz : meromorphicOrderAt f z ≠ ⊤) (hgz : meromorphicOrderAt g z ≠ ⊤) : meromorphicOrderAt f z = meromorphicOrderAt g z

Equal divisors determine equal meromorphic orders at a point where both orders are finite. The two functions may take values in different normed spaces over the same field.

theorem MeromorphicOn.divisor_finite_inter_support_of_isCompact {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U R K : Set 𝕜} (hK : IsCompact K) (hKU : K ⊆ U) (hRK : R ⊆ K) : (R ∩ Function.support ⇑(divisor f U)).Finite

A meromorphic divisor has finite support on any subset of a compact set in its domain. For f not meromorphic on U the divisor is zero.

theorem MeromorphicOn.divisor_finite_inter_support {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U R : Set 𝕜} [ProperSpace 𝕜] (hR : Bornology.IsBounded R) (hRU : closure R ⊆ U) : (R ∩ Function.support ⇑(divisor f U)).Finite

A bounded region has finite divisor support when its closure is in the meromorphic domain.