11.8. Meromorphic.MeromorphicNFRepair🔗

Jacobians.Meromorphic.MeromorphicNFRepair — source

untop₀_nonneg_iff

The integer order .untop₀ is ≥ 0 iff the raw WithTop ℤ order is ≥ 0. (⊤ ↦ 0 ≥ 0.)

theorem untop₀_nonneg_iff {α : WithTop ℤ} : (0 : ℤ) ≤ α.untop₀ ↔ 0 ≤ α

_root_.OpenPartialHomeomorph.tendsto_nhdsNE

An open partial homeomorphism carries the punctured neighborhood of a source point to the punctured neighborhood of its image: Tendsto φ (𝓝[≠] x) (𝓝[≠] (φ x)) for x ∈ φ.source. (Continuity gives the unpunctured limit; injectivity on the source removes the center.)

theorem _root_.OpenPartialHomeomorph.tendsto_nhdsNE {Y Z : Type*} [TopologicalSpace Y]
    [TopologicalSpace Z] (φ : OpenPartialHomeomorph Y Z) {x : Y} (hx : x ∈ φ.source) :
    Tendsto φ (𝓝[{x}ᶜ] x) (𝓝[{φ x}ᶜ] (φ x))

toMeromorphicNFAt_self_eq_limUnder

For a meromorphic function F : ℂ → ℂ whose order at w is ≥ 0, the value of its normal-form representative at the center equals the limit along 𝓝[≠] w.

theorem toMeromorphicNFAt_self_eq_limUnder {F : ℂ → ℂ} {w c : ℂ}
    (hF : MeromorphicAt F w) (ho : 0 ≤ meromorphicOrderAt F w)
    (hc : Tendsto F (𝓝[≠] w) (𝓝 c)) :
    toMeromorphicNFAt F w w = c

MeromorphicAt.exists_isOpen_meromorphicOn

From meromorphy of F *at* a point z, extract an open neighborhood V ∋ z on which F is meromorphic, and moreover analytic away from z. (Mathlib MeromorphicAt.eventually_analyticAt: F is analytic on a punctured neighborhood; together with meromorphy at z itself this is meromorphy on a full open V.)

theorem MeromorphicAt.exists_isOpen_meromorphicOn {F : ℂ → ℂ} {z : ℂ} (hF : MeromorphicAt F z) :
    ∃ V : Set ℂ, IsOpen V ∧ z ∈ V ∧ MeromorphicOn F V ∧
      ∀ w ∈ V, w ≠ z → AnalyticAt ℂ F w

analyticAt_toMeromorphicNFOn

The normal-form representative toMeromorphicNFOn F V is analytic at each point of V where the order of F is ≥ 0 (normal form + nonneg order ⟹ analytic).

theorem analyticAt_toMeromorphicNFOn {F : ℂ → ℂ} {V : Set ℂ} (hF : MeromorphicOn F V)
    (hord : ∀ w ∈ V, 0 ≤ meromorphicOrderAt F w) {w₀ : ℂ} (hw₀ : w₀ ∈ V) :
    AnalyticAt ℂ (toMeromorphicNFOn F V) w₀