Documentation

Mathlib.Geometry.Manifold.PartitionOfUnity

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

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 #

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 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} [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} (self : SmoothBumpCovering ι I M s) (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} [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} (self : SmoothBumpCovering ι I M s) :
    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} [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} (self : SmoothBumpCovering ι I M s) (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} [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 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.
    • 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} [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} (self : SmoothPartitionOfUnity ι I M s) :
      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} [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} (self : SmoothPartitionOfUnity ι I M s) (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} [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} (self : SmoothPartitionOfUnity ι I M s) (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} [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} (self : SmoothPartitionOfUnity ι I M s) (x : M) :
      ∑ᶠ (i : ι), (self.toFun i) x 1

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

      Equations
      • SmoothPartitionOfUnity.instFunLikeContMDiffMapRealModelWithCornersSelfTopENat = { coe := SmoothPartitionOfUnity.toFun, coe_injective' := }
      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) :
      ∑ᶠ (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) :
      ∑ᶠ (i : ι), (f i) x 1
      @[simp]
      theorem SmoothPartitionOfUnity.toPartitionOfUnity_toFun {ι : 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 : ι) :
      f.toPartitionOfUnity i = (f i)

      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} [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) => ∑ᶠ (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 ∑ᶠ (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 : MF} {i : ι} (hg : xtsupport (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 : MF} {i : ι} (hg : xtsupport (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 : ιMF} (hg : ∀ (i : ι), xtsupport (f i), ContMDiffAt I (modelWithCornersSelf F) n (g i) x) :
        ContMDiff I (modelWithCornersSelf F) 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} [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 : ιMF} (hg : ∀ (i : ι), xtsupport (f i), SmoothAt I (modelWithCornersSelf F) (g i) x) :
        Smooth I (modelWithCornersSelf F) 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} [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 : ιMF} (hφ : ∀ (i : ι), x₀ tsupport (f i)ContMDiffAt I (modelWithCornersSelf F) n (g i) x₀) :
        ContMDiffAt I (modelWithCornersSelf F) n (fun (x : M) => ∑ᶠ (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 : ι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} [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 : ιMF} {t : Set F} {x : M} (hx : x s) (hg : ∀ (i : ι), (f i) x 0g i x t) (ht : Convex t) :
        ∑ᶠ (i : ι), (f i) x g i x t
        def SmoothPartitionOfUnity.finsupport {ι : 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} (ρ : SmoothPartitionOfUnity ι I M s) (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} [NormedAddCommGroup E] [NormedSpace E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) {i : ι} :
          i ρ.finsupport x₀ i Function.support fun (i : ι) => (ρ i) x₀
          @[simp]
          theorem SmoothPartitionOfUnity.coe_finsupport {ι : 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} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) :
          (ρ.finsupport x₀) = Function.support fun (i : ι) => (ρ i) x₀
          theorem SmoothPartitionOfUnity.sum_finsupport {ι : 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} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) (hx₀ : x₀ s) :
          iρ.finsupport x₀, (ρ i) x₀ = 1
          theorem SmoothPartitionOfUnity.sum_finsupport' {ι : 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} (ρ : SmoothPartitionOfUnity ι I✝ M s) (x₀ : M) (hx₀ : x₀ s) {I : Finset ι} (hI : ρ.finsupport x₀ I) :
          iI, (ρ i) x₀ = 1
          theorem SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum {ι : 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} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) {A : Type u_1} [AddCommGroup A] [Module A] (φ : ιMA) :
          iρ.finsupport x₀, (ρ i) x₀ φ i x₀ = ∑ᶠ (i : ι), (ρ i) x₀ φ i x₀
          theorem SmoothPartitionOfUnity.finite_tsupport {ι : 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} (ρ : SmoothPartitionOfUnity ι I M s) (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} [NormedAddCommGroup E] [NormedSpace E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (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} [NormedAddCommGroup E] [NormedSpace E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) (i : ι) :
            i ρ.fintsupport x₀ x₀ tsupport (ρ i)
            theorem SmoothPartitionOfUnity.eventually_fintsupport_subset {ι : 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} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) :
            ∀ᶠ (y : M) in nhds x₀, ρ.fintsupport y ρ.fintsupport x₀
            theorem SmoothPartitionOfUnity.finsupport_subset_fintsupport {ι : 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} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) :
            ρ.finsupport x₀ ρ.fintsupport x₀
            theorem SmoothPartitionOfUnity.eventually_finsupport_subset {ι : 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} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M) :
            ∀ᶠ (y : M) in nhds x₀, ρ.finsupport y ρ.fintsupport x₀
            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) :

            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} [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} :
              f.toPartitionOfUnity.IsSubordinate U f.IsSubordinate 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} :
              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} [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 : ιMF} (hf : f.IsSubordinate 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) => ∑ᶠ (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} [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 : ιMF} (hf : f.IsSubordinate U) (ho : ∀ (i : ι), IsOpen (U i)) (hg : ∀ (i : ι), SmoothOn I (modelWithCornersSelf F) (g i) (U i)) :
              Smooth I (modelWithCornersSelf F) 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} [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 ) (f.toPartitionOfUnity 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)) :

              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} [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)) :
                (f.toSmoothPartitionOfUnity hf).toPartitionOfUnity = f.toPartitionOfUnity
                @[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 : ι) :
                ((f.toSmoothPartitionOfUnity hf) i) = (f.toPartitionOfUnity 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 : f.IsSubordinate U) (hf : ∀ (i : ι), Smooth I (modelWithCornersSelf ) (f i)) :
                (f.toSmoothPartitionOfUnity hf).IsSubordinate U
                instance SmoothBumpCovering.instCoeFunForallSmoothBumpFunctionC {ι : 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.instCoeFunForallSmoothBumpFunctionC = { coe := SmoothBumpCovering.toFun }
                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 : 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} [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 : MSet M} (h : fs.IsSubordinate 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 : MSet M} [T2Space M] [SigmaCompactSpace M] (hs : IsClosed s) (hU : xs, U x nhds x) :
                  ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), 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} [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) :
                  {i : ι | (fs.toFun i) x 0}.Finite
                  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)).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
                  • fs.ind x hx = .choose
                  Instances For
                    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 (fs.ind 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 (fs.ind 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 (fs.ind 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 (fs.ind x hx))).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 (fs.ind x hx))).source

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

                    Equations
                    • fs.fintype = .fintypeOfCompact
                    Instances For

                      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} [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 : MSet M} :
                        (f.toBumpCovering.IsSubordinate fun (i : ι) => U (f.c i)) f.IsSubordinate 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 : MSet M} :
                        f.IsSubordinate Uf.toBumpCovering.IsSubordinate fun (i : ι) => U (f.c i)

                        Alias of the reverse direction of SmoothBumpCovering.isSubordinate_toBumpCovering.

                        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} [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) :
                          (fs.toSmoothPartitionOfUnity i) x = (fs.toFun i) x * ∏ᶠ (j : ι) (_ : 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 0j t) :
                          (fs.toSmoothPartitionOfUnity i) x = (fs.toFun i) x * jFinset.filter (fun (j : ι) => WellOrderingRel j i) t, (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 ι), (fs.toSmoothPartitionOfUnity i) =ᶠ[nhds x] (fs.toFun i) * jFinset.filter (fun (j : ι) => WellOrderingRel j i) t, (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) :
                          (fs.toSmoothPartitionOfUnity 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 (fs.toSmoothPartitionOfUnity 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 : 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} [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) :
                          ∑ᶠ (i : ι), (fs.toSmoothPartitionOfUnity i) x = 1 - ∏ᶠ (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) (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} [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) :

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

                          Equations
                          Instances For
                            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), 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} [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), f.IsSubordinate fun (x : s) => (chartAt H x).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 : MSet F} {n : ℕ∞} (ht : ∀ (x : M), Convex (t x)) (Hloc : ∀ (x : M), Unhds x, ∃ (g : MF), ContMDiffOn I (modelWithCornersSelf F) n g U yU, 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 : MSet F} (ht : ∀ (x : M), Convex (t x)) (Hloc : ∀ (x : M), Unhds x, ∃ (g : MF), SmoothOn I (modelWithCornersSelf F) g U yU, 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 : MSet 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 : ι), 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} [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 : ι), 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.

                            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.