Continuous partition of unity #
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 i
form a locally finite family of sets; - each
f i
is nonnegative; ∑ᶠ i, f i x = 1
for allx ∈ s
;∑ᶠ i, f i x ≤ 1
for 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 i
form a locally finite family of sets; - each
f i
is nonnegative; - for each
x ∈ s
there existsi : ι
such thatf i y = 1
in 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 i
form a locally finite family of sets, i.e., for every pointx : X
there exists a neighborhoodU ∋ x
such that all but finitely many functionsf i
are zero onU
; - the functions
f i
are nonnegative; - the sum
∑ᶠ i, f i x
is equal to one for everyx ∈ s
and 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 i
form a locally finite family of sets, i.e., for every pointx : X
there exists a neighborhoodU ∋ x
such that all but finitely many functionsf i
are zero onU
; - for all
i
,x
we have0 ≤ f i x ≤ 1
; - each point
x ∈ s
belongs 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
.