Continuous partition of unity #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define partition_of_unity (ι X : Type*) [topological_space X] (s : set X := univ)
to be a continuous partition of unity on s indexed by ι. More precisely, f : partition_of_unity ι X s is a collection of continuous functions f i : C(X, ℝ), i : ι, such that
- the supports of
f iform a locally finite family of sets; - each
f iis nonnegative; ∑ᶠ i, f i x = 1for allx ∈ s;∑ᶠ i, f i x ≤ 1for allx : X.
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,
bump_covering (ι X : Type*) [topological_space X] (s : set X := univ), to be a collection of
functions f i : C(X, ℝ), i : ι, such that
- the supports of
f iform a locally finite family of sets; - each
f iis nonnegative; - for each
x ∈ sthere existsi : ιsuch thatf i y = 1in a neighborhood ofx.
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
bump_covering.to_partition_of_unity. 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
bump_covering.exists_is_subordinate_of_locally_finite. 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 bump_covering.exists_is_subordinate.
We also provide two slightly more general versions of these lemmas,
bump_covering.exists_is_subordinate_of_locally_finite_of_prop and
bump_covering.exists_is_subordinate_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 well_ordering_rel j i instead of j < i in the definition of
bump_covering.to_partition_of_unity to avoid a [linear_order ι] assumption. While
well_ordering_rel 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
- to_fun : ι → C(X, ℝ)
- locally_finite' : locally_finite (λ (i : ι), function.support ⇑(self.to_fun i))
- nonneg' : 0 ≤ self.to_fun
- sum_eq_one' : ∀ (x : X), x ∈ s → finsum (λ (i : ι), ⇑(self.to_fun i) x) = 1
- sum_le_one' : ∀ (x : X), finsum (λ (i : ι), ⇑(self.to_fun i) x) ≤ 1
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 iform a locally finite family of sets, i.e., for every pointx : Xthere exists a neighborhoodU ∋ xsuch that all but finitely many functionsf iare zero onU; - the functions
f iare nonnegative; - the sum
∑ᶠ i, f i xis equal to one for everyx ∈ sand is less than or equal to one otherwise.
If X is a normal paracompact space, then partition_of_unity.exists_is_subordinate guarantees
that for every open covering U : set (set X) of s there exists a partition of unity that is
subordinate to U.
Instances for partition_of_unity
- partition_of_unity.has_sizeof_inst
- partition_of_unity.has_coe_to_fun
- partition_of_unity.inhabited
- to_fun : ι → C(X, ℝ)
- locally_finite' : locally_finite (λ (i : ι), function.support ⇑(self.to_fun i))
- nonneg' : 0 ≤ self.to_fun
- le_one' : self.to_fun ≤ 1
- eventually_eq_one' : ∀ (x : X), x ∈ s → (∃ (i : ι), ⇑(self.to_fun i) =ᶠ[nhds x] 1)
A bump_covering ι X s is an indexed family of functions f i, i : ι, such that
- the supports of
f iform a locally finite family of sets, i.e., for every pointx : Xthere exists a neighborhoodU ∋ xsuch that all but finitely many functionsf iare zero onU; - for all
i,xwe have0 ≤ f i x ≤ 1; - each point
x ∈ sbelongs to the interior of{x | f i x = 1}for somei.
One of the main use cases for a bump_covering is to define a partition_of_unity, see
bump_covering.to_partition_of_unity, but some proofs can directly use a bump_covering instead of
a partition_of_unity.
If X is a normal paracompact space, then bump_covering.exists_is_subordinate guarantees that for
every open covering U : set (set X) of s there exists a bump_covering of s that is
subordinate to U.
Instances for bump_covering
- bump_covering.has_sizeof_inst
- bump_covering.has_coe_to_fun
- bump_covering.inhabited
Equations
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.
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 λ x, f i x • g x is continuous on the whole space.
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
λ x, ∑ᶠ i, f i x • g i x is continuous on the whole space.
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.
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
λ x, ∑ᶠ i, f i x • g i x is a continuous function.
Equations
A bump_covering that consists of a single function, uniformly equal to one, defined as an
example for inhabited instance.
Equations
- bump_covering.single i s = {to_fun := pi.single i 1, locally_finite' := _, nonneg' := _, le_one' := _, eventually_eq_one' := _}
Equations
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.
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 bump_covering ι X s that is subordinate to U. If X is a
paracompact space, then the assumption hf : locally_finite U can be omitted, see
bump_covering.exists_is_subordinate. This version assumes that p : (X → ℝ) → Prop is a predicate
that satisfies Urysohn's lemma, and provides a bump_covering such that each function of the
covering satisfies p.
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 bump_covering ι X s that is subordinate to U. If X is a
paracompact space, then the assumption hf : locally_finite U can be omitted, see
bump_covering.exists_is_subordinate.
If X is a paracompact normal topological space and U is an open covering of a closed set
s, then there exists a bump_covering ι 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
bump_covering such that each function of the covering satisfies p.
If X is a paracompact normal topological space and U is an open covering of a closed set
s, then there exists a bump_covering ι X s that is subordinate to U.
Index of a bump function such that fs i =ᶠ[𝓝 x] 1.
Partition of unity defined by a bump_covering. We use this auxiliary definition to prove some
properties of the new family of functions before bundling it into a partition_of_unity. Do not use
this definition, use bump_function.to_partition_of_unity 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 linear_order ι, we use well_ordering_rel instead of (<).
The partition of unity defined by a bump_covering.
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 linear_order ι, we use well_ordering_rel instead of (<).
Equations
- f.to_partition_of_unity = {to_fun := λ (i : ι), {to_fun := f.to_pou_fun i, continuous_to_fun := _}, locally_finite' := _, nonneg' := _, sum_eq_one' := _, sum_le_one' := _}
If X is a normal topological space and U is a locally finite open covering of a closed set
s, then there exists a partition_of_unity ι X s that is subordinate to U. If X is a
paracompact space, then the assumption hf : locally_finite U can be omitted, see
bump_covering.exists_is_subordinate.
If X is a paracompact normal topological space and U is an open covering of a closed set
s, then there exists a partition_of_unity ι X s that is subordinate to U.