SmoothBumpCovering.c_mem'
theorem SmoothBumpCovering.c_mem' :
∀ {ι : Type uι} {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] {s : optParam (Set M) Set.univ}
(self : SmoothBumpCovering ι I M s) (i : ι), self.c i ∈ s
The theorem `SmoothBumpCovering.c_mem'` states that for any given `ι`, `E`, `H`, `I`, `M`, and `s` where `ι` is any type, `E` is a normed add commutative group where `E` is also a normed space over the real numbers and has a finite dimension. `H` is a topological space, `I` is a model with corners in the real numbers, `E`, and `H`, and `M` is a topological space that is charted in `H`, with `s` as an optional parameter for a set of `M` elements (defaulting to the universal set). For a given smooth bump covering instance of `ι`, `I`, `M`, and `s`, any `i` from `ι`, the center of the bump function represented by `i` (given by `self.c i`) is an element of `s`.
More concisely: For any smooth bump covering instance of type `ι`, topological spaces `H` and `M`, and optional set `s` in `M`, the center of each bump function in `ι` belongs to `s`.
|
exists_smooth_zero_one_nhds_of_isClosed
theorem exists_smooth_zero_one_nhds_of_isClosed :
∀ {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] [inst_6 : SmoothManifoldWithCorners I M]
[inst_7 : T2Space M] [inst_8 : NormalSpace M] [inst_9 : SigmaCompactSpace M] {s t : Set M},
IsClosed s →
IsClosed t →
Disjoint s t →
∃ f,
(∀ᶠ (x : M) in nhdsSet s, f x = 0) ∧ (∀ᶠ (x : M) in nhdsSet t, f x = 1) ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
The theorem `exists_smooth_zero_one_nhds_of_isClosed` states that given a Hausdorff normal σ-compact finite dimensional manifold `M` and two disjoint closed sets `s` and `t` within `M`, there exists a smooth function `f` mapping from `M` to the closed interval [0, 1] such that `f` vanishes (i.e., `f` equals 0) in a neighborhood of `s` and equals `1` in a neighborhood of `t`. This means `f` smoothly transitions from `0` to `1` between the neighborhoods of these two disjoint sets.
More concisely: Given a Hausdorff normal σ-compact finite dimensional manifold `M` and two disjoint closed sets `s` and `t` within `M`, there exists a smooth function `f: M -> [0, 1]` with `f(s) = {0}` and `f(t) = {1}`.
|
Emetric.exists_smooth_forall_closedBall_subset
theorem Emetric.exists_smooth_forall_closedBall_subset :
∀ {ι : Type uι} {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 u_1} [inst_4 : EMetricSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
[inst_7 : SigmaCompactSpace M] {K U : ι → Set M},
(∀ (i : ι), IsClosed (K i)) →
(∀ (i : ι), IsOpen (U i)) →
(∀ (i : ι), K i ⊆ U i) →
LocallyFinite K →
∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i
This theorem states that given a smooth σ-compact manifold `M` with extended distance, if there exists a locally finite family `K` of closed sets, and a family `U` of open sets such that each set in `K` is contained in a corresponding set in `U`, then there exists a positive smooth function `δ` mapping from `M` to nonnegative real numbers. Furthermore, for any `i` and any `x` in `K i`, the closed ball in the extended metric space centered at `x` with radius `δ x` is contained in `U i`. This theorem is significant in mathematical analysis and manifold theory, where it is often necessary to find such a smooth function `δ` within an open set of a manifold that encapsulates certain properties.
More concisely: Given a smooth σ-compact manifold with an extended metric, if there exists a locally finite collection of closed sets and an open cover such that each closed set is contained in its open neighbor, then there exists a smooth positive function δ mapping each point to a radius such that the closed ball centered at that point with that radius is contained in the corresponding open set.
|
IsOpen.exists_msmooth_support_eq
theorem IsOpen.exists_msmooth_support_eq :
∀ {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] [inst_6 : SmoothManifoldWithCorners I M]
[inst_7 : SigmaCompactSpace M] [inst_8 : T2Space M] {s : Set M},
IsOpen s → ∃ f, Function.support f = s ∧ Smooth I (modelWithCornersSelf ℝ ℝ) f ∧ ∀ (x : M), 0 ≤ f x
This theorem states that for any open set within a finite-dimensional real manifold, there exists a nonnegative smooth function whose support is equal to that set. Here, 'support' of a function refers to the set of points where the function is not zero. The manifold is assumed to be sigma-compact and T2, which means it is a countable union of compact subsets and any two distinct points have disjoint open neighborhoods respectively. The smoothness of the function is with respect to the given manifolds modelled on the Euclidean space with the standard smooth structure. The function is nonnegative, meaning its value is always greater than or equal to zero.
More concisely: For any open set on a sigma-compact, T2 real manifold, there exists a nonnegative smooth function with that set as its support.
|
exists_smooth_forall_mem_convex_of_local
theorem exists_smooth_forall_mem_convex_of_local :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {H : Type uH}
[inst_5 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_6 : TopologicalSpace M]
[inst_7 : ChartedSpace H M] [inst_8 : SmoothManifoldWithCorners I M] [inst_9 : SigmaCompactSpace M]
[inst_10 : T2Space M] {t : M → Set F},
(∀ (x : M), Convex ℝ (t x)) →
(∀ (x : M), ∃ U ∈ nhds x, ∃ g, SmoothOn I (modelWithCornersSelf ℝ F) g U ∧ ∀ y ∈ U, g y ∈ t y) →
∃ g, ∀ (x : M), g x ∈ t x
This theorem, `exists_smooth_forall_mem_convex_of_local`, states that under certain conditions, a smooth function exists that maps every point in a given space to a corresponding convex set. Specifically, let `M` represent a sigma-compact, Hausdorff, finite dimensional topological manifold. Also, let `t` be a function that maps every point of `M` to a convex set in `F`. If for every point `x` in `M`, there is a neighborhood `U` and a function `g` that is smooth on `U` and maps every point `y` in `U` to its corresponding set `t y` in `F`, then a smooth function `g` exists that maps every point `x` in `M` to its corresponding set `t x` in `F`.
More concisely: If a map from a sigma-compact, Hausdorff, finite dimensional manifold to convex sets has local smooth representatives at each point, then there exists a global smooth representative of the map.
|
SmoothBumpCovering.IsSubordinate.toBumpCovering
theorem SmoothBumpCovering.IsSubordinate.toBumpCovering :
∀ {ι : Type uι} {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] [inst_6 : SmoothManifoldWithCorners I M]
{s : Set M} [inst_7 : T2Space M] {f : SmoothBumpCovering ι I M s} {U : M → Set M},
f.IsSubordinate U → f.toBumpCovering.IsSubordinate fun i => U (f.c i)
This theorem, **Alias** of the reverse direction of `SmoothBumpCovering.isSubordinate_toBumpCovering`, states that for any finite dimensional normed space `E` over the reals, a topological space `H`, a model with corners `I` from `E` to `H`, a topological space `M` with a charted space structure over `H` and `M` being a smooth manifold with corners `I`, given a set `s` of `M` and `M` being a `T2Space`, if a smooth bump covering `f` of `M` with base `s` is subordinate to a function `U` that maps from `M` to a set of `M`, then the bump covering (obtained by applying `toBumpCovering` to `f`) is subordinate to the function that maps each index to the set `U` evaluated at the center of the corresponding bump of `f`.
More concisely: Given a smooth manifold with corners `M` over a finite dimensional normed space `E` with a charted space structure over a topological space `H`, if a smooth bump covering `f: M -> M` with base `s` is subordinate to a function `U: M -> Sets M` and `M` is a `T2Space`, then the bump covering obtained from `f` is subordinate to the function `x => U(x)(0)` where `0` is the center of each bump.
|
SmoothBumpCovering.eventuallyEq_one'
theorem SmoothBumpCovering.eventuallyEq_one' :
∀ {ι : Type uι} {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] {s : optParam (Set M) Set.univ}
(self : SmoothBumpCovering ι I M s), ∀ x ∈ s, ∃ i, (nhds x).EventuallyEq (↑(self.toFun i)) 1
This theorem, titled `SmoothBumpCovering.eventuallyEq_one'`, states that for every point in a given set `s` in a manifold `M` (a topological space with a charted space structure), there exists a bump function (a smooth function that is equal to `1` at the center and decays to `0` at infinity) from the smooth bump covering of `M` that equals `1` in a neighborhood of that point. The manifold `M` is modeled on a finite-dimensional normed vector space `E` over the real numbers, with a model given by `I`. The set `s` is optional and defaults to the universal set of `M`.
More concisely: For every point in a manifold M, there exists a smooth bump function in its smooth bump covering that equals 1 in a neighborhood of that point.
|
SmoothBumpCovering.apply_ind
theorem SmoothBumpCovering.apply_ind :
∀ {ι : Type uι} {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] {s : Set M}
(fs : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s), ↑(fs.toFun (fs.ind x hx)) x = 1
The theorem `SmoothBumpCovering.apply_ind` states that, given a smooth bump covering `fs` (a partition of unity by smooth functions with compact support) of a set `s` in a differentiable manifold `M`, for any point `x` in `s`, the value of the function associated with the index `(SmoothBumpCovering.ind fs x hx)` at `x` is equal to 1. The context assumes `M` to be a charted space modeled on a finite-dimensional normed space `E` over real numbers, and the set `s` is a subset of `M`.
More concisely: For any smooth bump covering `fs` of a subset `s` in a differentiable manifold `M`, the function associated with the index of `x` in `s` according to `fs` equals 1 at `x`.
|
SmoothPartitionOfUnity.exists_isSubordinate
theorem SmoothPartitionOfUnity.exists_isSubordinate :
∀ {ι : Type uι} {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] [inst_6 : SmoothManifoldWithCorners I M]
[inst_7 : T2Space M] [inst_8 : SigmaCompactSpace M] {s : Set M},
IsClosed s → ∀ (U : ι → Set M), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U
This theorem states that, given a paracompact normal topological space `X`, a closed set `s`, and an open covering `U` of the set `s`, there exists a smooth partition of unity subordinate to `U`. This smooth partition of unity is a mathematical structure that allows us to "break down" a complex mathematical object into simpler parts, each of which can be studied separately. This is particularly useful in the study of differential and integral calculus on manifolds. The topology of the space `X`, the properties of the set `s` and the properties of the open covering `U` are all important in the statement and proof of this theorem.
More concisely: Given a paracompact normal topological space X, a closed set s, and an open covering U of s, there exists a smooth partition of unity subordinate to U.
|
exists_msmooth_support_eq_eq_one_iff
theorem exists_msmooth_support_eq_eq_one_iff :
∀ {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] [inst_6 : SmoothManifoldWithCorners I M]
[inst_7 : SigmaCompactSpace M] [inst_8 : T2Space M] {s t : Set M},
IsOpen s →
IsClosed t →
t ⊆ s →
∃ f,
Smooth I (modelWithCornersSelf ℝ ℝ) f ∧
Set.range f ⊆ Set.Icc 0 1 ∧ Function.support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
The theorem `exists_msmooth_support_eq_eq_one_iff` asserts that, given an open set `s` containing a closed set `t` situated in a finite-dimensional real manifold, there exists a smoothly varying function whose support is exactly `s`, which takes on values in the closed interval from 0 to 1, and is equal to 1 precisely on the set `t`. In other words, this function is characterized by smoothness, with its range confined to the interval [0,1], its support coinciding with the open set, and taking the value 1 specifically over the closed subset.
More concisely: Given an open set `s` containing a closed set `t` in a finite-dimensional real manifold, there exists a smoothly varying function with support equal to `s` and values in [0,1] that equals 1 on `t`.
|
SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul
theorem SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul :
∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners ℝ E H} {M : Type uM} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] {s : Set M}
{f : SmoothPartitionOfUnity ι I M s} {n : ℕ∞} {U : ι → Set M} {g : ι → M → F},
f.IsSubordinate U →
(∀ (i : ι), IsOpen (U i)) →
(∀ (i : ι), ContMDiffOn I (modelWithCornersSelf ℝ F) n (g i) (U i)) →
ContMDiff I (modelWithCornersSelf ℝ F) n fun x => finsum fun i => (f i) x • g i x
The theorem `SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul` states that, given a smooth partition of unity `f` on a set `s` in manifold `M`, which is subordinate to a family of open sets `U`, and a family of functions `g` such that each `g i` is continuously differentiable up to order `n` on `U i`, then the finite sum function which maps `x` to the sum over `i` of `f i x` times `g i x` is also continuously differentiable up to order `n` on the entire manifold. This basically means that a smooth combination of smooth functions remains smooth.
More concisely: Given a smooth partition of unity `f` on a manifold `M` subordinate to a cover `U`, and a family `g_i` of functions on `M` continuously differentiable up to order `n` on each `U_i`, the finite sum function `x ↦ ∑ i f_i x * g_i x` is continuously differentiable up to order `n` on the entire manifold `M`.
|
SmoothPartitionOfUnity.smooth_finsum_smul
theorem SmoothPartitionOfUnity.smooth_finsum_smul :
∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners ℝ E H} {M : Type uM} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] {s : Set M}
(f : SmoothPartitionOfUnity ι I M s) {g : ι → M → F},
(∀ (i : ι), ∀ x ∈ tsupport ⇑(f i), SmoothAt I (modelWithCornersSelf ℝ F) (g i) x) →
Smooth I (modelWithCornersSelf ℝ F) fun x => finsum fun i => (f i) x • g i x
The theorem `SmoothPartitionOfUnity.smooth_finsum_smul` states that if `f` is a smooth partition of unity on a set `s` in a manifold `M`, and if for each index `i`, the function `g i` is smooth at every point in the topological support of `f i` (i.e., the closure of the set of points where `f i` is nonzero), then the function that sends each point `x` in `M` to the finite sum over `i` of the product of `f i x` and `g i x` is smooth throughout the entire manifold. This sum is zero when the index set of `i` is infinite. This theorem relies on the specific structure of a smooth partition of unity and the properties of finiteness, smoothness, and topology.
More concisely: Given a smooth partition of unity `f` on a manifold `M` with smooth functions `g_i` supported in the closure of the nonzero sets of `f_i`, the function `∑ (i) (f_i ⊤ × g_i ⊤)` is a smooth function on `M`, where the sum is taken over the index set `i` and is zero when infinite.
|
SmoothPartitionOfUnity.sum_eq_one'
theorem SmoothPartitionOfUnity.sum_eq_one' :
∀ {ι : Type uι} {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] {s : optParam (Set M) Set.univ} (self : SmoothPartitionOfUnity ι I M s),
∀ x ∈ s, (finsum fun i => (self.toFun i) x) = 1
This theorem states that for any smooth partition of unity (which is a concept from differential geometry), the sum of all the functions in the partition equals to 1 for any point in the set `s`. More formally, consider a smooth partition of unity `self` defined on a manifold `M`, with `s` being a subset of `M` (defaulting to the entire set `M`). For every point `x` in `s`, the sum over all functions `i` in the partition, evaluated at `x`, equals to 1. This property is a defining characteristic of partitions of unity in differential geometry.
More concisely: For any smooth partition of unity on a manifold, the sum of its functions equals 1 at each point in the manifold.
|
SmoothPartitionOfUnity.nonneg'
theorem SmoothPartitionOfUnity.nonneg' :
∀ {ι : Type uι} {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] {s : optParam (Set M) Set.univ} (self : SmoothPartitionOfUnity ι I M s) (i : ι)
(x : M), 0 ≤ (self.toFun i) x
This theorem asserts that all functions in a smooth partition of unity are nonnegative. Specifically, for any index set `ι`, normed additive commutative group `E`, normed space over the real numbers `ℝ` and `E`, topological space `H`, model with corners `I` over `ℝ`, `E`, and `H`, topological space `M`, charted space `M` over `H`, optional parameter `s` which is a set of `M` (defaulting to the universal set of `M` if not provided), a smooth partition of unity `self` on these structures, and for any element `i` in the index set `ι` and any point `x` in `M`, the function associated with `i` in the partition of unity evaluated at `x` is greater than or equal to zero.
More concisely: For any smooth partition of unity `self` on a charted space `M` over a topological space `H`, all functions associated with indices in the partition are nonnegative on `M`.
|
SmoothPartitionOfUnity.locallyFinite'
theorem SmoothPartitionOfUnity.locallyFinite' :
∀ {ι : Type uι} {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] {s : optParam (Set M) Set.univ} (self : SmoothPartitionOfUnity ι I M s),
LocallyFinite fun i => Function.support ⇑(self.toFun i)
This theorem states that for every point in a smooth partition of unity (which is a certain mathematical structure used in the study of manifolds), there exist only finitely many functions which are nonzero at that point. A smooth partition of unity involves a family of functions and this theorem asserts that for each point, we can find a neighborhood (in the topological sense) such that only finitely many of these functions are nonzero in that neighborhood. This is a property of local finiteness of the support of the functions in the partition of unity.
More concisely: In a smooth partition of unity, each point has a neighborhood where only finitely many functions are nonzero.
|
SmoothPartitionOfUnity.sum_le_one'
theorem SmoothPartitionOfUnity.sum_le_one' :
∀ {ι : Type uι} {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] {s : optParam (Set M) Set.univ} (self : SmoothPartitionOfUnity ι I M s) (x : M),
(finsum fun i => (self.toFun i) x) ≤ 1
This theorem states that for any smooth partition of unity, the sum of the values of the functions in the partition at any point is less than or equal to one. More explicitly, given a type `ι`, a normed add commutative group `E`, a normed space over the reals `ℝ` and `E`, a topological space `H`, a model with corners `I` relating `ℝ`, `E` and `H`, a type `M`, a topological space `M`, a charted space `H` over `M`, and an optional parameter `s` set in `M` (defaulted to the universal set of `M`), each instance of a smooth partition of unity over these types and spaces has the property that for every element `x` in `M`, the sum of the function values `(self.toFun i) x` for all `i` in the partition is less than or equal to 1. Here, `finsum` is a function that sums over the function values for each element in the support of the function, if the support is finite, and gives zero otherwise.
More concisely: For any smooth partition of unity over a topological space with given types, spaces, and charts, the sum of the function values at each point is less than or equal to 1.
|
SmoothPartitionOfUnity.IsSubordinate.toPartitionOfUnity
theorem SmoothPartitionOfUnity.IsSubordinate.toPartitionOfUnity :
∀ {ι : Type uι} {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] {s : Set M} {f : SmoothPartitionOfUnity ι I M s} {U : ι → Set M},
f.IsSubordinate U → f.toPartitionOfUnity.IsSubordinate U
This theorem, termed **Alias** of the reverse direction of `SmoothPartitionOfUnity.isSubordinate_toPartitionOfUnity`, states that for any set of indices `ι`, types `E`, `H`, and `M`, with `E` being a normed add commutative group, `E` being a normed space over the real numbers, `H` being a topological space, `I` being a model with corners over real numbers, `E` and `H`, `M` being a topological space, `M` being a charted space over `H`, a set `s` of type `M`, a smooth partition of unity `f` on `s`, and a family of sets `U` indexed by `ι`, if the smooth partition of unity `f` is subordinate to `U`, then the partition of unity associated with `f` is also subordinate to `U`. In simpler terms, it suggests that the subordination relationship is preserved when transitioning from a smooth partition of unity to its associated partition of unity.
More concisely: Given a smooth partition of unity `f` on a set `s` in a charted space `M` over a topological space `H`, and a family of sets `U` indexed by `ι`, if `f` is subordinate to `U`, then the partition of unity associated with `f` is subordinate to `U`.
|
Metric.exists_smooth_forall_closedBall_subset
theorem Metric.exists_smooth_forall_closedBall_subset :
∀ {ι : Type uι} {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 u_1} [inst_4 : MetricSpace M] [inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M]
[inst_7 : SigmaCompactSpace M] {K U : ι → Set M},
(∀ (i : ι), IsClosed (K i)) →
(∀ (i : ι), IsOpen (U i)) →
(∀ (i : ι), K i ⊆ U i) →
LocallyFinite K → ∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedBall x (δ x) ⊆ U i
This theorem states that given a smooth, sigma-compact manifold `M` with a metric, and two families of sets `K` and `U`, indexed by `ι`, where `K` is a locally finite family of closed sets and `U` is a family of open sets with each set in `K` contained in the corresponding set in `U`, then there exists a positive smooth function `δ` from `M` to non-negative real numbers such that for any `i` and any point `x` in `K i`, the closed ball centered at `x` with radius `δ x` is a subset of `U i`. Here, the closed ball centered at `x` with radius `ε` is defined as the set of all points `y` such that the distance between `y` and `x` is less than or equal to `ε`.
More concisely: Given a smooth, sigma-compact manifold with a metric, if `K` is a locally finite family of closed sets and `U` is an open cover such that each `K_i` is contained in `U_i`, then there exists a smooth function `δ: M -> ℝ+` such that for all `x ∈ K_i`, the closed ball `B(x, δ x)` is a subset of `U_i`.
|
exists_smooth_zero_one_of_isClosed
theorem exists_smooth_zero_one_of_isClosed :
∀ {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] [inst_6 : SmoothManifoldWithCorners I M]
[inst_7 : T2Space M] [inst_8 : SigmaCompactSpace M] {s t : Set M},
IsClosed s →
IsClosed t → Disjoint s t → ∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
This theorem states that given two disjoint closed sets `s` and `t` in a Hausdorff (T2 space), sigma-compact, finite-dimensional manifold, there exists an infinitely differentiable (smooth) function that is equal to `0` on set `s` and equal to `1` on set `t`. The function's range is also confined within the closed interval from `0` to `1`. This theorem is associated with another theorem `exists_msmooth_zero_iff_one_iff_of_isClosed` that further asserts that `f` is equal to `0` precisely on `s` and to `1` precisely on `t`.
More concisely: Given two disjoint, closed subsets of a Hausdorff, sigma-compact, finite-dimensional manifold, there exists an infinitely differentiable function equal to 0 on the first set and 1 on the second set, with range in [0,1].
|
exists_smooth_one_nhds_of_subset_interior
theorem exists_smooth_one_nhds_of_subset_interior :
∀ {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] [inst_6 : SmoothManifoldWithCorners I M]
[inst_7 : T2Space M] [inst_8 : NormalSpace M] [inst_9 : SigmaCompactSpace M] {s t : Set M},
IsClosed s →
s ⊆ interior t → ∃ f, (∀ᶠ (x : M) in nhdsSet s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
This theorem states that given any two sets `s` and `t` within a Hausdorff normal σ-compact finite-dimensional manifold `M` - where `s` is open and contained within the interior of `t` - it is possible to define a smooth function `f` mapping from `M` to the interval `[0,1]`. This function is equal to 1 in a neighborhood of `s` and has support contained within `t`. More specifically, for all points `x` in `M`, the function `f(x)` will result in a value within the closed interval from 0 to 1. If `x` is not an element of `t`, `f(x)` will be equal to 0.
More concisely: Given any open set `s` in the Hausdorff normal σ-compact finite-dimensional manifold `M`, there exists a smooth function `f` from `M` to the interval `[0,1]` such that `f(x) = 1` for `x` in a neighborhood of `s` and `f(x) = 0` for `x` not in `t`, where `t` is the larger set containing `s` in its interior.
|
SmoothBumpCovering.locallyFinite'
theorem SmoothBumpCovering.locallyFinite' :
∀ {ι : Type uι} {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] {s : optParam (Set M) Set.univ}
(self : SmoothBumpCovering ι I M s), LocallyFinite fun i => Function.support ↑(self.toFun i)
This theorem, named `SmoothBumpCovering.locallyFinite'`, asserts that for any smooth bump covering (a family of smooth functions) in a finite-dimensional, normed additively commutative group over the real numbers, each point in the space only interacts with a finite number of non-zero functions in the family. More concretely, at every point of the space, there exists a neighborhood such that only finitely many functions in the smooth bump covering are non-zero within this neighborhood. This is a property known as local finiteness. The space is assumed to have a certain topological and differential structure (provided by the data `H`, `I`, `M`, and `s`) and the smooth bump covering is parameterized by a type `ι`.
More concisely: At every point in a finite-dimensional, normed additively commutative real group equipped with a specific topological and differential structure, there exists a neighborhood where only finitely many non-zero functions in a smooth bump covering are non-zero.
|
exists_msmooth_zero_iff_one_iff_of_isClosed
theorem exists_msmooth_zero_iff_one_iff_of_isClosed :
∀ {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] [inst_6 : SmoothManifoldWithCorners I M]
[inst_7 : SigmaCompactSpace M] [inst_8 : T2Space M] {s t : Set M},
IsClosed s →
IsClosed t →
Disjoint s t →
∃ f,
Smooth I (modelWithCornersSelf ℝ ℝ) f ∧
Set.range f ⊆ Set.Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
This theorem states that, for any two disjoint closed sets `s` and `t` in a Hausdorff σ-compact finite dimensional smooth manifold `M` with a model with corners `I` and a charted space over some topological space `H`, there exists a smooth function `f` from the manifold `M` to the reals (using the canonical model with corners for the reals) such that the range of function `f` is within the closed interval between 0 and 1 inclusive, and `f` maps any point in set `s` to `0` and any point in set `t` to `1`. The Hausdorff property guarantees that every two distinct points in the manifold have disjoint neighborhoods, and the σ-compact property implies the space is a countable union of compact subsets. The manifold being finite dimensional indicates it has a finite basis in its vector space.
More concisely: Given any two disjoint closed sets in a Hausdorff σ-compact finite dimensional smooth manifold, there exists a smooth function mapping the manifold to the reals with range [0,1] such that each set is mapped to its respective endpoint.
|
SmoothPartitionOfUnity.IsSubordinate.smooth_finsum_smul
theorem SmoothPartitionOfUnity.IsSubordinate.smooth_finsum_smul :
∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners ℝ E H} {M : Type uM} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] {s : Set M}
{f : SmoothPartitionOfUnity ι I M s} {U : ι → Set M} {g : ι → M → F},
f.IsSubordinate U →
(∀ (i : ι), IsOpen (U i)) →
(∀ (i : ι), SmoothOn I (modelWithCornersSelf ℝ F) (g i) (U i)) →
Smooth I (modelWithCornersSelf ℝ F) fun x => finsum fun i => (f i) x • g i x
This theorem states that if we have a smooth partition of unity `f` on a set `s` in a manifold `M`, which is subordinate to a family of open sets `U` indexed by `ι`, and we also have a family of functions `g` indexed by `ι` such that each function `g i` is smooth on the corresponding open set `U i`, then the function defined by the finite sum `fun x ↦ ∑ᶠ i, f i x • g i x` is smooth on the entire manifold. The smoothness of `g i` is defined with respect to the standard model with corners in the target space `F`, and the smoothness of the resulting function is also defined with respect to the same model with corners.
More concisely: Given a smooth partition of unity `f` and a family of smooth functions `g_i` on a manifold `M` subordinate to open sets `U_i`, the function `∑ᵢ in ι, f_i x * g_i x` is smooth on `M`.
|
SmoothPartitionOfUnity.contMDiff_finsum_smul
theorem SmoothPartitionOfUnity.contMDiff_finsum_smul :
∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF}
[inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {H : Type uH} [inst_4 : TopologicalSpace H]
{I : ModelWithCorners ℝ E H} {M : Type uM} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M] {s : Set M}
(f : SmoothPartitionOfUnity ι I M s) {n : ℕ∞} {g : ι → M → F},
(∀ (i : ι), ∀ x ∈ tsupport ⇑(f i), ContMDiffAt I (modelWithCornersSelf ℝ F) n (g i) x) →
ContMDiff I (modelWithCornersSelf ℝ F) n fun x => finsum fun i => (f i) x • g i x
This theorem states that if `f` is a smooth partition of unity on a set `s` of type `Set M` and `g` is a family of functions such that each `g i` is `C^n` smooth at every point of the topological support of `f i`, then the function that maps `x` to the sum over `i` of `f i x * g i x` (denoted `fun x => finsum fun i => (f i) x • g i x` in the code) is smooth on the entire manifold. Here, "smooth" means continuously differentiable to any order, and "manifold" refers to a topological space that locally resembles Euclidean space near each point. The theorem is formulated for a general manifold `M` equipped with a model with corners `I` and a normed vector space `F` over the real numbers.
More concisely: If `f` is a smooth partition of unity on a manifold `M` and each `g i` is `C^n` smooth on the topological support of `f i`, then the function summing `f i x * g i x` is smooth on `M`.
|
exists_contMDiffOn_forall_mem_convex_of_local
theorem exists_contMDiffOn_forall_mem_convex_of_local :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {H : Type uH}
[inst_5 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_6 : TopologicalSpace M]
[inst_7 : ChartedSpace H M] [inst_8 : SmoothManifoldWithCorners I M] [inst_9 : SigmaCompactSpace M]
[inst_10 : T2Space M] {t : M → Set F} {n : ℕ∞},
(∀ (x : M), Convex ℝ (t x)) →
(∀ (x : M), ∃ U ∈ nhds x, ∃ g, ContMDiffOn I (modelWithCornersSelf ℝ F) n g U ∧ ∀ y ∈ U, g y ∈ t y) →
∃ g, ∀ (x : M), g x ∈ t x
This theorem, `exists_contMDiffOn_forall_mem_convex_of_local`, states that under certain conditions, there exists a continuously differentiable function whose values are always within specified convex sets.
In detail, let us consider a σ-compact Hausdorff finite dimensional topological manifold `M`. For each point in `M`, associate a convex set in a normed space `F`. Assume that for each point `x` in `M`, there exists a neighborhood `U` and a function `g` that is continuously differentiable up to order `n` on `U` such that the value of `g` at any point `y` in `U` lies in the corresponding convex set associated with `y`. The theorem then states that there exists a function `g` that is continuously differentiable up to order `n` on `M` such that for each point `x` in `M`, the value `g(x)` lies in the corresponding convex set associated with `x`.
More concisely: Given a σ-compact Hausdorff finite dimensional manifold M with each point x having a neighborhood U and a continuously differentiable up to order n function g on U such that g(y) lies in the associated convex set for all y in U, there exists a continuously differentiable up to order n function g on M such that g(x) lies in the associated convex set for all x in M.
|
SmoothBumpCovering.exists_isSubordinate
theorem SmoothBumpCovering.exists_isSubordinate :
∀ {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] {s : Set M} {U : M → Set M} [inst_6 : T2Space M]
[inst_7 : SigmaCompactSpace M], IsClosed s → (∀ x ∈ s, U x ∈ nhds x) → ∃ ι f, f.IsSubordinate U
This theorem, `SmoothBumpCovering.exists_isSubordinate`, states that given a smooth manifold `M` with corners modelled on a finite dimensional real vector space, which is also a Hausdorff `σ`-compact topological space, and a closed set `s` in `M`, then if `U` is a collection of sets such that for each `x` in `s`, `U x` is a neighborhood of `x`, there exists a smooth bump covering of `s` that is subordinate to `U`. A bump covering is a collection of smooth functions whose supports cover the set `s` and being "subordinate" to `U` means that the support of each function in the collection is contained in some set of `U`.
More concisely: Given a smooth manifold with corners `M` (Hausdorff, σ-compact), a closed set `s ∈ M`, and a collection `U` of neighborhoods of `s`, there exists a smooth bump covering of `s` whose supports are contained in some set of `U`.
|
exists_smooth_forall_mem_convex_of_local_const
theorem exists_smooth_forall_mem_convex_of_local_const :
∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {H : Type uH}
[inst_5 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_6 : TopologicalSpace M]
[inst_7 : ChartedSpace H M] [inst_8 : SmoothManifoldWithCorners I M] [inst_9 : SigmaCompactSpace M]
[inst_10 : T2Space M] {t : M → Set F},
(∀ (x : M), Convex ℝ (t x)) → (∀ (x : M), ∃ c, ∀ᶠ (y : M) in nhds x, c ∈ t y) → ∃ g, ∀ (x : M), g x ∈ t x
This theorem states that given a σ-compact Hausdorff finite-dimensional topological manifold `M` and a family `t : M → Set F` of convex sets, if for each point `x : M`, there exists a vector `c : F` such that `c` belongs to the set `t y` for all `y` in a neighborhood of `x`, then there exists a smooth function `g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x` belongs to `t x` for all `x` in `M`. The theorem ensures that under certain conditions, we can find a smooth function that maps each point in the manifold to a member of its corresponding set in the given family of convex sets.
More concisely: Given a σ-compact Hausdorff finite-dimensional topological manifold `M` and a family `t : M → Set F` of convex sets such that for each `x : M`, there exists a vector `c : F` with `c ∈ t(y)` for all `y` in a neighborhood of `x`, there exists a smooth function `g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` with `g(x) ∈ t(x)` for all `x : M`.
|