23.7. ResidueTheorem.ResidueStokesCoverPoU🔗

Jacobians.ResidueTheorem.ResidueStokesCoverPoU — source

iUnion_chartOpen_coverCenter_eq

The genuine chart cover covers X (inner shrinkings already cover, and innerShrunkChart ⊆ chartOpen).

theorem iUnion_chartOpen_coverCenter_eq' {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] :
    (⋃ j : Fin ((chartCover : Finset X).card), chartOpen (X := X) (coverCenter j))
      = Set.univ

exists_coverPoU

A smooth PoU subordinate to the genuine chart cover, summing to 1 on all of X.

theorem exists_coverPoU :
    ∃ ρ : SmoothPartitionOfUnity (Fin ((chartCover : Finset X).card)) 𝓘(ℝ, ℂ) X Set.univ,
      ρ.IsSubordinate (fun j => chartOpen (X := X) (coverCenter j))

coverPoU

The chosen chart-cover PoU.

noncomputable def coverPoU :
    SmoothPartitionOfUnity (Fin ((chartCover : Finset X).card)) 𝓘(ℝ, ℂ) X Set.univ

coverPoU_subordinate

theorem coverPoU_subordinate :
    (coverPoU (X := X)).IsSubordinate (fun j => chartOpen (X := X) (coverCenter j))

coverPoU_tsupport_subset

tsupport ρ_j ⊆ chartOpen (coverCenter j).

theorem coverPoU_tsupport_subset (j : Fin ((chartCover : Finset X).card)) :
    tsupport (coverPoU (X := X) j) ⊆ chartOpen (X := X) (coverCenter j)

sum_coverPoU_eq_one

∑ j, ρ_j x = 1 at EVERY x : X.

theorem sum_coverPoU_eq_one (x : X) : ∑ j, (coverPoU (X := X)) j x = 1

contMDiff_coverPoU

theorem contMDiff_coverPoU (j : Fin ((chartCover : Finset X).card)) :
    ContMDiff 𝓘(ℝ, ℂ) 𝓘(ℝ, ℝ) (⊤ : ℕ∞) (coverPoU (X := X) j)

coverRhoC

The complexified PoU component ρC_j : X → ℂ.

noncomputable def coverRhoC (j : Fin ((chartCover : Finset X).card)) : X → ℂ

continuous_coverRhoC

theorem continuous_coverRhoC (j : Fin ((chartCover : Finset X).card)) :
    Continuous (coverRhoC (X := X) j)

sum_coverRhoC_eq_one

theorem sum_coverRhoC_eq_one (x : X) : ∑ j, coverRhoC (X := X) j x = 1

coverRhoC_eq_zero_of_notMem

theorem coverRhoC_eq_zero_of_notMem (j : Fin ((chartCover : Finset X).card)) {x : X}
    (hx : x ∉ tsupport (coverPoU (X := X) j)) : coverRhoC (X := X) j x = 0

coverPoU_eventually_zero_of_notMem

Off tsupport ρ_j, the (real) PoU component is locally ≡ 0 (the cst-germ form consumed by the ledger kill conditions).

theorem coverPoU_eventually_zero_of_notMem (j : Fin ((chartCover : Finset X).card)) {x : X}
    (hx : x ∉ tsupport (coverPoU (X := X) j)) :
    ∀ᶠ x' in 𝓝 x, (coverPoU (X := X) j) x' = 0

isCompact_tsupport_coverPoU

tsupport ρ_j is compact (X is compact).

theorem isCompact_tsupport_coverPoU (j : Fin ((chartCover : Finset X).card)) :
    IsCompact (tsupport (coverPoU (X := X) j))