Documentation

TauCeti.Geometry.Manifold.MFDeriv.Localized

Compactly supported functions with prescribed first derivative #

On a finite-dimensional Hausdorff real manifold, any value and continuous linear derivative at a point are realized by a globally smooth function supported in a prescribed neighborhood. The construction cuts off an affine function of the extended chart. It works for normed-space valued functions and also for manifolds with boundary.

This local first-jet realization allows, in particular, localized Hamiltonian perturbations with a prescribed differential without requiring a global coordinate chart.

Main results #

source
theorem TauCeti.exists_contMDiff_hasCompactSupport_mvfderiv_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [NormedAddCommGroup F] [NormedSpace ℝ F] (x : M) (c : F) (L : E →L[ℝ] F) {U : Set M} (hU : U ∈ nhds x) :
∃ (f : M → F), ContMDiff I (modelWithCornersSelf ℝ F) (↑⊤) f ∧ HasCompactSupport f ∧ tsupport f ⊆ U ∧ f x = c ∧ d% f x = L

Any prescribed value and derivative at a point of a finite-dimensional Hausdorff real manifold are realized by a smooth function compactly supported in any chosen neighborhood.

source
theorem TauCeti.exists_contMDiffMap_mvfderiv_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [NormedAddCommGroup F] [NormedSpace ℝ F] (x : M) (c : F) (L : E →L[ℝ] F) :
∃ (f : ContMDiffMap I (modelWithCornersSelf ℝ F) M F ↑⊤), f x = c ∧ d% ⇑f x = L

Any prescribed value and derivative at a point of a finite-dimensional Hausdorff real manifold are realized by a bundled smooth map.