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.

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.

TODO: Under suitable assumptions, 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.

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 Set.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 𝕜.

theorem Function.FactorizedRational.order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z : 𝕜} (d : 𝕜 → ℤ) (h₁d : (support d).Finite) : ⋯.order = ↑(d z)

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

theorem Function.FactorizedRational.order_ne_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z : 𝕜} (d : 𝕜 → ℤ) : ⋯.order ≠ ⊤

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.