ExistsContDiffBumpBase.u_exists
theorem ExistsContDiffBumpBase.u_exists :
∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
∃ u,
ContDiff ℝ ⊤ u ∧
(∀ (x : E), u x ∈ Set.Icc 0 1) ∧ Function.support u = Metric.ball 0 1 ∧ ∀ (x : E), u (-x) = u x
This theorem, `ExistsContDiffBumpBase.u_exists`, states that for any normed additive commutative group `E` that is also a finite-dimensional normed space over the real numbers, there exists a function `u` that satisfies the following conditions:
1. `u` is infinitely continuously differentiable (mentioned as `ContDiff ℝ ⊤ u`),
2. For all `x` in `E`, the value of `u` at `x` lies in the closed interval between 0 and 1, inclusive (expressed as `u x ∈ Set.Icc 0 1`),
3. The support of the function `u` (the set of points where `u` is non-zero) is exactly the open ball of radius 1 around the origin in `E` (indicated as `Function.support u = Metric.ball 0 1`),
4. The function `u` is even, that is, for every `x` in `E`, `u(-x)` equals `u(x)`.
In essence, the theorem guarantees the existence of an infinitely differentiable "bump" function that peaks at the origin of the space, is nonzero in a radius-1 ball around the origin, and is zero elsewhere.
More concisely: Given a finite-dimensional real normed space `E`, there exists an infinitely differentiable, even function `u` with support in the open ball of radius 1 around the origin and values in the closed interval [0, 1].
|
exists_smooth_tsupport_subset
theorem exists_smooth_tsupport_subset :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E} {x : E},
s ∈ nhds x → ∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ Set.range f ⊆ Set.Icc 0 1 ∧ f x = 1
This theorem states that for any given normed add-commutative group `E` over the real numbers, which also forms a finite dimensional normed space, if a set `s` is a neighborhood of a point `x` in `E`, then there exists a smooth function `f` with compact support and the function `f` lies entirely within the set `s`. Furthermore, the function `f` is infinitely continuously differentiable (`ContDiff ℝ ⊤ f`), its range lies in the closed interval from 0 to 1 (`Set.range f ⊆ Set.Icc 0 1`), and at the point `x`, the function `f` takes the value 1 (`f x = 1`).
More concisely: For any normed add-commutative group `E` over the real numbers that is finite dimensional and any neighborhood `s` of a point `x` in `E`, there exists an infinitely continuously differentiable function `f` with compact support in `s` and `f(x) = 1`, with the range of `f` contained in the open interval `(0, 1)`.
|
IsOpen.exists_smooth_support_eq
theorem IsOpen.exists_smooth_support_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{s : Set E}, IsOpen s → ∃ f, Function.support f = s ∧ ContDiff ℝ ⊤ f ∧ Set.range f ⊆ Set.Icc 0 1
This theorem states that for any open set `s` in a finite-dimensional real normed vector space `E`, there exists a smooth function `f` such that the support of `f` is exactly `s`. Furthermore, `f` is continuously differentiable to any order (as denoted by `ContDiff ℝ ⊤ f`) and the range of `f` is within the closed interval from 0 to 1 (as denoted by `Set.range f ⊆ Set.Icc 0 1`).
More concisely: Given any open set `s` in a finite-dimensional real normed vector space `E`, there exists a smooth function `f` with continuous derivatives of all orders such that `s` is the support of `f` and its range is contained in the closed interval `[0, 1]`.
|