Factorized Rational Functions

This file discusses functions 𝕜 → 𝕜 of the form ∏ᶠ u, (· - u) ^ d u, where d : 𝕜 → ℤ is integer-valued. We show that these "factorized rational functions" are meromorphic in normal form, with divisor equal to d.

Under suitable assumptions, we show that meromorphic functions are equivalent, modulo equality on codiscrete sets, to the product of a factorized rational function and an analytic function without zeros.

Implementation Note: For consistency, we use ∏ᶠ u, (· - u) ^ d u throughout. If the support of d is finite, then evaluation of functions commutes with finprod, and the helper lemma Function.FactorizedRational.finprod_eval asserts that ∏ᶠ u, (· - u) ^ d u equals the function fun x ↦ ∏ᶠ u, (x - u) ^ d u. If d has infinite support, this equality is wrong in general. There are elementary examples of functions d where ∏ᶠ u, (· - u) ^ d u is constant one, while fun x ↦ ∏ᶠ u, (x - u) ^ d u is not continuous.

Elementary Properties of Factorized Rational Functions

theorem Function.FactorizedRational.mulSupport {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (d : 𝕜 → ℤ) : (Function.mulSupport fun (u : 𝕜) => (fun (x : 𝕜) => x - u) ^ d u) = support d

Helper Lemma: Identify the support of d as the mulsupport of the product defining the factorized rational function.

theorem Function.FactorizedRational.finprod_eq_fun {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} (h : (support d).Finite) : ∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ d u = fun (x : 𝕜) => ∏ᶠ (u : 𝕜), (x - u) ^ d u

Helper Lemma: If the support of d is finite, then evaluation of functions commutes with finprod, and the function ∏ᶠ u, (· - u) ^ d u equals fun x ↦ ∏ᶠ u, (x - u) ^ d u.

theorem Function.FactorizedRational.analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} {x : 𝕜} (h : 0 ≤ d x) : AnalyticAt 𝕜 (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ d u) x

Factorized rational functions are analytic wherever the exponent is non-negative.

theorem Function.FactorizedRational.ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} {x : 𝕜} (h : d x = 0) : (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ d u) x ≠ 0

Factorized rational functions are non-zero wherever the exponent is zero.

theorem Function.FactorizedRational.extractFactor {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} (u₀ : 𝕜) (hd : (support d).Finite) : ∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ d u = (fun (x : 𝕜) => x - u₀) ^ d u₀ * ∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ update d u₀ 0 u

Helper Lemma for Computations: Extract one factor out of a factorized rational function.

theorem Function.FactorizedRational.meromorphicNFOn_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (d : 𝕜 → ℤ) : MeromorphicNFOn (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ d u) Set.univ

Factorized rational functions are meromorphic in normal form on univ.

theorem Function.FactorizedRational.meromorphicNFOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (d : 𝕜 → ℤ) (U : Set 𝕜) : MeromorphicNFOn (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ d u) U

Factorized rational functions are meromorphic in normal form on arbitrary subsets of 𝕜.

Orders and Divisors of Factorized Rational Functions

theorem Function.FactorizedRational.meromorphicOrderAt_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z : 𝕜} (d : 𝕜 → ℤ) (h₁d : (support d).Finite) : meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ d u) z = ↑(d z)

The order of the factorized rational function (∏ᶠ u, fun z ↦ (z - u) ^ d u) at z equals d z.

@[deprecated Function.FactorizedRational.meromorphicOrderAt_eq (since := "2025-05-22")]

theorem Function.FactorizedRational.order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z : 𝕜} (d : 𝕜 → ℤ) (h₁d : (support d).Finite) : meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ d u) z = ↑(d z)

Alias of Function.FactorizedRational.meromorphicOrderAt_eq.

---

The order of the factorized rational function (∏ᶠ u, fun z ↦ (z - u) ^ d u) at z equals d z.

theorem Function.FactorizedRational.meromorphicOrderAt_ne_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z : 𝕜} (d : 𝕜 → ℤ) : meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ d u) z ≠ ⊤

Factorized rational functions are nowhere locally constant zero.

@[deprecated Function.FactorizedRational.meromorphicOrderAt_ne_top (since := "2025-05-22")]

theorem Function.FactorizedRational.order_ne_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z : 𝕜} (d : 𝕜 → ℤ) : meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ d u) z ≠ ⊤

Alias of Function.FactorizedRational.meromorphicOrderAt_ne_top.

---

Factorized rational functions are nowhere locally constant zero.

theorem Function.FactorizedRational.divisor {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {D : locallyFinsuppWithin U ℤ} (hD : D.support.Finite) : MeromorphicOn.divisor (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ D u) U = D

If D is a divisor, then the divisor of the factorized rational function equals D.

Elimination of Zeros and Poles

This section shows that every meromorphic function with finitely many zeros and poles is equivalent, modulo equality on codiscrete sets, to the product of a factorized rational function and an analytic function without zeros.

We provide analogous results for functions of the form log ‖meromorphic‖.

TODO: Identify some of the terms that appear in the decomposition.

theorem MeromorphicOn.extract_zeros_poles {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} (h₁f : MeromorphicOn f U) (h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤) (h₃f : (divisor f U).support.Finite) : ∃ (g : 𝕜 → E), AnalyticOnNhd 𝕜 g U ∧ (∀ (u : ↑U), g ↑u ≠ 0) ∧ f =ᶠ[Filter.codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ (divisor f U) u) • g

If f is meromorphic on an open set U, if f is nowhere locally constant zero, and if the support of the divisor of f is finite, then there exists an analytic function g on U without zeros such that f is equivalent, modulo equality on codiscrete sets, to the product of g and the factorized rational function associated with the divisor of f.

theorem MeromorphicOn.extract_zeros_poles_log {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f g : 𝕜 → E} {D : Function.locallyFinsuppWithin U ℤ} (hg : ∀ (u : ↑U), g ↑u ≠ 0) (h : f =ᶠ[Filter.codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun (x : 𝕜) => x - u) ^ D u) • g) : (fun (x : 𝕜) => Real.log ‖f x‖) =ᶠ[Filter.codiscreteWithin U] (∑ᶠ (u : 𝕜), fun (x : 𝕜) => ↑(D u) * Real.log ‖x - u‖) + fun (x : 𝕜) => Real.log ‖g x‖

In the setting of MeromorphicOn.extract_zeros_poles, the function log ‖f‖ is equivalent, modulo equality on codiscrete subsets, to ∑ᶠ u, (divisor f U u * log ‖· - u‖) + log ‖g ·‖.