23.8. ResidueTheorem.ResidueStokesPoleBump🔗

Jacobians.ResidueTheorem.ResidueStokesPoleBump — source

exists_smooth_cutoff_profile

A C^∞ profile η with η ≡ 1 on (-∞, s₀] and η ≡ 0 on [s₁, ∞) (the smooth version of exists_cutoff_profile — same Real.smoothTransition construction).

theorem exists_smooth_cutoff_profile {s₀ s₁ : ℝ} (h : s₀ < s₁) :
    ∃ η : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) η ∧ (∀ s ≤ s₀, η s = 1) ∧ (∀ s, s₁ ≤ s → η s = 0)

PoleBumpData

Per-pole radial bump data over the finite set S (Forster 10.21's choice of coordinate neighbourhoods and cutoffs): for each a ∈ S, a radius ε a > 0 with the closed coordinate ball inside the chart target, whose X-side ball meets S only in {a}, and a smooth radial profile η a going 1 → 0 between (ε a)²/4 and (ε a)²/2.

structure PoleBumpData (S : Finset X) where

exists_poleBumpData

Existence of the bump data: chart targets are open, S is finite and X is T1, so each a ∈ S has a chart-image neighbourhood whose X-side ball avoids S \ {a}.

theorem exists_poleBumpData [T2Space X] [CompactSpace X] (S : Finset X) :
    Nonempty (PoleBumpData S)

poleBall

The X-side closed coordinate ball around the pole a.

noncomputable def poleBall (a : X) : Set X

poleBall_subset_source

theorem poleBall_subset_source {a : X} (ha : a ∈ S) :
    D.poleBall a ⊆ (chartAt (H := ℂ) a).source

isCompact_poleBall

theorem isCompact_poleBall {a : X} (ha : a ∈ S) : IsCompact (D.poleBall a)

mem_poleBall_iff

Membership of the chart image in the closed coordinate ball, for source points.

theorem mem_poleBall_iff {a : X} (ha : a ∈ S) {x : X}
    (hx : x ∈ (chartAt (H := ℂ) a).source) :
    x ∈ D.poleBall a ↔ (chartAt (H := ℂ) a) x ∈ closedBall ((chartAt (H := ℂ) a) a) (D.ε a)

bump

The radial bump at the pole a: η_a(normSq(chart_a x − chart_a a)) on the chart source, extended by 0 (the extension is smooth: the bump is supported in poleBall a).

noncomputable def bump (a : X) : X → ℝ

bump_eq_zero_of_notMem

The bump vanishes outside poleBall a (pointwise).

theorem bump_eq_zero_of_notMem {a : X} (ha : a ∈ S) {x : X} (hx : x ∉ D.poleBall a) :
    D.bump a x = 0

bump_eventually_one

The bump is ≡ 1 near its own pole.

theorem bump_eventually_one {a : X} (ha : a ∈ S) : ∀ᶠ x in 𝓝 a, D.bump a x = 1

bump_read_eventuallyEq

The chart-a read of bump a is the planar radial cutoff, near every target point.

theorem bump_read_eventuallyEq {a : X} (_ha : a ∈ S) {z : ℂ}
    (hz : z ∈ (chartAt (H := ℂ) a).target) :
    (fun w => ((D.bump a ((chartAt (H := ℂ) a).symm w) : ℝ) : ℂ)) =ᶠ[𝓝 z]
      fun w => ((D.η a (Complex.normSq (w - (chartAt (H := ℂ) a) a)) : ℝ) : ℂ)

bump_eventually_zero_of_ne

The bump of a is ≡ 0 near every other point of S (the separation field).

theorem bump_eventually_zero_of_ne {a : X} (ha : a ∈ S) {p : X} (hp : p ∈ S) (hne : p ≠ a) :
    ∀ᶠ x in 𝓝 p, D.bump a x = 0

bump_eventually_zero_of_notMem

The bump is ≡ 0 near every point outside poleBall a.

theorem bump_eventually_zero_of_notMem {a : X} (ha : a ∈ S) {p : X}
    (hp : p ∉ D.poleBall a) : ∀ᶠ x in 𝓝 p, D.bump a x = 0

totalBump

Forster's f₁ + ⋯ + f_n: the sum of the per-pole bumps.

noncomputable def totalBump : X → ℝ

totalBump_eventually_one

The total bump is ≡ 1 near every point of S (its own bump is 1, the others vanish — the separation field).

theorem totalBump_eventually_one {p : X} (hp : p ∈ S) :
    ∀ᶠ x in 𝓝 p, D.totalBump x = 1

contMDiff_bump

The bump is globally smooth (C^∞ chart read on the source; locally 0 off the compact poleBall).

theorem contMDiff_bump {a : X} (ha : a ∈ S) :
    ContMDiff 𝓘(ℝ, ℂ) 𝓘(ℝ, ℝ) (⊤ : ℕ∞) (D.bump a)

contMDiff_totalBump

theorem contMDiff_totalBump : ContMDiff 𝓘(ℝ, ℂ) 𝓘(ℝ, ℝ) (⊤ : ℕ∞) D.totalBump