17.11. DolbeaultComparison.LocalRealization🔗

Jacobians.DolbeaultComparison.LocalRealization — source

dePole

The "de-poled" function z ↦ (z - c)^{-k} · F(z) (multiply by (z-c)^{-k} to clear a pole of order ≤ k at c).

noncomputable def dePole (k : ℤ) (F : ℂ → ℂ) (c : ℂ) : ℂ → ℂ

laurentCoeff

The order-k Laurent coefficient of F at c: the punctured-neighbourhood limit of the de-poled function. When ord_c F ≥ k (so the de-pole has nonnegative order) this is the genuine coefficient a_k of (z-c)^k in the Laurent expansion; the junk value 0 otherwise.

noncomputable def laurentCoeff (k : ℤ) (F : ℂ → ℂ) (c : ℂ) : ℂ

meromorphicAt_zpow_sub

(· - c)^{-k} is meromorphic at c (a zpow of the analytic id - const).

theorem meromorphicAt_zpow_sub (k : ℤ) (c : ℂ) :
    MeromorphicAt (fun z => (z - c) ^ (-k)) c

meromorphicOrderAt_zpow_sub

The order of (· - c)^{-k} at c is -k (Mathlib's explicit witness).

theorem meromorphicOrderAt_zpow_sub (k : ℤ) (c : ℂ) :
    meromorphicOrderAt (fun z => (z - c) ^ (-k)) c = (-k : ℤ)

meromorphicAt_dePole

The de-pole is meromorphic at c when F is.

theorem meromorphicAt_dePole {k : ℤ} {F : ℂ → ℂ} {c : ℂ} (hF : MeromorphicAt F c) :
    MeromorphicAt (dePole k F c) c

meromorphicOrderAt_dePole

The order of the de-pole is -k + ord_c F (additivity of meromorphicOrderAt under mul).

theorem meromorphicOrderAt_dePole {k : ℤ} {F : ℂ → ℂ} {c : ℂ} (hF : MeromorphicAt F c) :
    meromorphicOrderAt (dePole k F c) c = (-k : ℤ) + meromorphicOrderAt F c

tendsto_dePole

Existence of the coefficient limit. If ord_c F ≥ k then the de-pole has nonnegative order, so it tends to the (well-defined) coefficient laurentCoeff k F c on the punctured neighbourhood.

theorem tendsto_dePole {k : ℤ} {F : ℂ → ℂ} {c : ℂ} (hF : MeromorphicAt F c)
    (hord : (k : WithTop ℤ) ≤ meromorphicOrderAt F c) :
    Tendsto (dePole k F c) (𝓝[≠] c) (𝓝 (laurentCoeff k F c))

dePole_add

The de-pole distributes over addition (pointwise).

theorem dePole_add (k : ℤ) (F G : ℂ → ℂ) (c : ℂ) :
    dePole k (F + G) c = dePole k F c + dePole k G c

dePole_smul

The de-pole commutes with scalar multiplication (pointwise).

theorem dePole_smul (k : ℤ) (s : ℂ) (F : ℂ → ℂ) (c : ℂ) :
    dePole k (s • F) c = s • dePole k F c

dePole_congr

The de-pole depends only on the germ of F at c.

theorem dePole_congr {k : ℤ} {F G : ℂ → ℂ} {c : ℂ} (h : F =ᶠ[𝓝[≠] c] G) :
    dePole k F c =ᶠ[𝓝[≠] c] dePole k G c

laurentCoeff_add

laurentCoeff is additive on functions of order ≥ k.

theorem laurentCoeff_add {k : ℤ} {F G : ℂ → ℂ} {c : ℂ}
    (hF : MeromorphicAt F c) (hG : MeromorphicAt G c)
    (hordF : (k : WithTop ℤ) ≤ meromorphicOrderAt F c)
    (hordG : (k : WithTop ℤ) ≤ meromorphicOrderAt G c) :
    laurentCoeff k (F + G) c = laurentCoeff k F c + laurentCoeff k G c

laurentCoeff_smul

laurentCoeff is ℂ-homogeneous on functions of order ≥ k.

theorem laurentCoeff_smul {k : ℤ} (s : ℂ) {F : ℂ → ℂ} {c : ℂ}
    (hF : MeromorphicAt F c) (hordF : (k : WithTop ℤ) ≤ meromorphicOrderAt F c) :
    laurentCoeff k (s • F) c = s • laurentCoeff k F c

laurentCoeff_congr

laurentCoeff depends only on the germ of F at c.

theorem laurentCoeff_congr {k : ℤ} {F G : ℂ → ℂ} {c : ℂ} (h : F =ᶠ[𝓝[≠] c] G) :
    laurentCoeff k F c = laurentCoeff k G c

laurentCoeff_eq_zero_iff

The kernel characterization (one-variable form). For F of order ≥ k at c, the order-k coefficient vanishes iff the order is *strictly* > k (i.e. the pole order is < k, so F already lies one order below). The de-pole has order -k + ord F ≥ 0, and its limit (laurentCoeff) is 0 iff that order is > 0 (tendsto_zero_iff/tendsto_ne_zero_iff).

theorem laurentCoeff_eq_zero_iff {k : ℤ} {F : ℂ → ℂ} {c : ℂ} (hF : MeromorphicAt F c)
    (hord : (k : WithTop ℤ) ≤ meromorphicOrderAt F c) :
    laurentCoeff k F c = 0 ↔ (k : WithTop ℤ) < meromorphicOrderAt F c

meromorphicOrderAt_zpow_self

The order of (· - c)^k at c is k (Mathlib's explicit witness, positive power form).

theorem meromorphicOrderAt_zpow_self (k : ℤ) (c : ℂ) :
    meromorphicOrderAt (fun z => (z - c) ^ k) c = (k : ℤ)

laurentCoeff_zpow_self

The witness coefficient is 1. The order-k Laurent coefficient of (· - c)^k at c is 1: the de-pole (z-c)^{-k}·(z-c)^k = (z-c)^0 = 1 off c, so its limit is 1.

theorem laurentCoeff_zpow_self (k : ℤ) (c : ℂ) :
    laurentCoeff k (fun z => (z - c) ^ k) c = 1

coeffWFn

The order-k coefficient of f : ↥W → ℂ at Pw : ↥W, in ↥W's chart.

noncomputable def coeffWFn {W : Opens X} (k : ℤ) (Pw : W) (f : W → ℂ) : ℂ

meromorphicAt_pullback

The chart pullback f ∘ (chartAt Pw).symm is meromorphic at the chart centre, for f meromorphic on ↥W.

theorem meromorphicAt_pullback {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {W : Opens X}
    {f : W → ℂ} (hf : IsMeromorphic (W : Type _) f)
    (Pw : W) : MeromorphicAt (f ∘ (chartAt (H := ℂ) Pw).symm) ((chartAt (H := ℂ) Pw) Pw)

coeffWFn_add

coeffWFn is additive on ↥W-functions of order ≥ k at Pw.

theorem coeffWFn_add {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] {W : Opens X} {k : ℤ}
    {Pw : W} {f g : W → ℂ}
    (hf : IsMeromorphic (W : Type _) f) (hg : IsMeromorphic (W : Type _) g)
    (hfo : (k : WithTop ℤ) ≤ ordU f Pw) (hgo : (k : WithTop ℤ) ≤ ordU g Pw) :
    coeffWFn k Pw (f + g) = coeffWFn k Pw f + coeffWFn k Pw g

coeffWFn_smul

coeffWFn is ℂ-homogeneous on ↥W-functions of order ≥ k at Pw.

theorem coeffWFn_smul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] {W : Opens X} {k : ℤ}
    {Pw : W} (s : ℂ) {f : W → ℂ}
    (hf : IsMeromorphic (W : Type _) f) (hfo : (k : WithTop ℤ) ≤ ordU f Pw) :
    coeffWFn k Pw (s • f) = s • coeffWFn k Pw f

coeffWFn_congr

coeffWFn depends only on the germ class (MGerm): if two representatives agree off a discrete set near every point, their coefficients at Pw agree (the relevant agreement is on 𝓝[≠] Pw, transported to the chart via the repo's eventually_comp_chart_iff').

theorem coeffWFn_congr {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] {W : Opens X} {k : ℤ}
    {Pw : W} {f g : W → ℂ}
    (h : f =ᶠ[𝓝[≠] Pw] g) : coeffWFn k Pw f = coeffWFn k Pw g

coeffWFn_eq_zero_iff

The kernel characterization on ↥W. For f meromorphic on ↥W with ordU f Pw ≥ k, the order-k coefficient at Pw vanishes iff ordU f Pw > k (one order lower pole).

theorem coeffWFn_eq_zero_iff {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {W : Opens X} {k : ℤ} {Pw : W} {f : W → ℂ}
    (hf : IsMeromorphic (W : Type _) f) (hord : (k : WithTop ℤ) ≤ ordU f Pw) :
    coeffWFn k Pw f = 0 ↔ (k : WithTop ℤ) < ordU f Pw

witnessFn

The witness section on ↥W: the k-th power of the centred chart coordinate at Pw.

noncomputable def witnessFn {W : Opens X} (Pw : W) (k : ℤ) : W → ℂ

witnessFn_pullback_eqOn

The chart pullback of the witness is exactly (z − c)^k on the chart target.

theorem witnessFn_pullback_eqOn {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {W : Opens X}
    (Pw : W) (k : ℤ) :
    Set.EqOn (witnessFn Pw k ∘ (chartAt (H := ℂ) Pw).symm)
      (fun z => (z - (chartAt (H := ℂ) Pw) Pw) ^ k) (chartAt (H := ℂ) Pw).target

witnessFn_pullback_eventuallyEq

The chart pullback of the witness agrees with (z − c)^k near the chart centre c.

theorem witnessFn_pullback_eventuallyEq {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {W : Opens X}
    (Pw : W) (k : ℤ) :
    (witnessFn Pw k ∘ (chartAt (H := ℂ) Pw).symm)
      =ᶠ[𝓝 ((chartAt (H := ℂ) Pw) Pw)] (fun z => (z - (chartAt (H := ℂ) Pw) Pw) ^ k)

witnessFn_meromorphicAt_center

The chart pullback of the witness is meromorphic at the chart centre (it agrees near c with (z−c)^k). This is the only meromorphy fact needed for the order/coefficient at Pw.

theorem witnessFn_meromorphicAt_center {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {W : Opens X}
    (Pw : W) (k : ℤ) :
    MeromorphicAt (witnessFn Pw k ∘ (chartAt (H := ℂ) Pw).symm) ((chartAt (H := ℂ) Pw) Pw)

ordU_witnessFn

The order of the witness at Pw is exactly k.

theorem ordU_witnessFn {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {W : Opens X}
    (Pw : W) (k : ℤ) :
    ordU (witnessFn Pw k) Pw = (k : ℤ)

coeffWFn_witnessFn

The witness coefficient is 1. The order-k Laurent coefficient of the witness at Pw equals 1 (its pullback is (z−c)^k, whose order-k coefficient is 1).

theorem coeffWFn_witnessFn {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {W : Opens X}
    (Pw : W) (k : ℤ) :
    coeffWFn k Pw (witnessFn Pw k) = 1

ordU_ge_of_mem_add_single

A section of 𝒪_{D+P} has order ≥ k = -(D P) - 1 at P (the membership bound at P).

theorem ordU_ge_of_mem_add_single {f : W → ℂ} (hP : P ∈ W)
    (hf : f ∈ OmegaD (D + Finsupp.single P 1) W) :
    ((-(D P) - 1 : ℤ) : WithTop ℤ) ≤ ordU f ⟨P, hP⟩

mem_OmegaD_iff_ordU_at_P

Membership reduction. For f ∈ 𝒪_{D+P}(W), f ∈ 𝒪_D(W) iff its order at P is at least k + 1 = -(D P). Away from P the order bounds for 𝒪_D and 𝒪_{D+P} coincide.

theorem mem_OmegaD_iff_ordU_at_P {f : W → ℂ} (hP : P ∈ W)
    (hf : f ∈ OmegaD (D + Finsupp.single P 1) W) :
    f ∈ OmegaD D W ↔ ((-(D P) : ℤ) : WithTop ℤ) ≤ ordU f ⟨P, hP⟩

coeffLin

The order-k coefficient functional 𝒪_{D+P}(W) →ₗ[ℂ] ℂ at P (k = -(D P) - 1). Linear because every section of 𝒪_{D+P} has order ≥ k at P (so coeffWFn is additive/homogeneous).

noncomputable def coeffLin :
    OmegaD (D + Finsupp.single P 1) W →ₗ[ℂ] ℂ where

coeffLin_apply

@[simp] theorem coeffLin_apply (f : OmegaD (D + Finsupp.single P 1) W) :
    coeffLin hP f = coeffWFn (-(D P) - 1) ⟨P, hP⟩ (f : W → ℂ)

coeffLin_eq_zero_iff

The kernel of coeffLin is exactly 𝒪_D(W) (the membership characterization). For f ∈ 𝒪_{D+P}(W), the order-k coefficient at P vanishes iff ordU f P > k iff f ∈ 𝒪_D(W).

theorem coeffLin_eq_zero_iff (f : OmegaD (D + Finsupp.single P 1) W) :
    coeffLin hP f = 0 ↔ (f : W → ℂ) ∈ OmegaD D W

OmegaD_le_add_single

𝒪_D(W) ⊆ 𝒪_{D+P}(W) (the order bound −(D+P) ≤ −D weakens), as a submodule inclusion of the function spaces.

theorem OmegaD_le_add_single : OmegaD D W ≤ OmegaD (D + Finsupp.single P 1) W

coeffGermFn

The order-k coefficient at P, lifted to the germ-class space MGerm W. Well-defined because coeffWFn depends only on the germ at P (and codiscreteWithin-agreement implies 𝓝[≠] Pw- agreement).

noncomputable def coeffGermFn (k : ℤ) (Pw : W) : MGerm W → ℂ

coeffGermFn_coe

@[simp] theorem coeffGermFn_coe {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {W : Opens X}
    (k : ℤ) (Pw : W) (f : W → ℂ) :
    coeffGermFn k Pw (toGerm W f) = coeffWFn k Pw f

coeffGermLin

The germ-class coefficient functional on 𝒪_{D+P}(W)-germs, OmegaDGerm (D+P) W →ₗ[ℂ] ℂ. The form the skyscraper coefficient arrow h0ToSky is built from (per-overlap; the global arrow is the matching family of these).

noncomputable def coeffGermLin :
    OmegaDGerm (D + Finsupp.single P 1) W →ₗ[ℂ] ℂ where

coeffGermFn_eq_zero_of_mem_OmegaDGerm

A germ in OmegaDGerm D W (image of 𝒪_D(W)) has vanishing order-k coefficient at P (it already lies one order below: ordU g P ≥ -(D P) = k + 1 > k).

theorem coeffGermFn_eq_zero_of_mem_OmegaDGerm {γ : MGerm W}
    (hγ : γ ∈ OmegaDGerm D W) :
    coeffGermFn (-(D P) - 1) ⟨P, hP⟩ γ = 0

ker_coeffGermLin

The kernel of the germ-class coefficient is exactly OmegaDGerm D W (the membership characterization at the germ level).

theorem ker_coeffGermLin :
    LinearMap.ker (coeffGermLin hP (D := D))
      = (OmegaDGerm D W).submoduleOf (OmegaDGerm (D + Finsupp.single P 1) W)