The Divisor of a meromorphic function

This file defines the divisor of a meromorphic function and proves the most basic lemmas about those divisors.

TODO

• Compatibility with restriction of divisors/functions
• Non-negativity of the divisor for an analytic function
• Behavior under addition of functions
• Congruence lemmas for codiscreteWithin

Definition of the Divisor

noncomputable def MeromorphicOn.divisor {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 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] [CompleteSpace 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] [CompleteSpace 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₀.

Behavior under Standard Operations

theorem MeromorphicOn.divisor_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [CompleteSpace 𝕜] {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 𝕜} [CompleteSpace 𝕜] {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 𝕜} [CompleteSpace 𝕜] {f : 𝕜 → 𝕜} : divisor f⁻¹ U = -divisor f U

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