# 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} [] [] {H : Type uH} [] (I : ) (M : Type uM) [] [] (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 fun 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' : xs, ∃ (i : ι), (self.toFun i) =ᶠ[nhds x] 1

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

Instances For
theorem SmoothBumpCovering.c_mem' {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : optParam (Set M) Set.univ} (self : ) (i : ι) :
self.c i s

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

theorem SmoothBumpCovering.locallyFinite' {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : optParam (Set M) Set.univ} (self : ) :
LocallyFinite fun (i : ι) => Function.support (self.toFun i)

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

theorem SmoothBumpCovering.eventuallyEq_one' {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : optParam (Set M) Set.univ} (self : ) (x : M) :
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} [] {H : Type uH} [] (I : ) (M : Type uM) [] [] (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 fun 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 : ι

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' : xs, ∑ᶠ (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), ∑ᶠ (i : ι), (self.toFun i) x 1

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

Instances For
theorem SmoothPartitionOfUnity.locallyFinite' {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : optParam (Set M) Set.univ} (self : ) :
LocallyFinite fun (i : ι) => Function.support (self.toFun i)

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

theorem SmoothPartitionOfUnity.nonneg' {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : optParam (Set M) Set.univ} (self : ) (i : ι) (x : M) :
0 (self.toFun i) x

All the functions in the partition of unity are nonnegative.

theorem SmoothPartitionOfUnity.sum_eq_one' {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : optParam (Set M) Set.univ} (self : ) (x : M) :
x s∑ᶠ (i : ι), (self.toFun i) x = 1

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

theorem SmoothPartitionOfUnity.sum_le_one' {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : optParam (Set M) Set.univ} (self : ) (x : M) :
∑ᶠ (i : ι), (self.toFun i) x 1

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

instance SmoothPartitionOfUnity.instFunLikeContMDiffMapRealModelWithCornersSelfTopENat {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} :
FunLike () ι ()
Equations
• SmoothPartitionOfUnity.instFunLikeContMDiffMapRealModelWithCornersSelfTopENat = { coe := SmoothPartitionOfUnity.toFun, coe_injective' := }
theorem SmoothPartitionOfUnity.locallyFinite {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) :
LocallyFinite fun (i : ι) => Function.support (f i)
theorem SmoothPartitionOfUnity.nonneg {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) (i : ι) (x : M) :
0 (f i) x
theorem SmoothPartitionOfUnity.sum_eq_one {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) {x : M} (hx : x s) :
∑ᶠ (i : ι), (f i) x = 1
theorem SmoothPartitionOfUnity.exists_pos_of_mem {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) {x : M} (hx : x s) :
∃ (i : ι), 0 < (f i) x
theorem SmoothPartitionOfUnity.sum_le_one {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) (x : M) :
∑ᶠ (i : ι), (f i) x 1
@[simp]
theorem SmoothPartitionOfUnity.toPartitionOfUnity_toFun {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) (i : ι) :
f.toPartitionOfUnity i = (f i)
def SmoothPartitionOfUnity.toPartitionOfUnity {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) :

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

Equations
• f.toPartitionOfUnity = { toFun := fun (i : ι) => (f i), locallyFinite' := , nonneg' := , sum_eq_one' := , sum_le_one' := }
Instances For
theorem SmoothPartitionOfUnity.smooth_sum {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) :
Smooth I fun (x : M) => ∑ᶠ (i : ι), (f i) x
theorem SmoothPartitionOfUnity.le_one {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) (i : ι) (x : M) :
(f i) x 1
theorem SmoothPartitionOfUnity.sum_nonneg {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) (x : M) :
0 ∑ᶠ (i : ι), (f i) x
theorem SmoothPartitionOfUnity.contMDiff_smul {ι : Type uι} {E : Type uE} [] {F : Type uF} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) {n : ℕ∞} {g : MF} {i : ι} (hg : xtsupport (f i), ContMDiffAt I n g x) :
ContMDiff I n fun (x : M) => (f i) x g x
theorem SmoothPartitionOfUnity.smooth_smul {ι : Type uι} {E : Type uE} [] {F : Type uF} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) {g : MF} {i : ι} (hg : xtsupport (f i), SmoothAt I g x) :
Smooth I fun (x : M) => (f i) x g x
theorem SmoothPartitionOfUnity.contMDiff_finsum_smul {ι : Type uι} {E : Type uE} [] {F : Type uF} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) {n : ℕ∞} {g : ιMF} (hg : ∀ (i : ι), xtsupport (f i), ContMDiffAt I n (g i) x) :
ContMDiff I n fun (x : M) => ∑ᶠ (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 fun x ↦ ∑ᶠ i, f i x • g i x is smooth on the whole manifold.

theorem SmoothPartitionOfUnity.smooth_finsum_smul {ι : Type uι} {E : Type uE} [] {F : Type uF} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) {g : ιMF} (hg : ∀ (i : ι), xtsupport (f i), SmoothAt I (g i) x) :
Smooth I fun (x : M) => ∑ᶠ (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 fun x ↦ ∑ᶠ i, f i x • g i x is smooth on the whole manifold.

theorem SmoothPartitionOfUnity.contMDiffAt_finsum {ι : Type uι} {E : Type uE} [] {F : Type uF} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) {n : ℕ∞} {x₀ : M} {g : ιMF} (hφ : ∀ (i : ι), x₀ tsupport (f i)ContMDiffAt I n (g i) x₀) :
ContMDiffAt I n (fun (x : M) => ∑ᶠ (i : ι), (f i) x g i x) x₀
theorem SmoothPartitionOfUnity.contDiffAt_finsum {ι : Type uι} {E : Type uE} [] {F : Type uF} [] {n : ℕ∞} {s : Set E} (f : ) {x₀ : E} {g : ιEF} (hφ : ∀ (i : ι), x₀ tsupport (f i)ContDiffAt n (g i) x₀) :
ContDiffAt n (fun (x : E) => ∑ᶠ (i : ι), (f i) x g i x) x₀
theorem SmoothPartitionOfUnity.finsum_smul_mem_convex {ι : Type uι} {E : Type uE} [] {F : Type uF} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) {g : ιMF} {t : Set F} {x : M} (hx : x s) (hg : ∀ (i : ι), (f i) x 0g i x t) (ht : ) :
∑ᶠ (i : ι), (f i) x g i x t
def SmoothPartitionOfUnity.finsupport {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) :

The support of a smooth partition of unity at a point x₀ as a Finset. This is the set of i : ι such that x₀ ∈ support f i, i.e. f i ≠ x₀.

Equations
• ρ.finsupport x₀ = ρ.toPartitionOfUnity.finsupport x₀
Instances For
@[simp]
theorem SmoothPartitionOfUnity.mem_finsupport {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) {i : ι} :
i ρ.finsupport x₀ i Function.support fun (i : ι) => (ρ i) x₀
@[simp]
theorem SmoothPartitionOfUnity.coe_finsupport {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) :
(ρ.finsupport x₀) = Function.support fun (i : ι) => (ρ i) x₀
theorem SmoothPartitionOfUnity.sum_finsupport {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) (hx₀ : x₀ s) :
iρ.finsupport x₀, (ρ i) x₀ = 1
theorem SmoothPartitionOfUnity.sum_finsupport' {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) (hx₀ : x₀ s) {I : } (hI : ρ.finsupport x₀ I) :
iI, (ρ i) x₀ = 1
theorem SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) {A : Type u_1} [] [] (φ : ιMA) :
iρ.finsupport x₀, (ρ i) x₀ φ i x₀ = ∑ᶠ (i : ι), (ρ i) x₀ φ i x₀
theorem SmoothPartitionOfUnity.finite_tsupport {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) :
{i : ι | x₀ tsupport (ρ i)}.Finite

The tsupports of a smooth partition of unity are locally finite.

def SmoothPartitionOfUnity.fintsupport {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x : M) :

The tsupport of a partition of unity at a point x₀ as a Finset. This is the set of i : ι such that x₀ ∈ tsupport f i.

Equations
• ρ.fintsupport x = .toFinset
Instances For
theorem SmoothPartitionOfUnity.mem_fintsupport_iff {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) (i : ι) :
i ρ.fintsupport x₀ x₀ tsupport (ρ i)
theorem SmoothPartitionOfUnity.eventually_fintsupport_subset {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) :
∀ᶠ (y : M) in nhds x₀, ρ.fintsupport y ρ.fintsupport x₀
theorem SmoothPartitionOfUnity.finsupport_subset_fintsupport {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) :
ρ.finsupport x₀ ρ.fintsupport x₀
theorem SmoothPartitionOfUnity.eventually_finsupport_subset {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (ρ : ) (x₀ : M) :
∀ᶠ (y : M) in nhds x₀, ρ.finsupport y ρ.fintsupport x₀
def SmoothPartitionOfUnity.IsSubordinate {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) (U : ιSet M) :

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
Instances For
@[simp]
theorem SmoothPartitionOfUnity.isSubordinate_toPartitionOfUnity {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} {f : } {U : ιSet M} :
f.toPartitionOfUnity.IsSubordinate U f.IsSubordinate U
theorem SmoothPartitionOfUnity.IsSubordinate.toPartitionOfUnity {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} {f : } {U : ιSet M} :
f.IsSubordinate Uf.toPartitionOfUnity.IsSubordinate U

Alias of the reverse direction of SmoothPartitionOfUnity.isSubordinate_toPartitionOfUnity.

theorem SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul {ι : Type uι} {E : Type uE} [] {F : Type uF} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} {f : } {n : ℕ∞} {U : ιSet M} {g : ιMF} (hf : f.IsSubordinate U) (ho : ∀ (i : ι), IsOpen (U i)) (hg : ∀ (i : ι), ContMDiffOn I n (g i) (U i)) :
ContMDiff I n fun (x : M) => ∑ᶠ (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 fun 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} [] {F : Type uF} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} {f : } {U : ιSet M} {g : ιMF} (hf : f.IsSubordinate U) (ho : ∀ (i : ι), IsOpen (U i)) (hg : ∀ (i : ι), SmoothOn I (g i) (U i)) :
Smooth I fun (x : M) => ∑ᶠ (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 fun x ↦ ∑ᶠ i, f i x • g i x is smooth on the whole manifold.

theorem BumpCovering.smooth_toPartitionOfUnity {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : BumpCovering ι M s) (hf : ∀ (i : ι), Smooth I (f i)) (i : ι) :
Smooth I (f.toPartitionOfUnity i)
def BumpCovering.toSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : BumpCovering ι M s) (hf : ∀ (i : ι), Smooth I (f i)) :

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.
Instances For
@[simp]
theorem BumpCovering.toSmoothPartitionOfUnity_toPartitionOfUnity {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : BumpCovering ι M s) (hf : ∀ (i : ι), Smooth I (f i)) :
(f.toSmoothPartitionOfUnity hf).toPartitionOfUnity = f.toPartitionOfUnity
@[simp]
theorem BumpCovering.coe_toSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : BumpCovering ι M s) (hf : ∀ (i : ι), Smooth I (f i)) (i : ι) :
((f.toSmoothPartitionOfUnity hf) i) = (f.toPartitionOfUnity i)
theorem BumpCovering.IsSubordinate.toSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} {f : BumpCovering ι M s} {U : ιSet M} (h : f.IsSubordinate U) (hf : ∀ (i : ι), Smooth I (f i)) :
(f.toSmoothPartitionOfUnity hf).IsSubordinate U
instance SmoothBumpCovering.instCoeFunForallSmoothBumpFunctionC {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} :
CoeFun () fun (x : ) => (i : ι) → SmoothBumpFunction I (x.c i)
Equations
• SmoothBumpCovering.instCoeFunForallSmoothBumpFunctionC = { coe := SmoothBumpCovering.toFun }
def SmoothBumpCovering.IsSubordinate {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (f : ) (U : MSet M) :

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
• f.IsSubordinate U = ∀ (i : ι), tsupport (f.toFun i) U (f.c i)
Instances For
theorem SmoothBumpCovering.IsSubordinate.support_subset {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} {fs : } {U : MSet M} (h : fs.IsSubordinate U) (i : ι) :
Function.support (fs.toFun i) U (fs.c i)
theorem SmoothBumpCovering.exists_isSubordinate {E : Type uE} [] [] {H : Type uH} [] (I : ) {M : Type uM} [] [] {s : Set M} {U : MSet M} [] (hs : ) (hU : xs, U x nhds x) :
∃ (ι : Type uM) (f : ), f.IsSubordinate 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} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) :
LocallyFinite fun (i : ι) => Function.support (fs.toFun i)
theorem SmoothBumpCovering.point_finite {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) (x : M) :
{i : ι | (fs.toFun i) x 0}.Finite
theorem SmoothBumpCovering.mem_chartAt_source_of_eq_one {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) {i : ι} {x : M} (h : (fs.toFun i) x = 1) :
x (chartAt H (fs.c i)).source
theorem SmoothBumpCovering.mem_extChartAt_source_of_eq_one {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) {i : ι} {x : M} (h : (fs.toFun i) x = 1) :
x (extChartAt I (fs.c i)).source
def SmoothBumpCovering.ind {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) (x : M) (hx : x s) :
ι

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

Equations
• fs.ind x hx = .choose
Instances For
theorem SmoothBumpCovering.eventuallyEq_one {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) (x : M) (hx : x s) :
(fs.toFun (fs.ind x hx)) =ᶠ[nhds x] 1
theorem SmoothBumpCovering.apply_ind {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) (x : M) (hx : x s) :
(fs.toFun (fs.ind x hx)) x = 1
theorem SmoothBumpCovering.mem_support_ind {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) (x : M) (hx : x s) :
x Function.support (fs.toFun (fs.ind x hx))
theorem SmoothBumpCovering.mem_chartAt_ind_source {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) (x : M) (hx : x s) :
x (chartAt H (fs.c (fs.ind x hx))).source
theorem SmoothBumpCovering.mem_extChartAt_ind_source {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) (x : M) (hx : x s) :
x (extChartAt I (fs.c (fs.ind x hx))).source
def SmoothBumpCovering.fintype {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) [] :

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

Equations
• fs.fintype = .fintypeOfCompact
Instances For
def SmoothBumpCovering.toBumpCovering {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) [] :

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

Equations
• fs.toBumpCovering = { toFun := fun (i : ι) => { toFun := (fs.toFun i), continuous_toFun := }, locallyFinite' := , nonneg' := , le_one' := , eventuallyEq_one' := }
Instances For
@[simp]
theorem SmoothBumpCovering.isSubordinate_toBumpCovering {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} [] {f : } {U : MSet M} :
(f.toBumpCovering.IsSubordinate fun (i : ι) => U (f.c i)) f.IsSubordinate U
theorem SmoothBumpCovering.IsSubordinate.toBumpCovering {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} [] {f : } {U : MSet M} :
f.IsSubordinate Uf.toBumpCovering.IsSubordinate fun (i : ι) => U (f.c i)

Alias of the reverse direction of SmoothBumpCovering.isSubordinate_toBumpCovering.

def SmoothBumpCovering.toSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) [] :

Every SmoothBumpCovering defines a smooth partition of unity.

Equations
• fs.toSmoothPartitionOfUnity = fs.toBumpCovering.toSmoothPartitionOfUnity
Instances For
theorem SmoothBumpCovering.toSmoothPartitionOfUnity_apply {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) [] (i : ι) (x : M) :
(fs.toSmoothPartitionOfUnity i) x = (fs.toFun i) x * ∏ᶠ (j : ι) (_ : ), (1 - (fs.toFun j) x)
theorem SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) [] (i : ι) (x : M) (t : ) (ht : ∀ (j : ι), (fs.toFun j) x 0j t) :
(fs.toSmoothPartitionOfUnity i) x = (fs.toFun i) x * jFinset.filter (fun (j : ι) => ) t, (1 - (fs.toFun j) x)
theorem SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) [] (i : ι) (x : M) :
∃ (t : ), (fs.toSmoothPartitionOfUnity i) =ᶠ[nhds x] (fs.toFun i) * jFinset.filter (fun (j : ι) => ) t, (1 - (fs.toFun j))
theorem SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) [] {i : ι} {x : M} (h : (fs.toFun i) x = 0) :
(fs.toSmoothPartitionOfUnity i) x = 0
theorem SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) [] (i : ι) :
Function.support (fs.toSmoothPartitionOfUnity i) Function.support (fs.toFun i)
theorem SmoothBumpCovering.IsSubordinate.toSmoothPartitionOfUnity {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} [] {f : } {U : MSet M} (h : f.IsSubordinate U) :
f.toSmoothPartitionOfUnity.IsSubordinate fun (i : ι) => U (f.c i)
theorem SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] {I : } {M : Type uM} [] [] {s : Set M} (fs : ) [] (x : M) :
∑ᶠ (i : ι), (fs.toSmoothPartitionOfUnity i) x = 1 - ∏ᶠ (i : ι), (1 - (fs.toFun i) x)
theorem exists_smooth_zero_one_of_isClosed {E : Type uE} [] [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] {s : Set M} {t : Set M} (hs : ) (ht : ) (hd : Disjoint s t) :
∃ (f : ), 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} [] [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] [] {s : Set M} {t : Set M} (hs : ) (ht : ) (hd : Disjoint s t) :
∃ (f : ), (∀ᶠ (x : M) in , f x = 0) (∀ᶠ (x : M) in , 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} [] [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] [] {s : Set M} {t : Set M} (hs : ) (hd : s ) :
∃ (f : ), (∀ᶠ (x : M) in , f x = 1) (xt, 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} [] {H : Type uH} [] (I : ) {M : Type uM} [] [] (i : ι) (s : Set M) :

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

Equations
• = ().toSmoothPartitionOfUnity
Instances For
instance SmoothPartitionOfUnity.instInhabited {ι : Type uι} {E : Type uE} [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] (s : Set M) :
Equations
theorem SmoothPartitionOfUnity.exists_isSubordinate {ι : Type uι} {E : Type uE} [] [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] {s : Set M} (hs : ) (U : ιSet M) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⋃ (i : ι), U i) :
∃ (f : ), f.IsSubordinate 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} [] [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] {s : Set M} (hs : ) :
∃ (f : SmoothPartitionOfUnity (s) I M s), f.IsSubordinate fun (x : s) => (chartAt H x).source
theorem SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source {E : Type uE} [] [] {H : Type uH} [] (I : ) (M : Type uM) [] [] [] :
∃ (f : ), f.IsSubordinate fun (x : M) => (chartAt H x).source
theorem exists_contMDiffOn_forall_mem_convex_of_local {E : Type uE} [] [] {F : Type uF} [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] {t : MSet F} {n : ℕ∞} (ht : ∀ (x : M), Convex (t x)) (Hloc : ∀ (x : M), Unhds x, ∃ (g : MF), ContMDiffOn I n g U yU, g y t y) :
∃ (g : ContMDiffMap I 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} [] [] {F : Type uF} [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] {t : MSet F} (ht : ∀ (x : M), Convex (t x)) (Hloc : ∀ (x : M), Unhds x, ∃ (g : MF), SmoothOn I g U yU, g y t y) :
∃ (g : ), ∀ (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} [] [] {F : Type uF} [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] {t : MSet F} (ht : ∀ (x : M), Convex (t x)) (Hloc : ∀ (x : M), ∃ (c : F), ∀ᶠ (y : M) in nhds x, c t y) :
∃ (g : ), ∀ (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} [] [] {H : Type uH} [] (I : ) {M : Type u_1} [] [] {K : ιSet M} {U : ιSet M} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : ) :
∃ (δ : ), (∀ (x : M), 0 < δ x) ∀ (i : ι), xK 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} [] [] {H : Type uH} [] (I : ) {M : Type u_1} [] [] {K : ιSet M} {U : ιSet M} (hK : ∀ (i : ι), IsClosed (K i)) (hU : ∀ (i : ι), IsOpen (U i)) (hKU : ∀ (i : ι), K i U i) (hfin : ) :
∃ (δ : ), (∀ (x : M), 0 < δ x) ∀ (i : ι), xK 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} [] [] {H : Type uH} [] (I : ) {s : Set H} (hs : ) :
∃ (f : H), Set.Icc 0 1
theorem IsOpen.exists_msmooth_support_eq {E : Type uE} [] [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] {s : Set M} (hs : ) :
∃ (f : M), ∀ (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} [] [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] {s : Set M} {t : Set M} (hs : ) (ht : ) (h : t s) :
∃ (f : M), Set.Icc 0 1 ∀ (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} [] [] {H : Type uH} [] (I : ) {M : Type uM} [] [] [] {s : Set M} {t : Set M} (hs : ) (ht : ) (hd : Disjoint s t) :
∃ (f : M), 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.