OpenSet #
Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.
Smooth cutoffs subordinate to an open set #
For a compact set K contained in an open set U of a finite-dimensional real
normed space, this file constructs a smooth cutoff function that equals one on
K and has closed support inside U.
The construction covers K by finitely many smooth bump functions supported in
U and forms 1 - ∏ (1 - fₓ), a smooth partition-of-unity-style envelope.
theorem
HCPolySupport.exists_contDiff_one_on_compact_tsupport_subset
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{K U : Set E}
(hK : IsCompact K)
(hKU : K ⊆ U)
(hU : IsOpen U)
:
A compact subset of an open set in a finite-dimensional real normed space admits a smooth cutoff which is one on the compact set and has closed support in the open set.