23.6. ResidueTheorem.ResidueLedgerTransport🔗

Jacobians.ResidueTheorem.ResidueLedgerTransport — source

pairRead

The pair-form coefficient h·dg₀ read in the canonical chart at y: (h∘chart⁻¹)·(g₀∘chart⁻¹)′. (pairFormResidue g₀ h a = resAt (pairRead g₀ h a) (chart a a).)

noncomputable def pairRead (g₀ h : MeromorphicFunction X) (y : X) : ℂ → ℂ

ReadsAnalyticAt

Honest own-chart analyticity of BOTH reads at x (the good locus of the ledger; its complement is finite by MeromorphicFunction.finite_nonAnalyticAt).

def ReadsAnalyticAt (g₀ h : MeromorphicFunction X) (x : X) : Prop

finite_not_readsAnalyticAt

The bad locus {¬ReadsAnalyticAt} is finite (union of the two finite analytic-bad sets).

theorem finite_not_readsAnalyticAt (g₀ h : MeromorphicFunction X) :
    {x : X | ¬ ReadsAnalyticAt g₀ h x}.Finite

analyticAt_read_of_ownChart

Chart-read analyticity transports from the own chart to ANY chart containing the point.

theorem analyticAt_read_of_ownChart {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {f : X → ℂ} {x y : X}
    (hxy : x ∈ (chartAt (H := ℂ) y).source)
    (hx : AnalyticAt ℂ (fun z => f ((chartAt (H := ℂ) x).symm z)) ((chartAt (H := ℂ) x) x)) :
    AnalyticAt ℂ (fun z => f ((chartAt (H := ℂ) y).symm z)) ((chartAt (H := ℂ) y) x)

analyticAt_pairRead

Off the bad set the pair coefficient is holomorphic in every chart (the chart-uniform Claim A): pairRead g₀ h y is AnalyticAt at chart_y x for every good x ∈ source_y.

theorem analyticAt_pairRead {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {g₀ h : MeromorphicFunction X} {x y : X}
    (hx : ReadsAnalyticAt g₀ h x) (hxy : x ∈ (chartAt (H := ℂ) y).source) :
    AnalyticAt ℂ (pairRead g₀ h y) ((chartAt (H := ℂ) y) x)

eventually_chart_window

Eventually near chart_y x, points stay in the chart target and their preimages stay in any chart source containing x — the germ window for all the transition computations below.

theorem eventually_chart_window {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {x y y' : X}
    (hxy : x ∈ (chartAt (H := ℂ) y).source) (hxy' : x ∈ (chartAt (H := ℂ) y').source) :
    ∀ᶠ w in 𝓝 ((chartAt (H := ℂ) y) x),
      w ∈ (chartAt (H := ℂ) y).target
        ∧ (chartAt (H := ℂ) y).symm w ∈ (chartAt (H := ℂ) y').source

read_eventuallyEq_read_comp_transition

On the germ window, a read through chart y is the read through chart y' composed with the transition T = chart_{y'} ∘ chart_y⁻¹.

theorem read_eventuallyEq_read_comp_transition {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f : X → ℂ) {x y y' : X}
    (hxy : x ∈ (chartAt (H := ℂ) y).source) (hxy' : x ∈ (chartAt (H := ℂ) y').source) :
    (fun w => f ((chartAt (H := ℂ) y).symm w)) =ᶠ[𝓝 ((chartAt (H := ℂ) y) x)]
      (fun w => f ((chartAt (H := ℂ) y').symm w))
        ∘ (fun w => (chartAt (H := ℂ) y') ((chartAt (H := ℂ) y).symm w))

pairRead_transform

The (1,0)-coefficient transformation rule (Claim B): at a good point x in the overlap of two chart sources, pairRead through y is pairRead through y' at the transported point, times the transition derivative.

theorem pairRead_transform {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {g₀ h : MeromorphicFunction X} {x y y' : X}
    (hx : ReadsAnalyticAt g₀ h x)
    (hxy : x ∈ (chartAt (H := ℂ) y).source) (hxy' : x ∈ (chartAt (H := ℂ) y').source) :
    pairRead g₀ h y ((chartAt (H := ℂ) y) x)
      = pairRead g₀ h y' ((chartAt (H := ℂ) y') x)
        * deriv (fun w => (chartAt (H := ℂ) y') ((chartAt (H := ℂ) y).symm w))
            ((chartAt (H := ℂ) y) x)

contDiffAt_complexRead

The complexified chart read of a smooth real function is C^∞ at chart-target points.

theorem contDiffAt_complexRead {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {v : X → ℝ}
    (hv : ContMDiff 𝓘(ℝ, ℂ) 𝓘(ℝ, ℝ) (⊤ : ℕ∞) v) (y : X) {z : ℂ}
    (hz : z ∈ (chartAt (H := ℂ) y).target) :
    ContDiffAt ℝ (⊤ : ℕ∞) (fun w => ((v ((chartAt (H := ℂ) y).symm w) : ℝ) : ℂ)) z

differentiableAt_complexRead

Real differentiability of the complexified chart read at target points.

theorem differentiableAt_complexRead {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {v : X → ℝ}
    (hv : ContMDiff 𝓘(ℝ, ℂ) 𝓘(ℝ, ℝ) (⊤ : ℕ∞) v) (y : X) {z : ℂ}
    (hz : z ∈ (chartAt (H := ℂ) y).target) :
    DifferentiableAt ℝ (fun w => ((v ((chartAt (H := ℂ) y).symm w) : ℝ) : ℂ)) z

continuousAt_dbar_complexRead

Continuity of the ∂̄ of a smooth chart read at target points.

theorem continuousAt_dbar_complexRead {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {v : X → ℝ}
    (hv : ContMDiff 𝓘(ℝ, ℂ) 𝓘(ℝ, ℝ) (⊤ : ℕ∞) v) (y : X) {z : ℂ}
    (hz : z ∈ (chartAt (H := ℂ) y).target) :
    ContinuousAt (DbarDisk.dbar
      (fun w => ((v ((chartAt (H := ℂ) y).symm w) : ℝ) : ℂ))) z

dbar_complexRead_eq_zero_of_eventually_const

If v is locally constant at the underlying point, the ∂̄ of its chart read vanishes AT the chart point (and indeed near it).

theorem dbar_complexRead_eq_zero_of_eventually_const {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X]
    {v : X → ℝ} {y : X} {z : ℂ}
    (hz : z ∈ (chartAt (H := ℂ) y).target)
    (hconst : ∃ cst : ℝ, ∀ᶠ x' in 𝓝 ((chartAt (H := ℂ) y).symm z), v x' = cst) :
    DbarDisk.dbar (fun w => ((v ((chartAt (H := ℂ) y).symm w) : ℝ) : ℂ)) z = 0

ledgerIntegrand

The canonical ledger integrand in the chart at y, over the window V ⊆ X:

𝟙_{chart''V} · (P∘chart⁻¹) · ∂̄(v∘chart⁻¹) · pairRead

— scalar field × (0,1)-cutoff-form coefficient × (1,0)-pair-form coefficient. The indicator makes the formula globally defined (the chart inverse takes junk values outside the target).

noncomputable def ledgerIntegrand (g₀ h : MeromorphicFunction X) (P : X → ℂ) (v : X → ℝ)
    (y : X) (V : Set X) : ℂ → ℂ

symm_mem_of_mem_image

Membership unpacking for chart images of subsets of the source.

theorem symm_mem_of_mem_image {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {y : X} {V : Set X} (hV : V ⊆ (chartAt (H := ℂ) y).source)
    {z : ℂ} (hz : z ∈ (chartAt (H := ℂ) y) '' V) :
    z ∈ (chartAt (H := ℂ) y).target ∧ (chartAt (H := ℂ) y).symm z ∈ V

ledgerIntegrand_congr_superset

Window change: the indicator window may be replaced by a larger one as long as on the difference either the scalar field vanishes (pointwise) or the cutoff is locally constant.

theorem ledgerIntegrand_congr_superset {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (g₀ h : MeromorphicFunction X) (P : X → ℂ) (v : X → ℝ)
    (y : X) {V W : Set X} (hVW : V ⊆ W) (hW : W ⊆ (chartAt (H := ℂ) y).source)
    (hkill : ∀ x ∈ W, x ∉ V → P x = 0 ∨ ∃ cst : ℝ, ∀ᶠ x' in 𝓝 x, v x' = cst) :
    ledgerIntegrand g₀ h P v y V = ledgerIntegrand g₀ h P v y W

sum_ledgerIntegrand

Cutoff aggregation: a finite sum of ledger integrands over a family of cutoffs is the ledger integrand of the summed cutoff (pointwise; the ∂̄ is additive on smooth reads).

theorem sum_ledgerIntegrand {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {ι : Type*} (s : Finset ι) (vF : ι → X → ℝ)
    (hvF : ∀ i ∈ s, ContMDiff 𝓘(ℝ, ℂ) 𝓘(ℝ, ℝ) (⊤ : ℕ∞) (vF i))
    (g₀ h : MeromorphicFunction X) (P : X → ℂ) (y : X) {V : Set X}
    (hV : V ⊆ (chartAt (H := ℂ) y).source) (z : ℂ) :
    ∑ i ∈ s, ledgerIntegrand g₀ h P (vF i) y V z
      = ledgerIntegrand g₀ h P (fun x => ∑ i ∈ s, vF i x) y V z

integral_ledgerIntegrand_transport

THE CHART-TRANSPORT INVARIANCE. The total plane integral of the ledger integrand does not depend on the chart it is read in: for an open window V inside both chart sources, and g₀/h-reads honestly analytic on V off a finite set,

∫_ℂ ledgerIntegrand g₀ h P v y V = ∫_ℂ ledgerIntegrand g₀ h P v y' V.

Holomorphic change of variables along the transition T = chart_{y'} ∘ chart_y⁻¹: the ∂̄-chain-rule factor conj T′ and the pairRead factor T′ combine exactly into the real Jacobian |T′|²; the finitely many bad points are a null set.

theorem integral_ledgerIntegrand_transport {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (g₀ h : MeromorphicFunction X)
    (P : X → ℂ) (v : X → ℝ) (hv : ContMDiff 𝓘(ℝ, ℂ) 𝓘(ℝ, ℝ) (⊤ : ℕ∞) v)
    {y y' : X} {V : Set X} (hVopen : IsOpen V)
    (hVy : V ⊆ (chartAt (H := ℂ) y).source) (hVy' : V ⊆ (chartAt (H := ℂ) y').source)
    {E : Set X} (hE : E.Finite)
    (hgood : ∀ x ∈ V, x ∉ E → ReadsAnalyticAt g₀ h x) :
    ∫ z, ledgerIntegrand g₀ h P v y V z = ∫ w, ledgerIntegrand g₀ h P v y' V w

continuous_ledgerIntegrand

Continuity of the ledger integrand. Bought pointwise: honest continuity at good interior points; local vanishing at bad points and outside a compact core K (the scalar field vanishes or the cutoff is locally constant there); eventual vanishing outside the window (neighbourhoods avoid the compact core image).

theorem continuous_ledgerIntegrand {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (g₀ h : MeromorphicFunction X)
    {P : X → ℂ} (hP : Continuous P)
    {v : X → ℝ} (hv : ContMDiff 𝓘(ℝ, ℂ) 𝓘(ℝ, ℝ) (⊤ : ℕ∞) v)
    {y : X} {V : Set X} (hVopen : IsOpen V) (hVsub : V ⊆ (chartAt (H := ℂ) y).source)
    {K : Set X} (hK : IsCompact K) (hKV : K ⊆ V)
    (hsupp : ∀ x ∈ V, x ∉ K → P x = 0 ∨ ∃ cst : ℝ, ∀ᶠ x' in 𝓝 x, v x' = cst)
    (hbad : ∀ x ∈ V, ¬ ReadsAnalyticAt g₀ h x →
      (∀ᶠ x' in 𝓝 x, P x' = 0) ∨ ∃ cst : ℝ, ∀ᶠ x' in 𝓝 x, v x' = cst) :
    Continuous (ledgerIntegrand g₀ h P v y V)

hasCompactSupport_ledgerIntegrand

Compact support of the ledger integrand (support inside the chart image of the core).

theorem hasCompactSupport_ledgerIntegrand {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (g₀ h : MeromorphicFunction X)
    (P : X → ℂ) {v : X → ℝ}
    {y : X} {V : Set X} (hVsub : V ⊆ (chartAt (H := ℂ) y).source)
    {K : Set X} (hK : IsCompact K) (hKV : K ⊆ V)
    (hsupp : ∀ x ∈ V, x ∉ K → P x = 0 ∨ ∃ cst : ℝ, ∀ᶠ x' in 𝓝 x, v x' = cst) :
    HasCompactSupport (ledgerIntegrand g₀ h P v y V)

integrable_ledgerIntegrand

Integrability of the ledger integrand (continuity + compact support).

theorem integrable_ledgerIntegrand {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (g₀ h : MeromorphicFunction X)
    {P : X → ℂ} (hP : Continuous P)
    {v : X → ℝ} (hv : ContMDiff 𝓘(ℝ, ℂ) 𝓘(ℝ, ℝ) (⊤ : ℕ∞) v)
    {y : X} {V : Set X} (hVopen : IsOpen V) (hVsub : V ⊆ (chartAt (H := ℂ) y).source)
    {K : Set X} (hK : IsCompact K) (hKV : K ⊆ V)
    (hsupp : ∀ x ∈ V, x ∉ K → P x = 0 ∨ ∃ cst : ℝ, ∀ᶠ x' in 𝓝 x, v x' = cst)
    (hbad : ∀ x ∈ V, ¬ ReadsAnalyticAt g₀ h x →
      (∀ᶠ x' in 𝓝 x, P x' = 0) ∨ ∃ cst : ℝ, ∀ᶠ x' in 𝓝 x, v x' = cst) :
    Integrable (ledgerIntegrand g₀ h P v y V) volume