14.11. Cech.MeromorphicAnalyticBadSet🔗

Jacobians.Cech.MeromorphicAnalyticBadSet — source

IsMeromorphic.mul

Meromorphy is preserved by pointwise products (MeromorphicAt.mul in every chart).

theorem IsMeromorphic.mul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ}
    (hf : IsMeromorphic X f) (hg : IsMeromorphic X g) :
    IsMeromorphic X (f * g)

MeromorphicFunction.mul_toFun

@[simp] theorem MeromorphicFunction.mul_toFun {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f g : MeromorphicFunction X) :
    (f * g).toFun = f.toFun * g.toFun

finite_of_forall_eventually_nhdsNE_notMem

A set avoided by a punctured neighbourhood of every point is finite (in a compact space). The indicator of S then has locally finite support, and LocallyFiniteSupport's compactness lemma finishes. (This is the exists_form_divisor finiteness pattern, extracted for sets.)

theorem finite_of_forall_eventually_nhdsNE_notMem {Y : Type*} [TopologicalSpace Y]
    [CompactSpace Y] {S : Set Y} (h : ∀ x : Y, ∀ᶠ y in 𝓝[≠] x, y ∉ S) : S.Finite

MeromorphicFunction.eventually_analyticAt_ownChart

Honest analyticity on a punctured neighbourhood, in each point's own chart. Around every x, a global meromorphic function is AnalyticAt (junk-free, value included) at every nearby point y ≠ x, read in y's OWN canonical chart. Mathlib's MeromorphicAt.eventually_analyticAt gives analyticity in the chart at x; the chart-transition analyticity (Jacobians.Dolbeault.analyticAt_chart_change) transports it to y's chart.

theorem MeromorphicFunction.eventually_analyticAt_ownChart (f : MeromorphicFunction X) (x : X) :
    ∀ᶠ y in 𝓝[≠] x,
      AnalyticAt ℂ (fun z => f.toFun ((chartAt (H := ℂ) y).symm z)) ((chartAt (H := ℂ) y) y)

MeromorphicFunction.finite_nonAnalyticAt

The analytic-bad set of a meromorphic function is FINITE. The set of points where the chart pullback of f fails honest AnalyticAt (genuine poles AND removable-singularity toFun-junk) is isolated (eventually_analyticAt_ownChart), hence finite on the compact X. This is the finite enlargement that feeds a MeromorphicFunction into the analyticity hypothesis of residueTheorem_unconditional.

theorem MeromorphicFunction.finite_nonAnalyticAt (f : MeromorphicFunction X) :
    {x : X | ¬ AnalyticAt ℂ (fun z => f.toFun ((chartAt (H := ℂ) x).symm z))
      ((chartAt (H := ℂ) x) x)}.Finite