Smooth partition of unity

In this file we define two structures, SmoothBumpCovering and SmoothPartitionOfUnity. Both structures describe coverings of a set by a locally finite family of supports of smooth functions with some additional properties. The former structure is mostly useful as an intermediate step in the construction of a smooth partition of unity but some proofs that traditionally deal with a partition of unity can use a SmoothBumpCovering as well.

Given a real manifold M and its subset s, a SmoothBumpCovering ι I M s is a collection of SmoothBumpFunctions f i indexed by i : ι such that

• the center of each f i belongs to s;

• the family of sets support (f i) is locally finite;

• for each x ∈ s, there exists i : ι such that f i =ᶠ[𝓝 x] 1. In the same settings, a SmoothPartitionOfUnity ι I M s is a collection of smooth nonnegative functions f i : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, i : ι, such that

• the family of sets support (f i) is locally finite;

• for each x ∈ s, the sum ∑ᶠ i, f i x equals one;

• for each x, the sum ∑ᶠ i, f i x is less than or equal to one.

We say that f : SmoothBumpCovering ι I M s is subordinate to a map U : M → Set M if for each index i, we have tsupport (f i) ⊆ U (f i).c. This notion is a bit more general than being subordinate to an open covering of M, because we make no assumption about the way U x depends on x.

We prove that on a smooth finitely dimensional real manifold with σ-compact Hausdorff topology, for any U : M → Set M such that ∀ x ∈ s, U x ∈ 𝓝 x there exists a SmoothBumpCovering ι I M s subordinate to U. Then we use this fact to prove a similar statement about smooth partitions of unity, see SmoothPartitionOfUnity.exists_isSubordinate.

Finally, we use existence of a partition of unity to prove lemma exists_smooth_forall_mem_convex_of_local that allows us to construct a globally defined smooth function from local functions.

TODO

• Build a framework for to transfer local definitions to global using partition of unity and use it to define, e.g., the integral of a differential form over a manifold. Lemma exists_smooth_forall_mem_convex_of_local is a first step in this direction.

Tags

smooth bump function, partition of unity

Covering by supports of smooth bump functions

In this section we define SmoothBumpCovering ι I M s to be a collection of SmoothBumpFunctions such that their supports is a locally finite family of sets and for each x ∈ s some function f i from the collection is equal to 1 in a neighborhood of x. A covering of this type is useful to construct a smooth partition of unity and can be used instead of a partition of unity in some proofs.

We prove that on a smooth finite dimensional real manifold with σ-compact Hausdorff topology, for any U : M → Set M such that ∀ x ∈ s, U x ∈ 𝓝 x there exists a SmoothBumpCovering ι I M s subordinate to U.

structure SmoothBumpCovering (ι : Type uι) {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type uM) [TopologicalSpace M] [ChartedSpace H M] (s : optParam (Set M) Set.univ) : Type (max uM uι)

We say that a collection of SmoothBumpFunctions is a SmoothBumpCovering of a set s if

• (f i).c ∈ s for all i;
• the family λ i, support (f i) is locally finite;
• for each point x ∈ s there exists i such that f i =ᶠ[𝓝 x] 1; in other words, x belongs to the interior of {y | f i y = 1};

If M is a finite dimensional real manifold which is a σ-compact Hausdorff topological space, then for every covering U : M → Set M, ∀ x, U x ∈ 𝓝 x, there exists a SmoothBumpCovering subordinate to U, see SmoothBumpCovering.exists_isSubordinate.

This covering can be used, e.g., to construct a partition of unity and to prove the weak Whitney embedding theorem.

• c : ι → M

  The center point of each bump in the smooth covering.

• toFun : (i : ι) → SmoothBumpFunction I (self.c i)

  A smooth bump function around c i.

• c_mem' : ∀ (i : ι), self.c i ∈ s

  All the bump functions in the covering are centered at points in s.

• locallyFinite' : LocallyFinite fun (i : ι) => Function.support ↑(self.toFun i)

  Around each point, there are only finitely many nonzero bump functions in the family.

• eventuallyEq_one' : ∀ x ∈ s, ∃ (i : ι), ↑(self.toFun i) =ᶠ[nhds x] 1

  Around each point in s, one of the bump functions is equal to 1.

structure SmoothPartitionOfUnity (ι : Type uι) {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type uM) [TopologicalSpace M] [ChartedSpace H M] (s : optParam (Set M) Set.univ) : Type (max uM uι)

We say that a collection of functions form a smooth partition of unity on a set s if

• all functions are infinitely smooth and nonnegative;
• the family λ i, support (f i) is locally finite;
• for all x ∈ s the sum ∑ᶠ i, f i x equals one;
• for all x, the sum ∑ᶠ i, f i x is less than or equal to one.

• toFun : ι → ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ⊤

  The family of functions forming the partition of unity.

• locallyFinite' : LocallyFinite fun (i : ι) => Function.support ⇑(self.toFun i)

  Around each point, there are only finitely many nonzero functions in the family.

• nonneg' : ∀ (i : ι) (x : M), 0 ≤ (self.toFun i) x

  All the functions in the partition of unity are nonnegative.

• sum_eq_one' : ∀ x ∈ s, (finsum fun (i : ι) => (self.toFun i) x) = 1

  The functions in the partition of unity add up to 1 at any point of s.

• sum_le_one' : ∀ (x : M), (finsum fun (i : ι) => (self.toFun i) x) ≤ 1

  The functions in the partition of unity add up to at most 1 everywhere.

instance SmoothPartitionOfUnity.instFunLikeSmoothPartitionOfUnityContMDiffMapRealToNontriviallyNormedFieldDenselyNormedFieldNormedAddCommGroupToNormedSpaceIsROrCInnerProductSpaceToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupModelWithCornersSelfPseudoMetricSpaceChartedSpaceSelfTopENatInstENatTop {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} : FunLike (SmoothPartitionOfUnity ι I M s) ι (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ⊤)

Equations

• One or more equations did not get rendered due to their size.

theorem SmoothPartitionOfUnity.locallyFinite {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) : LocallyFinite fun (i : ι) => Function.support ⇑(f i)

theorem SmoothPartitionOfUnity.nonneg {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) (i : ι) (x : M) : 0 ≤ (f i) x

theorem SmoothPartitionOfUnity.sum_eq_one {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) {x : M} (hx : x ∈ s) : (finsum fun (i : ι) => (f i) x) = 1

theorem SmoothPartitionOfUnity.exists_pos_of_mem {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) {x : M} (hx : x ∈ s) : ∃ (i : ι), 0 < (f i) x

theorem SmoothPartitionOfUnity.sum_le_one {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) (x : M) : (finsum fun (i : ι) => (f i) x) ≤ 1

def SmoothPartitionOfUnity.toPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) : PartitionOfUnity ι M s

Reinterpret a smooth partition of unity as a continuous partition of unity.

Equations

• One or more equations did not get rendered due to their size.

theorem SmoothPartitionOfUnity.smooth_sum {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) : Smooth I (modelWithCornersSelf ℝ ℝ) fun (x : M) => finsum fun (i : ι) => (f i) x

theorem SmoothPartitionOfUnity.le_one {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) (i : ι) (x : M) : (f i) x ≤ 1

theorem SmoothPartitionOfUnity.sum_nonneg {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) (x : M) : 0 ≤ finsum fun (i : ι) => (f i) x

theorem SmoothPartitionOfUnity.contMDiff_smul {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) {n : ℕ∞} {g : M → F} {i : ι} (hg : ∀ x ∈ tsupport ⇑(f i), ContMDiffAt I (modelWithCornersSelf ℝ F) n g x) : ContMDiff I (modelWithCornersSelf ℝ F) n fun (x : M) => (f i) x • g x

theorem SmoothPartitionOfUnity.smooth_smul {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) {g : M → F} {i : ι} (hg : ∀ x ∈ tsupport ⇑(f i), SmoothAt I (modelWithCornersSelf ℝ F) g x) : Smooth I (modelWithCornersSelf ℝ F) fun (x : M) => (f i) x • g x

theorem SmoothPartitionOfUnity.contMDiff_finsum_smul {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) {n : ℕ∞} {g : ι → M → F} (hg : ∀ (i : ι), ∀ x ∈ tsupport ⇑(f i), ContMDiffAt I (modelWithCornersSelf ℝ F) n (g i) x) : ContMDiff I (modelWithCornersSelf ℝ F) n fun (x : M) => finsum fun (i : ι) => (f i) x • g i x

If f is a smooth partition of unity on a set s : Set M and g : ι → M → F is a family of functions such that g i is $C^n$ smooth at every point of the topological support of f i, then the sum λ x, ∑ᶠ i, f i x • g i x is smooth on the whole manifold.

theorem SmoothPartitionOfUnity.smooth_finsum_smul {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) {g : ι → M → F} (hg : ∀ (i : ι), ∀ x ∈ tsupport ⇑(f i), SmoothAt I (modelWithCornersSelf ℝ F) (g i) x) : Smooth I (modelWithCornersSelf ℝ F) fun (x : M) => finsum fun (i : ι) => (f i) x • g i x

If f is a smooth partition of unity on a set s : Set M and g : ι → M → F is a family of functions such that g i is smooth at every point of the topological support of f i, then the sum λ x, ∑ᶠ i, f i x • g i x is smooth on the whole manifold.

theorem SmoothPartitionOfUnity.contMDiffAt_finsum {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) {n : ℕ∞} {x₀ : M} {g : ι → M → F} (hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I (modelWithCornersSelf ℝ F) n (g i) x₀) : ContMDiffAt I (modelWithCornersSelf ℝ F) n (fun (x : M) => finsum fun (i : ι) => (f i) x • g i x) x₀

theorem SmoothPartitionOfUnity.contDiffAt_finsum {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {s : Set E} (f : SmoothPartitionOfUnity ι (modelWithCornersSelf ℝ E) E s) {x₀ : E} {g : ι → E → F} (hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContDiffAt ℝ n (g i) x₀) : ContDiffAt ℝ n (fun (x : E) => finsum fun (i : ι) => (f i) x • g i x) x₀

theorem SmoothPartitionOfUnity.finsum_smul_mem_convex {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) {g : ι → M → F} {t : Set F} {x : M} (hx : x ∈ s) (hg : ∀ (i : ι), (f i) x ≠ 0 → g i x ∈ t) (ht : Convex ℝ t) : (finsum fun (i : ι) => (f i) x • g i x) ∈ t

def SmoothPartitionOfUnity.IsSubordinate {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) (U : ι → Set M) : Prop

A smooth partition of unity f i is subordinate to a family of sets U i indexed by the same type if for each i the closure of the support of f i is a subset of U i.

Equations

• SmoothPartitionOfUnity.IsSubordinate f U = ∀ (i : ι), tsupport ⇑(f i) ⊆ U i

@[simp]

theorem SmoothPartitionOfUnity.isSubordinate_toPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {f : SmoothPartitionOfUnity ι I M s} {U : ι → Set M} : PartitionOfUnity.IsSubordinate (SmoothPartitionOfUnity.toPartitionOfUnity f) U ↔ SmoothPartitionOfUnity.IsSubordinate f U

theorem SmoothPartitionOfUnity.IsSubordinate.toPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {f : SmoothPartitionOfUnity ι I M s} {U : ι → Set M} : SmoothPartitionOfUnity.IsSubordinate f U → PartitionOfUnity.IsSubordinate (SmoothPartitionOfUnity.toPartitionOfUnity f) U

Alias of the reverse direction of SmoothPartitionOfUnity.isSubordinate_toPartitionOfUnity.

theorem SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {f : SmoothPartitionOfUnity ι I M s} {n : ℕ∞} {U : ι → Set M} {g : ι → M → F} (hf : SmoothPartitionOfUnity.IsSubordinate f U) (ho : ∀ (i : ι), IsOpen (U i)) (hg : ∀ (i : ι), ContMDiffOn I (modelWithCornersSelf ℝ F) n (g i) (U i)) : ContMDiff I (modelWithCornersSelf ℝ F) n fun (x : M) => finsum fun (i : ι) => (f i) x • g i x

If f is a smooth partition of unity on a set s : Set M subordinate to a family of open sets U : ι → Set M and g : ι → M → F is a family of functions such that g i is $C^n$ smooth on U i, then the sum λ x, ∑ᶠ i, f i x • g i x is $C^n$ smooth on the whole manifold.

theorem SmoothPartitionOfUnity.IsSubordinate.smooth_finsum_smul {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {f : SmoothPartitionOfUnity ι I M s} {U : ι → Set M} {g : ι → M → F} (hf : SmoothPartitionOfUnity.IsSubordinate f U) (ho : ∀ (i : ι), IsOpen (U i)) (hg : ∀ (i : ι), SmoothOn I (modelWithCornersSelf ℝ F) (g i) (U i)) : Smooth I (modelWithCornersSelf ℝ F) fun (x : M) => finsum fun (i : ι) => (f i) x • g i x

If f is a smooth partition of unity on a set s : Set M subordinate to a family of open sets U : ι → Set M and g : ι → M → F is a family of functions such that g i is smooth on U i, then the sum λ x, ∑ᶠ i, f i x • g i x is smooth on the whole manifold.

theorem BumpCovering.smooth_toPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : BumpCovering ι M s) (hf : ∀ (i : ι), Smooth I (modelWithCornersSelf ℝ ℝ) ⇑(f i)) (i : ι) : Smooth I (modelWithCornersSelf ℝ ℝ) ⇑((BumpCovering.toPartitionOfUnity f) i)

def BumpCovering.toSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : BumpCovering ι M s) (hf : ∀ (i : ι), Smooth I (modelWithCornersSelf ℝ ℝ) ⇑(f i)) : SmoothPartitionOfUnity ι I M s

A BumpCovering such that all functions in this covering are smooth generates a smooth partition of unity.

In our formalization, not every f : BumpCovering ι M s with smooth functions f i is a SmoothBumpCovering; instead, a SmoothBumpCovering is a covering by supports of SmoothBumpFunctions. So, we define BumpCovering.toSmoothPartitionOfUnity, then reuse it in SmoothBumpCovering.toSmoothPartitionOfUnity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BumpCovering.toSmoothPartitionOfUnity_toPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : BumpCovering ι M s) (hf : ∀ (i : ι), Smooth I (modelWithCornersSelf ℝ ℝ) ⇑(f i)) : SmoothPartitionOfUnity.toPartitionOfUnity (BumpCovering.toSmoothPartitionOfUnity f hf) = BumpCovering.toPartitionOfUnity f

@[simp]

theorem BumpCovering.coe_toSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : BumpCovering ι M s) (hf : ∀ (i : ι), Smooth I (modelWithCornersSelf ℝ ℝ) ⇑(f i)) (i : ι) : ⇑((BumpCovering.toSmoothPartitionOfUnity f hf) i) = ⇑((BumpCovering.toPartitionOfUnity f) i)

theorem BumpCovering.IsSubordinate.toSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {f : BumpCovering ι M s} {U : ι → Set M} (h : BumpCovering.IsSubordinate f U) (hf : ∀ (i : ι), Smooth I (modelWithCornersSelf ℝ ℝ) ⇑(f i)) : SmoothPartitionOfUnity.IsSubordinate (BumpCovering.toSmoothPartitionOfUnity f hf) U

instance SmoothBumpCovering.instCoeFunSmoothBumpCoveringForAllSmoothBumpFunctionC {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} : CoeFun (SmoothBumpCovering ι I M s) fun (x : SmoothBumpCovering ι I M s) => (i : ι) → SmoothBumpFunction I (x.c i)

Equations

• SmoothBumpCovering.instCoeFunSmoothBumpCoveringForAllSmoothBumpFunctionC = { coe := SmoothBumpCovering.toFun s }

def SmoothBumpCovering.IsSubordinate {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : SmoothBumpCovering ι I M s) (U : M → Set M) : Prop

We say that f : SmoothBumpCovering ι I M s is subordinate to a map U : M → Set M if for each index i, we have tsupport (f i) ⊆ U (f i).c. This notion is a bit more general than being subordinate to an open covering of M, because we make no assumption about the way U x depends on x.

Equations

• SmoothBumpCovering.IsSubordinate f U = ∀ (i : ι), tsupport ↑(f.toFun i) ⊆ U (f.c i)

theorem SmoothBumpCovering.IsSubordinate.support_subset {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {fs : SmoothBumpCovering ι I M s} {U : M → Set M} (h : SmoothBumpCovering.IsSubordinate fs U) (i : ι) : Function.support ↑(fs.toFun i) ⊆ U (fs.c i)

theorem SmoothBumpCovering.exists_isSubordinate {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {U : M → Set M} [T2Space M] [SigmaCompactSpace M] (hs : IsClosed s) (hU : ∀ x ∈ s, U x ∈ nhds x) : ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), SmoothBumpCovering.IsSubordinate f U

Let M be a smooth manifold with corners modelled on a finite dimensional real vector space. Suppose also that M is a Hausdorff σ-compact topological space. Let s be a closed set in M and U : M → Set M be a collection of sets such that U x ∈ 𝓝 x for every x ∈ s. Then there exists a smooth bump covering of s that is subordinate to U.

theorem SmoothBumpCovering.locallyFinite {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) : LocallyFinite fun (i : ι) => Function.support ↑(fs.toFun i)

theorem SmoothBumpCovering.point_finite {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M) : Set.Finite {i : ι | ↑(fs.toFun i) x ≠ 0}

theorem SmoothBumpCovering.mem_chartAt_source_of_eq_one {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) {i : ι} {x : M} (h : ↑(fs.toFun i) x = 1) : x ∈ (chartAt H (fs.c i)).toPartialEquiv.source

theorem SmoothBumpCovering.mem_extChartAt_source_of_eq_one {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) {i : ι} {x : M} (h : ↑(fs.toFun i) x = 1) : x ∈ (extChartAt I (fs.c i)).source

def SmoothBumpCovering.ind {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s) : ι

Index of a bump function such that fs i =ᶠ[𝓝 x] 1.

Equations

• SmoothBumpCovering.ind fs x hx = Exists.choose (_ : ∃ (i : ι), ↑(fs.toFun i) =ᶠ[nhds x] 1)

theorem SmoothBumpCovering.eventuallyEq_one {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s) : ↑(fs.toFun (SmoothBumpCovering.ind fs x hx)) =ᶠ[nhds x] 1

theorem SmoothBumpCovering.apply_ind {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s) : ↑(fs.toFun (SmoothBumpCovering.ind fs x hx)) x = 1

theorem SmoothBumpCovering.mem_support_ind {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s) : x ∈ Function.support ↑(fs.toFun (SmoothBumpCovering.ind fs x hx))

theorem SmoothBumpCovering.mem_chartAt_ind_source {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s) : x ∈ (chartAt H (fs.c (SmoothBumpCovering.ind fs x hx))).toPartialEquiv.source

theorem SmoothBumpCovering.mem_extChartAt_ind_source {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s) : x ∈ (extChartAt I (fs.c (SmoothBumpCovering.ind fs x hx))).source

def SmoothBumpCovering.fintype {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (fs : SmoothBumpCovering ι I M s) [CompactSpace M] : Fintype ι

The index type of a SmoothBumpCovering of a compact manifold is finite.

Equations

• One or more equations did not get rendered due to their size.

def SmoothBumpCovering.toBumpCovering {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} (fs : SmoothBumpCovering ι I M s) [T2Space M] : BumpCovering ι M s

Reinterpret a SmoothBumpCovering as a continuous BumpCovering. Note that not every f : BumpCovering ι M s with smooth functions f i is a SmoothBumpCovering.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SmoothBumpCovering.isSubordinate_toBumpCovering {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} [T2Space M] {f : SmoothBumpCovering ι I M s} {U : M → Set M} : (BumpCovering.IsSubordinate (SmoothBumpCovering.toBumpCovering f) fun (i : ι) => U (f.c i)) ↔ SmoothBumpCovering.IsSubordinate f U

theorem SmoothBumpCovering.IsSubordinate.toBumpCovering {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} [T2Space M] {f : SmoothBumpCovering ι I M s} {U : M → Set M} : SmoothBumpCovering.IsSubordinate f U → BumpCovering.IsSubordinate (SmoothBumpCovering.toBumpCovering f) fun (i : ι) => U (f.c i)

Alias of the reverse direction of SmoothBumpCovering.isSubordinate_toBumpCovering.

def SmoothBumpCovering.toSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} (fs : SmoothBumpCovering ι I M s) [T2Space M] : SmoothPartitionOfUnity ι I M s

Every SmoothBumpCovering defines a smooth partition of unity.

Equations

• SmoothBumpCovering.toSmoothPartitionOfUnity fs = BumpCovering.toSmoothPartitionOfUnity (SmoothBumpCovering.toBumpCovering fs) (_ : ∀ (i : ι), Smooth I (modelWithCornersSelf ℝ ℝ) ↑(fs.toFun i))

theorem SmoothBumpCovering.toSmoothPartitionOfUnity_apply {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} (fs : SmoothBumpCovering ι I M s) [T2Space M] (i : ι) (x : M) : ((SmoothBumpCovering.toSmoothPartitionOfUnity fs) i) x = ↑(fs.toFun i) x * finprod fun (j : ι) => finprod fun (x_1 : WellOrderingRel j i) => 1 - ↑(fs.toFun j) x

theorem SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} (fs : SmoothBumpCovering ι I M s) [T2Space M] (i : ι) (x : M) (t : Finset ι) (ht : ∀ (j : ι), WellOrderingRel j i → ↑(fs.toFun j) x ≠ 0 → j ∈ t) : ((SmoothBumpCovering.toSmoothPartitionOfUnity fs) i) x = ↑(fs.toFun i) x * Finset.prod (Finset.filter (fun (j : ι) => WellOrderingRel j i) t) fun (j : ι) => 1 - ↑(fs.toFun j) x

theorem SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} (fs : SmoothBumpCovering ι I M s) [T2Space M] (i : ι) (x : M) : ∃ (t : Finset ι), ⇑((SmoothBumpCovering.toSmoothPartitionOfUnity fs) i) =ᶠ[nhds x] ↑(fs.toFun i) * Finset.prod (Finset.filter (fun (j : ι) => WellOrderingRel j i) t) fun (j : ι) => 1 - ↑(fs.toFun j)

theorem SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} (fs : SmoothBumpCovering ι I M s) [T2Space M] {i : ι} {x : M} (h : ↑(fs.toFun i) x = 0) : ((SmoothBumpCovering.toSmoothPartitionOfUnity fs) i) x = 0

theorem SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} (fs : SmoothBumpCovering ι I M s) [T2Space M] (i : ι) : Function.support ⇑((SmoothBumpCovering.toSmoothPartitionOfUnity fs) i) ⊆ Function.support ↑(fs.toFun i)

theorem SmoothBumpCovering.IsSubordinate.toSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} [T2Space M] {f : SmoothBumpCovering ι I M s} {U : M → Set M} (h : SmoothBumpCovering.IsSubordinate f U) : SmoothPartitionOfUnity.IsSubordinate (SmoothBumpCovering.toSmoothPartitionOfUnity f) fun (i : ι) => U (f.c i)

theorem SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} (fs : SmoothBumpCovering ι I M s) [T2Space M] (x : M) : (finsum fun (i : ι) => ((SmoothBumpCovering.toSmoothPartitionOfUnity fs) i) x) = 1 - finprod fun (i : ι) => 1 - ↑(fs.toFun i) x

theorem exists_smooth_zero_one_of_isClosed {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [T2Space M] [SigmaCompactSpace M] {s : Set M} {t : Set M} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ⊤), Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Set.Icc 0 1

Given two disjoint closed sets s, t in a Hausdorff σ-compact finite dimensional manifold, there exists an infinitely smooth function that is equal to 0 on s and to 1 on t. See also exists_msmooth_zero_iff_one_iff_of_isClosed, which ensures additionally that f is equal to 0 exactly on s and to 1 exactly on t.

theorem exists_smooth_zero_one_nhds_of_isClosed {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [T2Space M] [NormalSpace M] [SigmaCompactSpace M] {s : Set M} {t : Set M} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ⊤), (∀ᶠ (x : M) in nhdsSet s, f x = 0) ∧ (∀ᶠ (x : M) in nhdsSet t, f x = 1) ∧ ∀ (x : M), f x ∈ Set.Icc 0 1

Given two disjoint closed sets s, t in a Hausdorff normal σ-compact finite dimensional manifold M, there exists a smooth function f : M → [0,1] that vanishes in a neighbourhood of s and is equal to 1 in a neighbourhood of t.

theorem exists_smooth_one_nhds_of_subset_interior {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [T2Space M] [NormalSpace M] [SigmaCompactSpace M] {s : Set M} {t : Set M} (hs : IsClosed s) (hd : s ⊆ interior t) : ∃ (f : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ⊤), (∀ᶠ (x : M) in nhdsSet s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ (x : M), f x ∈ Set.Icc 0 1

Given two sets s, t in a Hausdorff normal σ-compact finite-dimensional manifold M with s open and s ⊆ interior t, there is a smooth function f : M → [0,1] which is equal to s in a neighbourhood of s and has support contained in t.

def SmoothPartitionOfUnity.single {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] (i : ι) (s : Set M) : SmoothPartitionOfUnity ι I M s

A SmoothPartitionOfUnity that consists of a single function, uniformly equal to one, defined as an example for Inhabited instance.

Equations

• SmoothPartitionOfUnity.single I i s = BumpCovering.toSmoothPartitionOfUnity (BumpCovering.single i s) (_ : ∀ (j : ι), Smooth I (modelWithCornersSelf ℝ ℝ) ⇑((BumpCovering.single i s) j))

instance SmoothPartitionOfUnity.instInhabitedSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [Inhabited ι] (s : Set M) : Inhabited (SmoothPartitionOfUnity ι I M s)

Equations

• SmoothPartitionOfUnity.instInhabitedSmoothPartitionOfUnity I s = { default := SmoothPartitionOfUnity.single I default s }

theorem SmoothPartitionOfUnity.exists_isSubordinate {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [T2Space M] [SigmaCompactSpace M] {s : Set M} (hs : IsClosed s) (U : ι → Set M) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⊆ ⋃ (i : ι), U i) : ∃ (f : SmoothPartitionOfUnity ι I M s), SmoothPartitionOfUnity.IsSubordinate f U

If X is a paracompact normal topological space and U is an open covering of a closed set s, then there exists a SmoothPartitionOfUnity ι M s that is subordinate to U.

theorem SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source_of_isClosed {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [T2Space M] [SigmaCompactSpace M] {s : Set M} (hs : IsClosed s) : ∃ (f : SmoothPartitionOfUnity (↑s) I M s), SmoothPartitionOfUnity.IsSubordinate f fun (x : ↑s) => (chartAt H ↑x).toPartialEquiv.source

theorem SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type uM) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [T2Space M] [SigmaCompactSpace M] : ∃ (f : SmoothPartitionOfUnity M I M), SmoothPartitionOfUnity.IsSubordinate f fun (x : M) => (chartAt H x).toPartialEquiv.source

theorem exists_contMDiffOn_forall_mem_convex_of_local {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] {t : M → Set F} {n : ℕ∞} (ht : ∀ (x : M), Convex ℝ (t x)) (Hloc : ∀ (x : M), ∃ U ∈ nhds x, ∃ (g : M → F), ContMDiffOn I (modelWithCornersSelf ℝ F) n g U ∧ ∀ y ∈ U, g y ∈ t y) : ∃ (g : ContMDiffMap I (modelWithCornersSelf ℝ F) M F n), ∀ (x : M), g x ∈ t x

Let M be a σ-compact Hausdorff finite dimensional topological manifold. Let t : M → Set F be a family of convex sets. Suppose that for each point x : M there exists a neighborhood U ∈ 𝓝 x and a function g : M → F such that g is $C^n$ smooth on U and g y ∈ t y for all y ∈ U. Then there exists a $C^n$ smooth function g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯ such that g x ∈ t x for all x. See also exists_smooth_forall_mem_convex_of_local and exists_smooth_forall_mem_convex_of_local_const.

theorem exists_smooth_forall_mem_convex_of_local {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] {t : M → Set F} (ht : ∀ (x : M), Convex ℝ (t x)) (Hloc : ∀ (x : M), ∃ U ∈ nhds x, ∃ (g : M → F), SmoothOn I (modelWithCornersSelf ℝ F) g U ∧ ∀ y ∈ U, g y ∈ t y) : ∃ (g : ContMDiffMap I (modelWithCornersSelf ℝ F) M F ⊤), ∀ (x : M), g x ∈ t x

Let M be a σ-compact Hausdorff finite dimensional topological manifold. Let t : M → Set F be a family of convex sets. Suppose that for each point x : M there exists a neighborhood U ∈ 𝓝 x and a function g : M → F such that g is smooth on U and g y ∈ t y for all y ∈ U. Then there exists a smooth function g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯ such that g x ∈ t x for all x. See also exists_contMDiffOn_forall_mem_convex_of_local and exists_smooth_forall_mem_convex_of_local_const.

theorem exists_smooth_forall_mem_convex_of_local_const {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] {t : M → Set F} (ht : ∀ (x : M), Convex ℝ (t x)) (Hloc : ∀ (x : M), ∃ (c : F), ∀ᶠ (y : M) in nhds x, c ∈ t y) : ∃ (g : ContMDiffMap I (modelWithCornersSelf ℝ F) M F ⊤), ∀ (x : M), g x ∈ t x

Let M be a σ-compact Hausdorff finite dimensional topological manifold. Let t : M → Set F be a family of convex sets. Suppose that for each point x : M there exists a vector c : F such that for all y in a neighborhood of x we have c ∈ t y. Then there exists a smooth function g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯ such that g x ∈ t x for all x. See also exists_contMDiffOn_forall_mem_convex_of_local and exists_smooth_forall_mem_convex_of_local.

theorem Emetric.exists_smooth_forall_closedBall_subset {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_1} [EMetricSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] {K : ι → Set M} {U : ι → Set M} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) : ∃ (δ : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ⊤), (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i

Let M be a smooth σ-compact manifold with extended distance. Let K : ι → Set M be a locally finite family of closed sets, let U : ι → Set M be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive smooth function δ : M → ℝ≥0 such that for any i and x ∈ K i, we have EMetric.closedBall x (δ x) ⊆ U i.

theorem Metric.exists_smooth_forall_closedBall_subset {ι : Type uι} {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_1} [MetricSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] {K : ι → Set M} {U : ι → Set M} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i ⊆ U i) (hfin : LocallyFinite K) : ∃ (δ : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ⊤), (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedBall x (δ x) ⊆ U i

Let M be a smooth σ-compact manifold with a metric. Let K : ι → Set M be a locally finite family of closed sets, let U : ι → Set M be a family of open sets such that K i ⊆ U i for all i. Then there exists a positive smooth function δ : M → ℝ≥0 such that for any i and x ∈ K i, we have Metric.closedBall x (δ x) ⊆ U i.

theorem IsOpen.exists_msmooth_support_eq_aux {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {s : Set H} (hs : IsOpen s) : ∃ (f : H → ℝ), Function.support f = s ∧ Smooth I (modelWithCornersSelf ℝ ℝ) f ∧ Set.range f ⊆ Set.Icc 0 1

theorem IsOpen.exists_msmooth_support_eq {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] {s : Set M} (hs : IsOpen s) : ∃ (f : M → ℝ), Function.support f = s ∧ Smooth I (modelWithCornersSelf ℝ ℝ) f ∧ ∀ (x : M), 0 ≤ f x

Given an open set in a finite-dimensional real manifold, there exists a nonnegative smooth function with support equal to s.

theorem exists_msmooth_support_eq_eq_one_iff {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] {s : Set M} {t : Set M} (hs : IsOpen s) (ht : IsClosed t) (h : t ⊆ s) : ∃ (f : M → ℝ), Smooth I (modelWithCornersSelf ℝ ℝ) f ∧ Set.range f ⊆ Set.Icc 0 1 ∧ Function.support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Given an open set s containing a closed set t in a finite-dimensional real manifold, there exists a smooth function with support equal to s, taking values in [0,1], and equal to 1 exactly on t.

theorem exists_msmooth_zero_iff_one_iff_of_isClosed {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] {s : Set M} {t : Set M} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ (f : M → ℝ), 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

Given two disjoint closed sets s, t in a Hausdorff σ-compact finite dimensional manifold, there exists an infinitely smooth function that is equal to 0 exactly on s and to 1 exactly on t. See also exists_smooth_zero_one_of_isClosed for a slightly weaker version.