SmoothBumpFunction.exists_r_pos_lt_subset_ball
theorem SmoothBumpFunction.exists_r_pos_lt_subset_ball :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM}
[inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) {s : Set M},
IsClosed s →
s ⊆ Function.support ↑f →
∃ r ∈ Set.Ioo 0 f.rOut,
s ⊆ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' Metric.ball (↑(extChartAt I c) c) r
The theorem states that for a smooth bump function `f`, and a closed subset `s` of the support of `f` (that is, of the open ball of radius `f.rOut`), there exists a positive radius `r` less than `f.rOut` such that `s` is a subset of the open ball of radius `r`. In more formal terms, given a condition that `s` is a subset of the support of `f`, there exists a radius `r` in the open interval from 0 to `f.rOut`, such that `s` is a subset of the intersection of the source of the preferred chart at `c` and the preimage under the extension of this chart of the open ball (in the Euclidean metric space) centered at the image of `c` under this extension and of radius `r`. Here, `E` is a finite-dimensional real normed add-commutative group, `H` is a topological space, `I` is a model with corners (a smooth manifold structure) from the reals to `E` and `H`, and `M` is a topological space equipped with a charted space structure with model `H`.
More concisely: Given a smooth bump function `f` on a finite-dimensional Euclidean space `E` with support `s`, there exists a radius `r < f.rOut` such that `s` is contained in the open ball of radius `r` in `E`.
|
SmoothBumpFunction.support_eq_inter_preimage
theorem SmoothBumpFunction.support_eq_inter_preimage :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM}
[inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c),
Function.support ↑f = (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' Metric.ball (↑(extChartAt I c) c) f.rOut
This theorem states that for any normed additively commutative group `E` that is a finite-dimensional real vector space, and any topological space `H`, given a model with corners `I` from the reals to `E` and `H`, and any topological space `M` that is a charted space over `H`, and any point `c` in `M`, for any smooth bump function `f` with model `I` and center `c`, the support of `f` (the set of points where `f` is not zero) is equal to the intersection of the source of the chart at `c` and the preimage under the extended chart at `c` of the open ball centered at the image under the extended chart at `c` of `c` with radius given by `f.rOut` (the radius at which `f` tapers off to zero).
More concisely: For any smooth bump function `f` with model `I` and center `c` in a charted space `M` over a topological space `H`, the support of `f` equals the intersection of the source of the chart at `c` and the preimage under the extended chart at `c` of the open ball centered at the image of `c` with radius `f.rOut`.
|
SmoothBumpFunction.support_mem_nhds
theorem SmoothBumpFunction.support_mem_nhds :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM}
[inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c),
Function.support ↑f ∈ nhds c
The theorem `SmoothBumpFunction.support_mem_nhds` states that for any Smooth Bump Function `f` defined on a finite dimensional normed vector space `E` over the real numbers, with a model with corners `I`, a topological space `H`, and a charted space `M` with corresponding topological space, the support of `f`, which is the set of points where `f` is not zero, is a neighborhood of `c`. In other words, the support of `f` is in the neighborhood filter of `c`. This means that around the point `c`, we can find an open set where `f` is non-zero.
More concisely: The support of a Smooth Bump Function on a finite dimensional normed vector space is contained in the neighborhood filter of any point in its domain.
|
SmoothBumpFunction.nhdsWithin_range_basis
theorem SmoothBumpFunction.nhdsWithin_range_basis :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
{I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M},
(nhdsWithin (↑(extChartAt I c) c) (Set.range ↑I)).HasBasis (fun x => True) fun f =>
Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I
This theorem states that for a given smooth bump function `f` defined with respect to a model with corners `I` and a point `c` in a topological space `M` charted by a space `H`, the closed balls of radius `f.rOut` in the normed additive commutative group `E` intersected with the range of `I` form a basis for the neighborhood within the range of `I` at the point `c` under the exterior chart at `I` and `c`. In other words, the sets formed by taking the intersection of the closed ball around the image of `c` under the exterior chart (with radius given by `f.rOut`) and the set of points reachable by `I`, provide a basis for the filter that captures the local behavior at the image of `c` under the exterior chart, restricted to the set of points reachable by `I`.
More concisely: The closed balls in the normed additive commutative group, centered at the image of a point `c` under an exterior chart `I` in a topological space `M`, with radii given by the smooth bump function `f`'s outward radius, form a basis for the neighborhood filter of `c` within the range of `I`.
|
SmoothBumpFunction.tsupport_subset_symm_image_closedBall
theorem SmoothBumpFunction.tsupport_subset_symm_image_closedBall :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM}
[inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c)
[inst_6 : T2Space M],
tsupport ↑f ⊆ ↑(extChartAt I c).symm '' (Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I)
This theorem states that for any normed additive commutative group `E`, which is a normed space over ℝ and is finite dimensional, and for any topological space `H` with a model with corners `I` to `E`, any "charted space" `M` over `H` with a specific point `c` in `M`, and a smooth bump function `f` based on `I` and centered at `c`, in a T2 (Hausdorff) space `M`, the topological support of `f` is a subset of the set obtained by mapping the intersection of the closed ball of radius `f.rOut` centered at the image of `c` under the extension of the chart at `c` and the range of `I` under the inverse of the extension of the chart at `c`.
In other words, the set of all points where the smooth bump function does not vanish is contained within a certain region defined by the model with corners, the chart at the point `c`, and the radius `f.rOut` of the smooth bump function. This region is within the inverse image of the intersection of a closed ball in the model space and the range of the model with corners under the extension of the chart at `c`.
More concisely: For any finite-dimensional normed space `E` over ℝ, charted space `M` over a T2 topological space `H` with a smooth bump function `f` and radius `rOut`, the support of `f` is contained in the inverse image of the intersection of the closed ball of radius `rOut` around `f(c)` in `E` and the range of `I` under the extension of the chart at `c`.
|
SmoothBumpFunction.smooth
theorem SmoothBumpFunction.smooth :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM}
[inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c)
[inst_6 : T2Space M] [inst_7 : SmoothManifoldWithCorners I M], Smooth I (modelWithCornersSelf ℝ ℝ) ↑f
The theorem states that a smooth bump function is infinitely differentiable. More specifically, for a given normed additive commutative group `E` that also forms a finite-dimensional real normed space, a topological space `H`, a model with corners `I` defined on `E` and `H`, a topological space `M` that is also a charted space with manifold `H` and `M`, and a point `c` in `M`, any smooth bump function `f` defined using the model with corners `I` and the point `c`, where `M` is a T2 space (a topological space where any two distinct points have disjoint open neighborhoods) and `M` is a smooth manifold with corners `I`, is smooth with respect to the model with corners defined on the real numbers and `M`. "Smooth" here means the function is differentiable and all of its derivatives are continuous.
More concisely: Given a smooth bump function defined using a model with corners on a T2, smooth manifold with corners over a finite-dimensional real normed space, the function is infinitely differentiable.
|
SmoothBumpFunction.nhds_basis_support
theorem SmoothBumpFunction.nhds_basis_support :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{H : Type uH} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM}
[inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {c : M} [inst_6 : T2Space M] {s : Set M},
s ∈ nhds c → (nhds c).HasBasis (fun f => tsupport ↑f ⊆ s) fun f => Function.support ↑f
In this theorem, given a set `s` which is a neighborhood of a point `c`, we establish a basis for the neighborhood filter at `c`. Specifically, the basis elements are the supports of a certain type of function called "smooth bump functions" (`SmoothBumpFunction I c`). Each of these supports not only is a neighborhood of `c`, but also any neighborhood of `c` includes `support f` for some smooth bump function `f` such that the topological support of `f` is a subset of `s`. This theorem applies to normed add commutative groups `E` over the real numbers (`ℝ`) with a finite dimension, topological spaces `M` and `H`, and a model with corners `I` on `E` and `H`. The space `M` is also required to be a `T2Space`, meaning that any two distinct points in it have disjoint open neighborhoods.
More concisely: Given a set `s` that is a neighborhood of a point `c` in a finite-dimensional topological vector space `E` over the real numbers with a `T2Topology`, there exists a basis for the neighborhood filter at `c` consisting of supports of smooth bump functions on `E` with topological support contained in `s`.
|
SmoothBumpFunction.nhds_basis_tsupport
theorem SmoothBumpFunction.nhds_basis_tsupport :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{H : Type uH} [inst_3 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM}
[inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (c : M) [inst_6 : T2Space M],
(nhds c).HasBasis (fun x => True) fun f => tsupport ↑f
This theorem states that, for any given point `c` in a `T2Space` manifold `M` modeled by some `ModelWithCorners` `I` with `NormedSpace` `E` and `TopologicalSpace` `H`, the closures of supports of smooth bump functions centered at `c` form a basis for the neighborhood filter at `c`. In other words, each of these closures is a neighborhood of `c` and each neighborhood of `c` includes the topological support of some smooth bump function centered at `c`.
More concisely: For any point `c` in a `T2Space` manifold `M`, the closures of supports of smooth bump functions centered at `c` form a basis for the neighborhood filter at `c`. In other words, each closure is a neighborhood of `c` and every neighborhood of `c` contains the support of some smooth bump function centered at `c`.
|
SmoothBumpFunction.smooth_smul
theorem SmoothBumpFunction.smooth_smul :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM}
[inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c)
[inst_6 : T2Space M] [inst_7 : SmoothManifoldWithCorners I M] {G : Type u_1} [inst_8 : NormedAddCommGroup G]
[inst_9 : NormedSpace ℝ G] {g : M → G},
SmoothOn I (modelWithCornersSelf ℝ G) g (chartAt H c).source →
Smooth I (modelWithCornersSelf ℝ G) fun x => ↑f x • g x
The theorem `SmoothBumpFunction.smooth_smul` states that if you have a smooth bump function `f : SmoothBumpFunction I c` and another function `g : M → G` that is smooth on the source of the chart at `c`, then the scalar multiplication function `f • g`, which takes an element from the manifold and returns the product of the function values of `f` and `g` at that point, is smooth on the entire manifold `M`. Here, "smooth" means that the function has derivatives of all orders everywhere. All of these definitions are within the context of a finite-dimensional real vector space `E`, a manifold `M` modelled on a topological space `H` with corners modelled on `E`, and a target normed add-commutative group `G`. The smoothness of `g` is defined relative to the model with corners derived from `G`, and the smoothness of `f • g` is also defined relative to this same model with corners.
More concisely: If `f` is a smooth bump function on a manifold `M` and `g` is a smooth function on `M` relative to a given model with corners, then their pointwise product `f • g` is a smooth function on `M` relative to the same model with corners.
|