Cutting a function off in a chart

Let u be a C¹ real function on a manifold without boundary and b a smooth bump function on the model space, centred at the chart image of a point c, whose closed support ball lies in the target of the extended chart at c. The product y ↦ b y * u ((extChartAt I c).symm y) is then a compactly supported C¹ function on the model space, agreeing with the coordinate expression of u where b = 1. This is the standard way to localize an estimate from the model space to a manifold. This file records its regularity and the bound on its derivative.

Conversely, a compactly supported function on the model space whose support lies in the chart target is the coordinate expression of a compactly supported function on the manifold, extended by zero outside the chart. This is the standard way to transplant a test function from the model space to a manifold.

Main results

• ContDiffBump.contDiff_mul_comp_extChartAt_symm: the cut-off coordinate expression is C¹.
• ContDiffBump.norm_fderiv_mul_comp_extChartAt_symm_le: in the chart target its derivative is bounded by the derivative of the coordinate expression plus G |u|, where G bounds the derivative of the bump.
• ContDiffBump.fderiv_mul_comp_extChartAt_symm_eq_zero: its derivative vanishes outside the closed support ball of the bump.
• TauCeti.Manifold.exists_contMDiff_comp_extChartAt_symm_eq: a C^n function on the model space with compact support in the chart target is the coordinate expression of a compactly supported C^n function on the manifold.

theorem ContDiffBump.contDiff_mul_comp_extChartAt_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {c : M} (b : ContDiffBump (↑(extChartAt I c) c)) {u : M → ℝ} [I.Boundaryless] [IsManifold I 1 M] (hb : Metric.closedBall (↑(extChartAt I c) c) b.rOut ⊆ (extChartAt I c).target) (hu : ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 u) : ContDiff ℝ 1 fun (y : E) => ↑b y * u (↑(extChartAt I c).symm y)

A bump function whose closed support ball lies in the chart target, times the coordinate expression of a C¹ function, is a C¹ function on the model space.

theorem ContDiffBump.norm_fderiv_mul_comp_extChartAt_symm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {c : M} (b : ContDiffBump (↑(extChartAt I c) c)) {u : M → ℝ} [I.Boundaryless] [IsManifold I 1 M] (hu : ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 u) {G : ℝ} (hG : ∀ (y : E), ‖fderiv ℝ (↑b) y‖ ≤ G) {y : E} (hy : y ∈ (extChartAt I c).target) : ‖fderiv ℝ (fun (y : E) => ↑b y * u (↑(extChartAt I c).symm y)) y‖ ≤ ‖fderiv ℝ (fun (y : E) => u (↑(extChartAt I c).symm y)) y‖ + G * |u (↑(extChartAt I c).symm y)|

The derivative of the cut-off coordinate expression at a point of the chart target is bounded by the derivative of the coordinate expression plus G |u|, where G bounds the derivative of the bump.

theorem ContDiffBump.fderiv_mul_comp_extChartAt_symm_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {c : M} (b : ContDiffBump (↑(extChartAt I c) c)) {u : M → ℝ} {y : E} (hy : y ∉ Metric.closedBall (↑(extChartAt I c) c) b.rOut) : fderiv ℝ (fun (y : E) => ↑b y * u (↑(extChartAt I c).symm y)) y = 0

The cut-off coordinate expression has zero derivative outside the closed support ball of the bump.

theorem TauCeti.Manifold.exists_contMDiff_comp_extChartAt_symm_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] {n : WithTop ℕ∞} [IsManifold I n M] {c : M} {w : E → F} (hw : ContDiff 𝕜 n w) (hwc : HasCompactSupport w) (hwt : tsupport w ⊆ (extChartAt I c).target) : ∃ (u : M → F), ContMDiff I (modelWithCornersSelf 𝕜 F) n u ∧ HasCompactSupport u ∧ tsupport u ⊆ ↑(extChartAt I c).symm '' tsupport w ∧ ∀ y ∈ (extChartAt I c).target, u (↑(extChartAt I c).symm y) = w y

Transplanting a function from a chart. A C^n function w on the model space whose support is a compact subset of the target of the extended chart at c is, on that target, the coordinate expression of a compactly supported C^n function u on M whose support lies in the chart preimage of the support of w.