Extending local smooth data to global smooth maps

Vector-valued data on a closed subset of a smooth manifold extend globally if they extend smoothly near every point of that subset. The extension can have topological support inside any prescribed open neighbourhood. This is the partition-of-unity step in extending velocities from an embedded submanifold to its ambient manifold.

The construction reduces to Mathlib's exists_contMDiffMap_forall_mem_convex_of_local, applied to singleton constraints on the closed set and zero constraints off an open neighbourhood whose closure lies in the prescribed one.

The pointwise form needs only one bump function: a function that is smooth on a neighbourhood of a point has the germ there of a globally smooth map (ContMDiffOn.exists_contMDiffMap_eventuallyEq), with no paracompactness assumption. A smooth map on an open subset, extended arbitrarily outside it, stays smooth on that subset (ContMDiffMap.contMDiffOn_extend). Reference: M. Hirsch, Differential Topology, Chapter 2, §2, and Chapter 8, §1.

theorem ContMDiffMap.contMDiffOn_extend {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {M' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} (U : TopologicalSpace.Opens M) (f : ContMDiffMap I I' (↥U) M' n) (g : M → M') : ContMDiffOn I I' n (Function.extend Subtype.val (⇑f) g) ↑U

Extending a smooth map on an open subset arbitrarily outside that subset gives a map that is smooth on the subset.

theorem ContMDiffOn.exists_contMDiffMap_eventuallyEq {E : Type u_1} {F : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] {n : ℕ∞} {U : Set M} {g : M → F} {x : M} (hg : ContMDiffOn I (modelWithCornersSelf ℝ F) (↑n) g U) (hU : U ∈ nhds x) : ∃ (G : ContMDiffMap I (modelWithCornersSelf ℝ F) M F ↑n), ⇑G =ᶠ[nhds x] g

A smooth germ is the germ of a global smooth map. A vector-valued function that is C^n on a neighbourhood of a point agrees near that point with a globally C^n map, namely its product with a smooth bump function supported in that neighbourhood.

theorem IsClosed.exists_contMDiffMap_eqOn {E : Type u_1} {F : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] {n : ℕ∞} [SigmaCompactSpace M] {s U : Set M} (hs : IsClosed s) {g : M → F} (hU : IsOpen U) (hsU : s ⊆ U) (hloc : ∀ x ∈ s, ∃ V ∈ nhds x, ∃ (g' : M → F), ContMDiffOn I (modelWithCornersSelf ℝ F) (↑n) g' V ∧ Set.EqOn g' g (s ∩ V)) : ∃ (G : ContMDiffMap I (modelWithCornersSelf ℝ F) M F ↑n), Set.EqOn (⇑G) g s ∧ tsupport ⇑G ⊆ U

Locally smoothly extendible vector-valued data on a closed set have a global C^n extension supported inside any prescribed open neighbourhood of that set. No regularity is required of the original function away from the closed set.