Theorems · Theorem · complex analysis

MeromorphicOn.extract_zeros_poles

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  MeromorphicOn f U →
    (∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤) →
      (MeromorphicOn.divisor f U).support.Finite →
        ∃ g,
          AnalyticOnNhd 𝕜 g U ∧
            (∀ (u : ↑U), g ↑u ≠ 0) ∧
              f =ᶠ[Filter.codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x => x - u) ^ (MeromorphicOn.divisor f U) u) • g

If f is meromorphic on an open set U, if f is nowhere locally constant zero, and if the support of the divisor of f is finite, then there exists an analytic function g on U without zeros such that f is equivalent, modulo equality on codiscrete sets, to the product of g and the factorized rational function associated with the divisor of f.

Defined in

Mathlib.Analysis.Meromorphic.FactorizedRational

Cited by

4 results in Mathlib

Foundations

Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace