Documentation

Mathlib.Analysis.Analytic.Meromorphic

Meromorphic functions #

Main statements:

def MeromorphicAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜E) (x : 𝕜) :

Meromorphy of f at x (more precisely, on a punctured neighbourhood of x; the value at x itself is irrelevant).

Equations
Instances For
    theorem AnalyticAt.meromorphicAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) :
    theorem MeromorphicAt.id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (x : 𝕜) :
    theorem MeromorphicAt.const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (e : E) (x : 𝕜) :
    MeromorphicAt (fun (x : 𝕜) => e) x
    theorem MeromorphicAt.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {g : 𝕜E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    theorem MeromorphicAt.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜𝕜} {g : 𝕜E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    theorem MeromorphicAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {g : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    theorem MeromorphicAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} (hf : MeromorphicAt f x) :
    @[simp]
    theorem MeromorphicAt.neg_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} :
    theorem MeromorphicAt.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {g : 𝕜E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    theorem MeromorphicAt.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {g : 𝕜E} {x : 𝕜} (hf : MeromorphicAt f x) (hfg : f =ᶠ[nhdsWithin x {x}] g) :

    With our definitions, MeromorphicAt f x depends only on the values of f on a punctured neighbourhood of x (not on f x)

    theorem MeromorphicAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) :
    @[simp]
    theorem MeromorphicAt.inv_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} :
    theorem MeromorphicAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {g : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    theorem MeromorphicAt.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ) :
    theorem MeromorphicAt.zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ) :
    noncomputable def MeromorphicAt.order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} (hf : MeromorphicAt f x) :

    The order of vanishing of a meromorphic function, as an element of ℤ ∪ ∞ (to include the case of functions identically 0 near x).

    Equations
    Instances For
      theorem MeromorphicAt.order_eq_top_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} (hf : MeromorphicAt f x) :
      MeromorphicAt.order hf = ∀ᶠ (z : 𝕜) in nhdsWithin x {x}, f z = 0
      theorem MeromorphicAt.order_eq_int_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} (hf : MeromorphicAt f x) (n : ) :
      MeromorphicAt.order hf = n ∃ (g : 𝕜E), AnalyticAt 𝕜 g x g x 0 ∀ᶠ (z : 𝕜) in nhdsWithin x {x}, f z = (z - x) ^ n g z
      theorem AnalyticAt.meromorphicAt_order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) :

      Compatibility of notions of order for analytic and meromorphic functions.

      theorem MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {x : 𝕜} :
      MeromorphicAt f x ∃ (n : ) (g : 𝕜E), AnalyticAt 𝕜 g x ∀ᶠ (z : 𝕜) in nhdsWithin x {x}, f z = (z - x) ^ n g z
      def MeromorphicOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜E) (U : Set 𝕜) :

      Meromorphy of a function on a set.

      Equations
      Instances For
        theorem AnalyticOn.meromorphicOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {U : Set 𝕜} (hf : AnalyticOn 𝕜 f U) :
        theorem MeromorphicOn.id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} :
        theorem MeromorphicOn.const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (e : E) {U : Set 𝕜} :
        MeromorphicOn (fun (x : 𝕜) => e) U
        theorem MeromorphicOn.mono_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {U : Set 𝕜} (hf : MeromorphicOn f U) {V : Set 𝕜} (hv : V U) :
        theorem MeromorphicOn.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {g : 𝕜E} {U : Set 𝕜} (hf : MeromorphicOn f U) (hg : MeromorphicOn g U) :
        theorem MeromorphicOn.sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {g : 𝕜E} {U : Set 𝕜} (hf : MeromorphicOn f U) (hg : MeromorphicOn g U) :
        theorem MeromorphicOn.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {U : Set 𝕜} (hf : MeromorphicOn f U) :
        @[simp]
        theorem MeromorphicOn.neg_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {U : Set 𝕜} :
        theorem MeromorphicOn.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : 𝕜𝕜} {f : 𝕜E} {U : Set 𝕜} (hs : MeromorphicOn s U) (hf : MeromorphicOn f U) :
        theorem MeromorphicOn.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {t : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (ht : MeromorphicOn t U) :
        theorem MeromorphicOn.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) :
        @[simp]
        theorem MeromorphicOn.inv_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} :
        theorem MeromorphicOn.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {t : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (ht : MeromorphicOn t U) :
        theorem MeromorphicOn.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ) :
        theorem MeromorphicOn.zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : 𝕜𝕜} {U : Set 𝕜} (hs : MeromorphicOn s U) (n : ) :
        theorem MeromorphicOn.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜E} {g : 𝕜E} {U : Set 𝕜} (hf : MeromorphicOn f U) (h_eq : Set.EqOn f g U) (hu : IsOpen U) :