Documentation

Mathlib.Analysis.Meromorphic.Divisor

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 #

Definition of the Divisor #

noncomputable def MeromorphicOn.divisor {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] (f : π•œ β†’ E) (U : Set π•œ) :

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
Instances For
    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β‚€.

    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) :

    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 : π•œ β†’ π•œ} :

    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.