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

• One or more equations did not get rendered due to their size.

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 MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).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 = (meromorphicOrderAt f z).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.

@[simp]

theorem MeromorphicOn.divisor_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (e : E) : divisor (fun (x : 𝕜) => e) U = 0

The divisor of a constant function is 0.

@[simp]

theorem MeromorphicOn.divisor_intCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (n : ℤ) : divisor (↑n) U = 0

The divisor of a constant function is 0.

@[simp]

theorem MeromorphicOn.divisor_natCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (n : ℕ) : divisor (↑n) U = 0

The divisor of a constant function is 0.

@[simp]

theorem MeromorphicOn.divisor_ofNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (n : ℕ) : divisor (OfNat.ofNat n) U = 0

The divisor of a constant function is 0.

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 ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) (h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) : 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_fun_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 ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) (h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) : divisor (fun (z : 𝕜) => f₁ z • f₂ z) 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.

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 ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) (h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) : 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₂.

theorem MeromorphicOn.divisor_fun_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f₁ f₂ : 𝕜 → 𝕜} (h₁f₁ : MeromorphicOn f₁ U) (h₁f₂ : MeromorphicOn f₂ U) (h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) (h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) : divisor (fun (z : 𝕜) => f₁ z * f₂ z) 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.

@[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_fun_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜} : divisor (fun (z : 𝕜) => (f z)⁻¹) U = -divisor f U

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

theorem MeromorphicOn.divisor_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicOn f U) (n : ℕ) : divisor (f ^ n) U = n • divisor f U

If f is meromorphic, then the divisor of f ^ n is n times the divisor of f.

theorem MeromorphicOn.divisor_fun_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicOn f U) (n : ℕ) : divisor (fun (z : 𝕜) => f z ^ n) U = n • divisor f U

If f is meromorphic, then the divisor of f ^ n is n times the divisor of f.

theorem MeromorphicOn.divisor_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicOn f U) (n : ℤ) : divisor (f ^ n) U = n • divisor f U

If f is meromorphic, then the divisor of f ^ n is n times the divisor of f.

theorem MeromorphicOn.divisor_fun_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜} (hf : MeromorphicOn f U) (n : ℤ) : divisor (fun (z : 𝕜) => f z ^ n) U = n • divisor f U

If f is meromorphic, then the divisor of f ^ n is n times the divisor of f.

@[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.