Smooth cutoffs for compact subsets

This module provides smooth, compactly supported cutoffs for compact subsets of a finite-dimensional real normed space. The cutoff is equal to one on a neighborhood of the compact set and has topological support in a prescribed open set, which is the localization step used for compact exhaustions in domain arguments. Taking differences of consecutive cutoffs along a compact exhaustion gives a decomposition of unity (not necessarily nonnegative) of an open set by compactly supported smooth functions, together with cutoffs equal to one on their supports which are locally finite in the open set (IsOpen.exists_contDiff_decomposition_cutoff); this is the gluing device for global approximation on a domain. Locally finite sums of smooth functions are smooth (contDiffAt_tsum_of_eventually_eq_zero).

It also provides radial cutoffs between two concentric closed balls of radii r < R whose gradient is at most c / (R - r) for a universal constant c, the quantitative form needed by iteration arguments over families of balls with shrinking gaps.

References

• L. C. Evans, Partial Differential Equations, §5.2.

theorem IsCompact.exists_contDiff_cutoff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K U : Set E} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (ψ : E → ℝ), ContDiff ℝ (↑⊤) ψ ∧ Set.range ψ ⊆ Set.Icc 0 1 ∧ K ⊆ interior (ψ ⁻¹' {1}) ∧ HasCompactSupport ψ ∧ tsupport ψ ⊆ U

A compact set contained in an open set admits a smooth cutoff equal to one on a neighborhood of the compact set.

The cutoff takes values in [0, 1], has compact support, and its topological support is contained in the prescribed open set.

theorem IsCompact.exists_contDiff_cutoff_with_bounds {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K U : Set E} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (ψ : E → ℝ) (M : ℝ), ContDiff ℝ (↑⊤) ψ ∧ Set.range ψ ⊆ Set.Icc 0 1 ∧ K ⊆ interior (ψ ⁻¹' {1}) ∧ HasCompactSupport ψ ∧ tsupport ψ ⊆ U ∧ 0 ≤ M ∧ (∀ (x : E), |ψ x| ≤ M) ∧ ∀ (x : E), ‖gradient ψ x‖ ≤ M

A compact set contained in an open set admits a smooth cutoff whose value and gradient are bounded by a common nonnegative constant.

theorem ContDiff.exists_abs_le_and_norm_gradient_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {ψ : E → ℝ} (hψ : ContDiff ℝ 1 ψ) (hcpt : HasCompactSupport ψ) : ∃ (M : ℝ), 0 ≤ M ∧ (∀ (x : E), |ψ x| ≤ M) ∧ ∀ (x : E), ‖gradient ψ x‖ ≤ M

A compactly supported C¹ function and its gradient are bounded by a common nonnegative constant.

theorem CompactExhaustion.exists_contDiff_cutoff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {Omega : TopologicalSpace.Opens E} (K : CompactExhaustion ↥Omega) (n : ℕ) : ∃ (ψ : E → ℝ), ContDiff ℝ (↑⊤) ψ ∧ Set.range ψ ⊆ Set.Icc 0 1 ∧ Subtype.val '' K n ⊆ interior (ψ ⁻¹' {1}) ∧ HasCompactSupport ψ ∧ tsupport ψ ⊆ Subtype.val '' interior (K (n + 1))

A compact-exhaustion term in an open set admits a smooth cutoff supported in the interior of the next term.

theorem IsOpen.exists_contDiff_decomposition_cutoff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {U : Set E} (hU : IsOpen U) : ∃ (ζ : ℕ → E → ℝ) (χ : ℕ → E → ℝ), (∀ (j : ℕ), ContDiff ℝ (↑⊤) (ζ j) ∧ HasCompactSupport (ζ j) ∧ tsupport (ζ j) ⊆ U) ∧ (∀ (j : ℕ), ContDiff ℝ (↑⊤) (χ j) ∧ HasCompactSupport (χ j) ∧ tsupport (χ j) ⊆ U) ∧ (∀ (j : ℕ), Set.EqOn (χ j) 1 (tsupport (ζ j))) ∧ ∀ x ∈ U, ∃ (m : ℕ), ∀ᶠ (y : E) in nhds x, (∀ (j : ℕ), m ≤ j → χ j y = 0) ∧ ∀ (N : ℕ), m ≤ N → ∑ j ∈ Finset.range N, ζ j y = 1

A smooth decomposition of unity of an open set, with cutoffs. Every open set U of a finite-dimensional real normed space carries smooth compactly supported functions ζ j and χ j, j : ℕ, with topological supports in U, such that χ j = 1 on the topological support of ζ j, and every point of U has a neighbourhood on which χ j vanishes and ∑ j ∈ Finset.range N, ζ j = 1 for all large j and N.

So (ζ j) is a decomposition of unity of U by test functions on U, and the cutoffs χ j form a family which is locally finite in U. Neither family is locally finite at the frontier of U. The functions ζ j are differences of consecutive cutoffs along a compact exhaustion of U, and need not be nonnegative.

theorem TauCeti.contDiffAt_tsum_of_eventually_eq_zero {E : Type u_1} [NormedAddCommGroup E] {𝕜 : Type u_2} {ι : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {g : ι → E → F} {x : E} (s : Finset ι) (hg : ∀ j ∈ s, ContDiffAt 𝕜 n (g j) x) (hs : ∀ᶠ (y : E) in nhds x, ∀ j ∉ s, g j y = 0) : ContDiffAt 𝕜 n (fun (y : E) => ∑' (j : ι), g j y) x

A sum of functions which are smooth at x is smooth at x if, on a neighbourhood of x, all but finitely many of them vanish. This makes the locally finite sums built from IsOpen.exists_contDiff_decomposition_cutoff smooth on the open set.

theorem TauCeti.exists_forall_contDiff_cutoff_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x₀ : E) {r R : ℝ}, 0 < r → r < R → ∃ (ψ : E → ℝ), ContDiff ℝ (↑⊤) ψ ∧ Set.range ψ ⊆ Set.Icc 0 1 ∧ Set.EqOn ψ 1 (Metric.closedBall x₀ r) ∧ tsupport ψ ⊆ Metric.closedBall x₀ R ∧ ∀ (x : E), ‖gradient ψ x‖ ≤ c / (R - r)

Radial cutoffs with a quantitative gradient bound. There is a universal constant c such that for every centre x₀ and radii 0 < r < R, some smooth ψ with values in [0, 1] equals one on closedBall x₀ r, has topological support in closedBall x₀ R, and satisfies

‖∇ψ x‖ ≤ c / (R - r) for every x.

The inverse dependence on the gap R - r is what iteration arguments over families of balls with geometrically shrinking gaps need. The cutoff is Real.smoothTransition ((R - ‖x - x₀‖) / (R - r)), and c is a Lipschitz constant of Real.smoothTransition.