Documentation

Mathlib.Topology.PartitionOfUnity

Continuous partition of unity #

In this file we define PartitionOfUnity (ι X : Type*) [TopologicalSpace X] (s : Set X := univ) to be a continuous partition of unity on s indexed by ι. More precisely, f : PartitionOfUnity ι X s is a collection of continuous functions f i : C(X, ℝ), i : ι, such that

In the case s = univ the last assumption follows from the previous one but it is convenient to have this assumption in the case s ≠ univ.

We also define a bump function covering, BumpCovering (ι X : Type*) [TopologicalSpace X] (s : Set X := univ), to be a collection of functions f i : C(X, ℝ), i : ι, such that

The term is motivated by the smooth case.

If f is a bump function covering indexed by a linearly ordered type, then g i x = f i x * ∏ᶠ j < i, (1 - f j x) is a partition of unity, see BumpCovering.toPartitionOfUnity. Note that only finitely many terms 1 - f j x are not equal to one, so this product is well-defined.

Note that g i x = ∏ᶠ j ≤ i, (1 - f j x) - ∏ᶠ j < i, (1 - f j x), so most terms in the sum ∑ᶠ i, g i x cancel, and we get ∑ᶠ i, g i x = 1 - ∏ᶠ i, (1 - f i x), and the latter product equals zero because one of f i x is equal to one.

We say that a partition of unity or a bump function covering f is subordinate to a family of sets U i, i : ι, if the closure of the support of each f i is included in U i. We use Urysohn's Lemma to prove that a locally finite open covering of a normal topological space admits a subordinate bump function covering (hence, a subordinate partition of unity), see BumpCovering.exists_isSubordinate_of_locallyFinite. If X is a paracompact space, then any open covering admits a locally finite refinement, hence it admits a subordinate bump function covering and a subordinate partition of unity, see BumpCovering.exists_isSubordinate.

We also provide two slightly more general versions of these lemmas, BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop and BumpCovering.exists_isSubordinate_of_prop, to be used later in the construction of a smooth partition of unity.

Implementation notes #

Most (if not all) books only define a partition of unity of the whole space. However, quite a few proofs only deal with f i such that tsupport (f i) meets a specific closed subset, and it is easier to formalize these proofs if we don't have other functions right away.

We use WellOrderingRel j i instead of j < i in the definition of BumpCovering.toPartitionOfUnity to avoid a [LinearOrder ι] assumption. While WellOrderingRel j i is a well order, not only a strict linear order, we never use this property.

Tags #

partition of unity, bump function, Urysohn's lemma, normal space, paracompact space

structure PartitionOfUnity (ι : Type u_1) (X : Type u_2) [TopologicalSpace X] (s : optParam (Set X) Set.univ) :
Type (max u_1 u_2)

A continuous partition of unity on a set s : Set X is a collection of continuous functions f i such that

  • the supports of f i form a locally finite family of sets, i.e., for every point x : X there exists a neighborhood U ∋ x such that all but finitely many functions f i are zero on U;
  • the functions f i are nonnegative;
  • the sum ∑ᶠ i, f i x is equal to one for every x ∈ s and is less than or equal to one otherwise.

If X is a normal paracompact space, then PartitionOfUnity.exists_isSubordinate guarantees that for every open covering U : Set (Set X) of s there exists a partition of unity that is subordinate to U.

  • toFun : ιC(X, )

    The collection of continuous functions underlying this partition of unity

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

    the supports of the underlying functions are a locally finite family of sets

  • nonneg' : 0 self.toFun

    the functions are non-negative

  • sum_eq_one' : xs, ∑ᶠ (i : ι), (self.toFun i) x = 1

    the functions sum up to one on s

  • sum_le_one' : ∀ (x : X), ∑ᶠ (i : ι), (self.toFun i) x 1

    the functions sum up to at most one, globally

Instances For
    theorem PartitionOfUnity.locallyFinite' {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : PartitionOfUnity ι X s) :
    LocallyFinite fun (i : ι) => Function.support (self.toFun i)

    the supports of the underlying functions are a locally finite family of sets

    theorem PartitionOfUnity.nonneg' {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : PartitionOfUnity ι X s) :
    0 self.toFun

    the functions are non-negative

    theorem PartitionOfUnity.sum_eq_one' {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : PartitionOfUnity ι X s) (x : X) :
    x s∑ᶠ (i : ι), (self.toFun i) x = 1

    the functions sum up to one on s

    theorem PartitionOfUnity.sum_le_one' {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : PartitionOfUnity ι X s) (x : X) :
    ∑ᶠ (i : ι), (self.toFun i) x 1

    the functions sum up to at most one, globally

    structure BumpCovering (ι : Type u_1) (X : Type u_2) [TopologicalSpace X] (s : optParam (Set X) Set.univ) :
    Type (max u_1 u_2)

    A BumpCovering ι X s is an indexed family of functions f i, i : ι, such that

    • the supports of f i form a locally finite family of sets, i.e., for every point x : X there exists a neighborhood U ∋ x such that all but finitely many functions f i are zero on U;
    • for all i, x we have 0 ≤ f i x ≤ 1;
    • each point x ∈ s belongs to the interior of {x | f i x = 1} for some i.

    One of the main use cases for a BumpCovering is to define a PartitionOfUnity, see BumpCovering.toPartitionOfUnity, but some proofs can directly use a BumpCovering instead of a PartitionOfUnity.

    If X is a normal paracompact space, then BumpCovering.exists_isSubordinate guarantees that for every open covering U : Set (Set X) of s there exists a BumpCovering of s that is subordinate to U.

    • toFun : ιC(X, )

      The collections of continuous functions underlying this bump covering

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

      the supports of the underlying functions are a locally finite family of sets

    • nonneg' : 0 self.toFun

      the functions are non-negative

    • le_one' : self.toFun 1

      the functions are each at most one

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

      Each point x ∈ s belongs to the interior of {x | f i x = 1} for some i.

    Instances For
      theorem BumpCovering.locallyFinite' {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : BumpCovering ι X s) :
      LocallyFinite fun (i : ι) => Function.support (self.toFun i)

      the supports of the underlying functions are a locally finite family of sets

      theorem BumpCovering.nonneg' {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : BumpCovering ι X s) :
      0 self.toFun

      the functions are non-negative

      theorem BumpCovering.le_one' {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : BumpCovering ι X s) :
      self.toFun 1

      the functions are each at most one

      theorem BumpCovering.eventuallyEq_one' {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : BumpCovering ι X s) (x : X) :
      x s∃ (i : ι), (self.toFun i) =ᶠ[nhds x] 1

      Each point x ∈ s belongs to the interior of {x | f i x = 1} for some i.

      Equations
      • PartitionOfUnity.instFunLikeContinuousMapReal = { coe := PartitionOfUnity.toFun, coe_injective' := }
      theorem PartitionOfUnity.locallyFinite {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) :
      LocallyFinite fun (i : ι) => Function.support (f i)
      theorem PartitionOfUnity.locallyFinite_tsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) :
      LocallyFinite fun (i : ι) => tsupport (f i)
      theorem PartitionOfUnity.nonneg {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (i : ι) (x : X) :
      0 (f i) x
      theorem PartitionOfUnity.sum_eq_one {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) {x : X} (hx : x s) :
      ∑ᶠ (i : ι), (f i) x = 1
      theorem PartitionOfUnity.exists_pos {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) {x : X} (hx : x s) :
      ∃ (i : ι), 0 < (f i) x

      If f is a partition of unity on s, then for every x ∈ s there exists an index i such that 0 < f i x.

      theorem PartitionOfUnity.sum_le_one {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (x : X) :
      ∑ᶠ (i : ι), (f i) x 1
      theorem PartitionOfUnity.sum_nonneg {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (x : X) :
      0 ∑ᶠ (i : ι), (f i) x
      theorem PartitionOfUnity.le_one {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (i : ι) (x : X) :
      (f i) x 1
      def PartitionOfUnity.finsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) :

      The support of a 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₀ = .toFinset
      Instances For
        @[simp]
        theorem PartitionOfUnity.mem_finsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) {i : ι} :
        i ρ.finsupport x₀ i Function.support fun (i : ι) => (ρ i) x₀
        @[simp]
        theorem PartitionOfUnity.coe_finsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) :
        (ρ.finsupport x₀) = Function.support fun (i : ι) => (ρ i) x₀
        theorem PartitionOfUnity.sum_finsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) {x₀ : X} (hx₀ : x₀ s) :
        iρ.finsupport x₀, (ρ i) x₀ = 1
        theorem PartitionOfUnity.sum_finsupport' {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) {x₀ : X} (hx₀ : x₀ s) {I : Finset ι} (hI : ρ.finsupport x₀ I) :
        iI, (ρ i) x₀ = 1
        theorem PartitionOfUnity.sum_finsupport_smul_eq_finsum {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) {x₀ : X} {M : Type u_2} [AddCommGroup M] [Module M] (φ : ιXM) :
        iρ.finsupport x₀, (ρ i) x₀ φ i x₀ = ∑ᶠ (i : ι), (ρ i) x₀ φ i x₀
        theorem PartitionOfUnity.finite_tsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) :
        {i : ι | x₀ tsupport (ρ i)}.Finite

        The tsupports of a partition of unity are locally finite.

        def PartitionOfUnity.fintsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) :

        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 PartitionOfUnity.mem_fintsupport_iff {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) (i : ι) :
          i ρ.fintsupport x₀ x₀ tsupport (ρ i)
          theorem PartitionOfUnity.eventually_fintsupport_subset {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) :
          ∀ᶠ (y : X) in nhds x₀, ρ.fintsupport y ρ.fintsupport x₀
          theorem PartitionOfUnity.finsupport_subset_fintsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) :
          ρ.finsupport x₀ ρ.fintsupport x₀
          theorem PartitionOfUnity.eventually_finsupport_subset {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) :
          ∀ᶠ (y : X) in nhds x₀, ρ.finsupport y ρ.fintsupport x₀
          theorem PartitionOfUnity.continuous_smul {ι : Type u} {X : Type v} [TopologicalSpace X] {E : Type u_1} [AddCommMonoid E] [SMulWithZero E] [TopologicalSpace E] [ContinuousSMul E] {s : Set X} (f : PartitionOfUnity ι X s) {g : XE} {i : ι} (hg : xtsupport (f i), ContinuousAt g x) :
          Continuous fun (x : X) => (f i) x g x

          If f is a partition of unity on s : Set X and g : X → E is continuous at every point of the topological support of some f i, then fun x ↦ f i x • g x is continuous on the whole space.

          theorem PartitionOfUnity.continuous_finsum_smul {ι : Type u} {X : Type v} [TopologicalSpace X] {E : Type u_1} [AddCommMonoid E] [SMulWithZero E] [TopologicalSpace E] [ContinuousSMul E] {s : Set X} (f : PartitionOfUnity ι X s) [ContinuousAdd E] {g : ιXE} (hg : ∀ (i : ι), xtsupport (f i), ContinuousAt (g i) x) :
          Continuous fun (x : X) => ∑ᶠ (i : ι), (f i) x g i x

          If f is a partition of unity on a set s : Set X and g : ι → X → E is a family of functions such that each g i is continuous at every point of the topological support of f i, then the sum fun x ↦ ∑ᶠ i, f i x • g i x is continuous on the whole space.

          def PartitionOfUnity.IsSubordinate {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (U : ιSet X) :

          A 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
            theorem PartitionOfUnity.exists_finset_nhd' {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X) :
            ∃ (I : Finset ι), (∀ᶠ (x : X) in nhdsWithin x₀ s, iI, (ρ i) x = 1) ∀ᶠ (x : X) in nhds x₀, (Function.support fun (x_1 : ι) => (ρ x_1) x) I
            theorem PartitionOfUnity.exists_finset_nhd {ι : Type u} {X : Type v} [TopologicalSpace X] (ρ : PartitionOfUnity ι X) (x₀ : X) :
            ∃ (I : Finset ι), ∀ᶠ (x : X) in nhds x₀, iI, (ρ i) x = 1 (Function.support fun (x_1 : ι) => (ρ x_1) x) I
            theorem PartitionOfUnity.exists_finset_nhd_support_subset {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} {f : PartitionOfUnity ι X s} {U : ιSet X} (hso : f.IsSubordinate U) (ho : ∀ (i : ι), IsOpen (U i)) (x : X) :
            ∃ (is : Finset ι), nnhds x, n iis, U i zn, (Function.support fun (x : ι) => (f x) z) is
            theorem PartitionOfUnity.IsSubordinate.continuous_finsum_smul {ι : Type u} {X : Type v} [TopologicalSpace X] {E : Type u_1} [AddCommMonoid E] [SMulWithZero E] [TopologicalSpace E] [ContinuousSMul E] {s : Set X} {f : PartitionOfUnity ι X s} [ContinuousAdd E] {U : ιSet X} (ho : ∀ (i : ι), IsOpen (U i)) (hf : f.IsSubordinate U) {g : ιXE} (hg : ∀ (i : ι), ContinuousOn (g i) (U i)) :
            Continuous fun (x : X) => ∑ᶠ (i : ι), (f i) x g i x

            If f is a partition of unity that is subordinate to a family of open sets U i and g : ι → X → E is a family of functions such that each g i is continuous on U i, then the sum fun x ↦ ∑ᶠ i, f i x • g i x is a continuous function.

            Equations
            • BumpCovering.instFunLikeContinuousMapReal = { coe := BumpCovering.toFun, coe_injective' := }
            theorem BumpCovering.locallyFinite {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) :
            LocallyFinite fun (i : ι) => Function.support (f i)
            theorem BumpCovering.locallyFinite_tsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) :
            LocallyFinite fun (i : ι) => tsupport (f i)
            theorem BumpCovering.point_finite {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) :
            {i : ι | (f i) x 0}.Finite
            theorem BumpCovering.nonneg {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) :
            0 (f i) x
            theorem BumpCovering.le_one {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) :
            (f i) x 1
            def BumpCovering.single {ι : Type u} {X : Type v} [TopologicalSpace X] (i : ι) (s : Set X) :

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

            Equations
            Instances For
              @[simp]
              theorem BumpCovering.coe_single {ι : Type u} {X : Type v} [TopologicalSpace X] (i : ι) (s : Set X) :
              instance BumpCovering.instInhabited {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [Inhabited ι] :
              Equations
              def BumpCovering.IsSubordinate {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (U : ιSet X) :

              A collection of bump functions 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
                theorem BumpCovering.IsSubordinate.mono {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} {f : BumpCovering ι X s} {U : ιSet X} {V : ιSet X} (hU : f.IsSubordinate U) (hV : ∀ (i : ι), U i V i) :
                f.IsSubordinate V
                theorem BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] (p : (X)Prop) (h01 : ∀ (s t : Set X), IsClosed sIsClosed tDisjoint s t∃ (f : C(X, )), p f Set.EqOn (⇑f) 0 s Set.EqOn (⇑f) 1 t ∀ (x : X), f x Set.Icc 0 1) (hs : IsClosed s) (U : ιSet X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⋃ (i : ι), U i) :
                ∃ (f : BumpCovering ι X s), (∀ (i : ι), p (f i)) f.IsSubordinate U

                If X is a normal topological space and U i, i : ι, is a locally finite open covering of a closed set s, then there exists a BumpCovering ι X s that is subordinate to U. If X is a paracompact space, then the assumption hf : LocallyFinite U can be omitted, see BumpCovering.exists_isSubordinate. This version assumes that p : (X → ℝ) → Prop is a predicate that satisfies Urysohn's lemma, and provides a BumpCovering such that each function of the covering satisfies p.

                theorem BumpCovering.exists_isSubordinate_of_locallyFinite {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] (hs : IsClosed s) (U : ιSet X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⋃ (i : ι), U i) :
                ∃ (f : BumpCovering ι X s), f.IsSubordinate U

                If X is a normal topological space and U i, i : ι, is a locally finite open covering of a closed set s, then there exists a BumpCovering ι X s that is subordinate to U. If X is a paracompact space, then the assumption hf : LocallyFinite U can be omitted, see BumpCovering.exists_isSubordinate.

                theorem BumpCovering.exists_isSubordinate_of_prop {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X] (p : (X)Prop) (h01 : ∀ (s t : Set X), IsClosed sIsClosed tDisjoint s t∃ (f : C(X, )), p f Set.EqOn (⇑f) 0 s Set.EqOn (⇑f) 1 t ∀ (x : X), f x Set.Icc 0 1) (hs : IsClosed s) (U : ιSet X) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⋃ (i : ι), U i) :
                ∃ (f : BumpCovering ι X s), (∀ (i : ι), p (f i)) 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 BumpCovering ι X s that is subordinate to U. This version assumes that p : (X → ℝ) → Prop is a predicate that satisfies Urysohn's lemma, and provides a BumpCovering such that each function of the covering satisfies p.

                theorem BumpCovering.exists_isSubordinate {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X] (hs : IsClosed s) (U : ιSet X) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⋃ (i : ι), U i) :
                ∃ (f : BumpCovering ι X 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 BumpCovering ι X s that is subordinate to U.

                def BumpCovering.ind {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) (hx : x s) :
                ι

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

                Equations
                • f.ind x hx = .choose
                Instances For
                  theorem BumpCovering.eventuallyEq_one {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) (hx : x s) :
                  (f (f.ind x hx)) =ᶠ[nhds x] 1
                  theorem BumpCovering.ind_apply {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) (hx : x s) :
                  (f (f.ind x hx)) x = 1
                  def BumpCovering.toPOUFun {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) :

                  Partition of unity defined by a BumpCovering. We use this auxiliary definition to prove some properties of the new family of functions before bundling it into a PartitionOfUnity. Do not use this definition, use BumpCovering.toPartitionOfUnity instead.

                  The partition of unity is given by the formula g i x = f i x * ∏ᶠ j < i, (1 - f j x). In other words, g i x = ∏ᶠ j < i, (1 - f j x) - ∏ᶠ j ≤ i, (1 - f j x), so ∑ᶠ i, g i x = 1 - ∏ᶠ j, (1 - f j x). If x ∈ s, then one of f j x equals one, hence the product of 1 - f j x vanishes, and ∑ᶠ i, g i x = 1.

                  In order to avoid an assumption LinearOrder ι, we use WellOrderingRel instead of (<).

                  Equations
                  Instances For
                    theorem BumpCovering.toPOUFun_zero_of_zero {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) {i : ι} {x : X} (h : (f i) x = 0) :
                    f.toPOUFun i x = 0
                    theorem BumpCovering.support_toPOUFun_subset {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) :
                    Function.support (f.toPOUFun i) Function.support (f i)
                    theorem BumpCovering.toPOUFun_eq_mul_prod {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) (t : Finset ι) (ht : ∀ (j : ι), WellOrderingRel j i(f j) x 0j t) :
                    f.toPOUFun i x = (f i) x * jFinset.filter (fun (j : ι) => WellOrderingRel j i) t, (1 - (f j) x)
                    theorem BumpCovering.sum_toPOUFun_eq {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) :
                    ∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
                    theorem BumpCovering.exists_finset_toPOUFun_eventuallyEq {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) :
                    ∃ (t : Finset ι), f.toPOUFun i =ᶠ[nhds x] (f i) * (∏ jFinset.filter (fun (j : ι) => WellOrderingRel j i) t, (1 - f j))
                    theorem BumpCovering.continuous_toPOUFun {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) :
                    Continuous (f.toPOUFun i)
                    def BumpCovering.toPartitionOfUnity {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) :

                    The partition of unity defined by a BumpCovering.

                    The partition of unity is given by the formula g i x = f i x * ∏ᶠ j < i, (1 - f j x). In other words, g i x = ∏ᶠ j < i, (1 - f j x) - ∏ᶠ j ≤ i, (1 - f j x), so ∑ᶠ i, g i x = 1 - ∏ᶠ j, (1 - f j x). If x ∈ s, then one of f j x equals one, hence the product of 1 - f j x vanishes, and ∑ᶠ i, g i x = 1.

                    In order to avoid an assumption LinearOrder ι, we use WellOrderingRel instead of (<).

                    Equations
                    • f.toPartitionOfUnity = { toFun := fun (i : ι) => { toFun := f.toPOUFun i, continuous_toFun := }, locallyFinite' := , nonneg' := , sum_eq_one' := , sum_le_one' := }
                    Instances For
                      theorem BumpCovering.toPartitionOfUnity_apply {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) :
                      (f.toPartitionOfUnity i) x = (f i) x * ∏ᶠ (j : ι) (_ : WellOrderingRel j i), (1 - (f j) x)
                      theorem BumpCovering.toPartitionOfUnity_eq_mul_prod {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) (t : Finset ι) (ht : ∀ (j : ι), WellOrderingRel j i(f j) x 0j t) :
                      (f.toPartitionOfUnity i) x = (f i) x * jFinset.filter (fun (j : ι) => WellOrderingRel j i) t, (1 - (f j) x)
                      theorem BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) :
                      ∃ (t : Finset ι), (f.toPartitionOfUnity i) =ᶠ[nhds x] (f i) * (∏ jFinset.filter (fun (j : ι) => WellOrderingRel j i) t, (1 - f j))
                      theorem BumpCovering.toPartitionOfUnity_zero_of_zero {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) {i : ι} {x : X} (h : (f i) x = 0) :
                      (f.toPartitionOfUnity i) x = 0
                      theorem BumpCovering.support_toPartitionOfUnity_subset {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) :
                      Function.support (f.toPartitionOfUnity i) Function.support (f i)
                      theorem BumpCovering.sum_toPartitionOfUnity_eq {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) :
                      ∑ᶠ (i : ι), (f.toPartitionOfUnity i) x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
                      theorem BumpCovering.IsSubordinate.toPartitionOfUnity {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} {f : BumpCovering ι X s} {U : ιSet X} (h : f.IsSubordinate U) :
                      f.toPartitionOfUnity.IsSubordinate U
                      Equations
                      • PartitionOfUnity.instInhabited = { default := default.toPartitionOfUnity }
                      theorem PartitionOfUnity.exists_isSubordinate_of_locallyFinite {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] (hs : IsClosed s) (U : ιSet X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⋃ (i : ι), U i) :
                      ∃ (f : PartitionOfUnity ι X s), f.IsSubordinate U

                      If X is a normal topological space and U is a locally finite open covering of a closed set s, then there exists a PartitionOfUnity ι X s that is subordinate to U. If X is a paracompact space, then the assumption hf : LocallyFinite U can be omitted, see BumpCovering.exists_isSubordinate.

                      theorem PartitionOfUnity.exists_isSubordinate {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X] (hs : IsClosed s) (U : ιSet X) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⋃ (i : ι), U i) :
                      ∃ (f : PartitionOfUnity ι X 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 PartitionOfUnity ι X s that is subordinate to U.