Extending finite-dimensional smooth germs

A function which is smooth, of finite or infinite order, on a neighbourhood of a point of a finite-dimensional real normed space agrees near that point with a globally smooth function of the same order. A smooth bump function performs the extension while preserving the original function near the base point. Since the bump is compactly supported, so is the representative, and a representative of order at least one is moreover globally Lipschitz.

These general calculus lemmas are used by the parameter-dependent ODE construction for the Lie-group exponential, and by the construction of a local flow out of the global solution of a globally Lipschitz field.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The exponential map".

theorem ContDiffOn.exists_contDiff_eventuallyEq_of_finiteDimensional {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] {n : ℕ∞} {f : E → F} {x : E} {s : Set E} (hfs : ContDiffOn ℝ (↑n) f s) (hs : s ∈ nhds x) : ∃ (g : E → F), ContDiff ℝ (↑n) g ∧ HasCompactSupport g ∧ g =ᶠ[nhds x] f

A function which is smooth on a neighbourhood of a point of a finite-dimensional real normed space agrees near that point with a compactly supported globally smooth function of the same order.

theorem ContDiffAt.exists_contDiff_eventuallyEq_of_finiteDimensional {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] (n : ℕ) {f : E → F} {x : E} (hf : ContDiffAt ℝ (↑n) f x) : ∃ (g : E → F), ContDiff ℝ (↑n) g ∧ HasCompactSupport g ∧ g =ᶠ[nhds x] f

A finite-order smooth germ on a finite-dimensional real normed space has a compactly supported globally smooth representative of the same order.

theorem ContDiffOn.exists_lipschitzWith_contDiff_eventuallyEq_of_finiteDimensional {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] {n : ℕ∞} {f : E → F} {x : E} {s : Set E} (hf : ContDiffOn ℝ (↑n + 1) f s) (hs : s ∈ nhds x) : ∃ (g : E → F) (K : NNReal), ContDiff ℝ (↑n + 1) g ∧ LipschitzWith K g ∧ g =ᶠ[nhds x] f

A function which is smooth of order at least one on a neighbourhood of a point of a finite-dimensional real normed space agrees near that point with a globally smooth and globally Lipschitz function of the same order: the compactly supported representative above has a bounded derivative.