The Divisor of a meromorphic function

This file defines the divisor of a meromorphic function and proves the most basic lemmas about those divisors. The lemma MeromorphicOn.divisor_restrict guarantees compatibility between restrictions of divisors and of meromorphic functions to subsets of their domain of definition.

Definition of the Divisor

noncomputable def MeromorphicOn.divisor {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (U : Set 𝕜) : Function.locallyFinsuppWithin U ℤ

The divisor of a meromorphic function f, mapping a point z to the order of f at z, and to zero if the order is infinite.

Equations

• MeromorphicOn.divisor f U = { toFun := fun (z : 𝕜) => if h : MeromorphicOn f U ∧ z ∈ U then ⋯.order.untop₀ else 0, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }

theorem MeromorphicOn.divisor_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z : 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (U : Set 𝕜) : (divisor f U) z = if h : MeromorphicOn f U ∧ z ∈ U then ⋯.order.untop₀ else 0

Definition of the divisor

@[simp]

theorem MeromorphicOn.divisor_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {z : 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (hf : MeromorphicOn f U) (hz : z ∈ U) : (divisor f U) z = ⋯.order.untop₀

Simplifier lemma: on U, the divisor of a function f that is meromorphic on U evaluates to order.untop₀.

Congruence Lemmas

theorem MeromorphicOn.divisor_congr_codiscreteWithin_of_eqOn_compl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} (hf₁ : MeromorphicOn f₁ U) (h₁ : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) (h₂ : Set.EqOn f₁ f₂ Uᶜ) : divisor f₁ U = divisor f₂ U

If f₁ is meromorphic on U, if f₂ agrees with f₁ on a codiscrete subset of U and outside of U, then f₁ and f₂ induce the same divisors on U.

theorem MeromorphicOn.divisor_congr_codiscreteWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} (hf₁ : MeromorphicOn f₁ U) (h₁ : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) (h₂ : IsOpen U) : divisor f₁ U = divisor f₂ U

If f₁ is meromorphic on an open set U, if f₂ agrees with f₁ on a codiscrete subset of U, then f₁ and f₂ induce the same divisors onU.

Divisors of Analytic Functions

theorem MeromorphicOn.AnalyticOnNhd.divisor_nonneg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (hf : AnalyticOnNhd 𝕜 f U) : 0 ≤ divisor f U

Analytic functions have non-negative divisors.

Behavior under Standard Operations

theorem MeromorphicOn.divisor_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E} (h₁f₁ : MeromorphicOn f₁ U) (h₁f₂ : MeromorphicOn f₂ U) (h₂f₁ : ∀ (z : 𝕜) (hz : z ∈ U), ⋯.order ≠ ⊤) (h₂f₂ : ∀ (z : 𝕜) (hz : z ∈ U), ⋯.order ≠ ⊤) : divisor (f₁ • f₂) U = divisor f₁ U + divisor f₂ U

If orders are finite, the divisor of the scalar product of two meromorphic functions is the sum of the divisors.

See MeromorphicOn.exists_order_ne_top_iff_forall and MeromorphicOn.order_ne_top_of_isPreconnected for two convenient criteria to guarantee conditions h₂f₁ and h₂f₂.

theorem MeromorphicOn.divisor_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f₁ f₂ : 𝕜 → 𝕜} (h₁f₁ : MeromorphicOn f₁ U) (h₁f₂ : MeromorphicOn f₂ U) (h₂f₁ : ∀ (z : 𝕜) (hz : z ∈ U), ⋯.order ≠ ⊤) (h₂f₂ : ∀ (z : 𝕜) (hz : z ∈ U), ⋯.order ≠ ⊤) : divisor (f₁ * f₂) U = divisor f₁ U + divisor f₂ U

If orders are finite, the divisor of the product of two meromorphic functions is the sum of the divisors.

See MeromorphicOn.exists_order_ne_top_iff_forall and MeromorphicOn.order_ne_top_of_isPreconnected for two convenient criteria to guarantee conditions h₂f₁ and h₂f₂.

@[simp]

theorem MeromorphicOn.divisor_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜} : divisor f⁻¹ U = -divisor f U

The divisor of the inverse is the negative of the divisor.

@[simp]

theorem MeromorphicOn.divisor_restrict {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {V : Set 𝕜} (hf : MeromorphicOn f U) (hV : V ⊆ U) : (divisor f U).restrict hV = divisor f V

Taking the divisor of a meromorphic function commutes with restriction.

theorem MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} (hf₁ : MeromorphicOn f₁ U) (hf₂ : AnalyticOnNhd 𝕜 f₂ U) : (divisor (f₁ + f₂) U)⁻ = (divisor f₁ U)⁻

Adding an analytic function to a meromorphic one does not change the pole divisor.

theorem MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} (hf₁ : AnalyticOnNhd 𝕜 f₁ U) (hf₂ : MeromorphicOn f₂ U) : (divisor (f₁ + f₂) U)⁻ = (divisor f₂ U)⁻

Adding an analytic function to a meromorphic one does not change the pole divisor.