mathlib documentation

topology.partition_of_unity

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

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 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

structure partition_of_unity (ι : Type u_1) (X : Type u_2) [topological_space X] (s : 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 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
structure bump_covering (ι : Type u_1) (X : Type u_2) [topological_space X] (s : set X := set.univ) :
Type (max u_1 u_2)

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 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 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
@[protected, instance]
def partition_of_unity.has_coe_to_fun {ι : Type u} {X : Type v} [topological_space X] {s : set X} :
has_coe_to_fun (partition_of_unity ι X s) (λ (_x : partition_of_unity ι X s), ι → C(X, ))
Equations
@[protected]
theorem partition_of_unity.locally_finite {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : partition_of_unity ι X s) :
theorem partition_of_unity.locally_finite_tsupport {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : partition_of_unity ι X s) :
locally_finite (λ (i : ι), tsupport (f i))
theorem partition_of_unity.nonneg {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : partition_of_unity ι X s) (i : ι) (x : X) :
0 (f i) x
theorem partition_of_unity.sum_eq_one {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : partition_of_unity ι X s) {x : X} (hx : x s) :
finsum (λ (i : ι), (f i) x) = 1
theorem partition_of_unity.exists_pos {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : partition_of_unity ι 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 partition_of_unity.sum_le_one {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : partition_of_unity ι X s) (x : X) :
finsum (λ (i : ι), (f i) x) 1
theorem partition_of_unity.sum_nonneg {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : partition_of_unity ι X s) (x : X) :
0 finsum (λ (i : ι), (f i) x)
theorem partition_of_unity.le_one {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : partition_of_unity ι X s) (i : ι) (x : X) :
(f i) x 1
theorem partition_of_unity.continuous_smul {ι : Type u} {X : Type v} [topological_space X] {E : Type u_1} [add_comm_monoid E] [smul_with_zero E] [topological_space E] [has_continuous_smul E] {s : set X} (f : partition_of_unity ι X s) {g : X → E} {i : ι} (hg : ∀ (x : X), x tsupport (f i)continuous_at g x) :
continuous (λ (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 λ x, f i x • g x is continuous on the whole space.

theorem partition_of_unity.continuous_finsum_smul {ι : Type u} {X : Type v} [topological_space X] {E : Type u_1} [add_comm_monoid E] [smul_with_zero E] [topological_space E] [has_continuous_smul E] {s : set X} (f : partition_of_unity ι X s) [has_continuous_add E] {g : ι → X → E} (hg : ∀ (i : ι) (x : X), x tsupport (f i)continuous_at (g i) x) :
continuous (λ (x : X), finsum (λ (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 λ x, ∑ᶠ i, f i x • g i x is continuous on the whole space.

def partition_of_unity.is_subordinate {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : partition_of_unity ι X s) (U : ι → set X) :
Prop

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
theorem partition_of_unity.exists_finset_nhd_support_subset {ι : Type u} {X : Type v} [topological_space X] {s : set X} {f : partition_of_unity ι X s} {U : ι → set X} (hso : f.is_subordinate U) (ho : ∀ (i : ι), is_open (U i)) (x : X) :
∃ (is : finset ι) {n : set X} (hn₁ : n nhds x) (hn₂ : n ⋂ (i : ι) (H : i is), U i), ∀ (z : X), z nfunction.support (λ (i : ι), (f i) z) is
theorem partition_of_unity.is_subordinate.continuous_finsum_smul {ι : Type u} {X : Type v} [topological_space X] {E : Type u_1} [add_comm_monoid E] [smul_with_zero E] [topological_space E] [has_continuous_smul E] {s : set X} {f : partition_of_unity ι X s} [has_continuous_add E] {U : ι → set X} (ho : ∀ (i : ι), is_open (U i)) (hf : f.is_subordinate U) {g : ι → X → E} (hg : ∀ (i : ι), continuous_on (g i) (U i)) :
continuous (λ (x : X), finsum (λ (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 λ x, ∑ᶠ i, f i x • g i x is a continuous function.

@[protected, instance]
def bump_covering.has_coe_to_fun {ι : Type u} {X : Type v} [topological_space X] {s : set X} :
has_coe_to_fun (bump_covering ι X s) (λ (_x : bump_covering ι X s), ι → C(X, ))
Equations
@[protected]
theorem bump_covering.locally_finite {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) :
theorem bump_covering.locally_finite_tsupport {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) :
locally_finite (λ (i : ι), tsupport (f i))
@[protected]
theorem bump_covering.point_finite {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (x : X) :
{i : ι | (f i) x 0}.finite
theorem bump_covering.nonneg {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (i : ι) (x : X) :
0 (f i) x
theorem bump_covering.le_one {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (i : ι) (x : X) :
(f i) x 1
@[protected]
noncomputable def bump_covering.single {ι : Type u} {X : Type v} [topological_space X] (i : ι) (s : set X) :

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

Equations
@[simp]
theorem bump_covering.coe_single {ι : Type u} {X : Type v} [topological_space X] (i : ι) (s : set X) :
@[protected, instance]
noncomputable def bump_covering.inhabited {ι : Type u} {X : Type v} [topological_space X] {s : set X} [inhabited ι] :
Equations
def bump_covering.is_subordinate {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (U : ι → set X) :
Prop

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
theorem bump_covering.is_subordinate.mono {ι : Type u} {X : Type v} [topological_space X] {s : set X} {f : bump_covering ι X s} {U V : ι → set X} (hU : f.is_subordinate U) (hV : ∀ (i : ι), U i V i) :
theorem bump_covering.exists_is_subordinate_of_locally_finite_of_prop {ι : Type u} {X : Type v} [topological_space X] {s : set X} [normal_space X] (p : (X → ) → Prop) (h01 : ∀ (s t : set X), is_closed sis_closed tdisjoint s t(∃ (f : C(X, )), p f set.eq_on f 0 s set.eq_on f 1 t ∀ (x : X), f x set.Icc 0 1)) (hs : is_closed s) (U : ι → set X) (ho : ∀ (i : ι), is_open (U i)) (hf : locally_finite U) (hU : s ⋃ (i : ι), U i) :
∃ (f : bump_covering ι X s), (∀ (i : ι), p (f i)) f.is_subordinate 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 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.

theorem bump_covering.exists_is_subordinate_of_locally_finite {ι : Type u} {X : Type v} [topological_space X] {s : set X} [normal_space X] (hs : is_closed s) (U : ι → set X) (ho : ∀ (i : ι), is_open (U i)) (hf : locally_finite U) (hU : s ⋃ (i : ι), U i) :
∃ (f : bump_covering ι X s), f.is_subordinate 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 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.

theorem bump_covering.exists_is_subordinate_of_prop {ι : Type u} {X : Type v} [topological_space X] {s : set X} [normal_space X] [paracompact_space X] (p : (X → ) → Prop) (h01 : ∀ (s t : set X), is_closed sis_closed tdisjoint s t(∃ (f : C(X, )), p f set.eq_on f 0 s set.eq_on f 1 t ∀ (x : X), f x set.Icc 0 1)) (hs : is_closed s) (U : ι → set X) (ho : ∀ (i : ι), is_open (U i)) (hU : s ⋃ (i : ι), U i) :
∃ (f : bump_covering ι X s), (∀ (i : ι), p (f i)) f.is_subordinate U

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.

theorem bump_covering.exists_is_subordinate {ι : Type u} {X : Type v} [topological_space X] {s : set X} [normal_space X] [paracompact_space X] (hs : is_closed s) (U : ι → set X) (ho : ∀ (i : ι), is_open (U i)) (hU : s ⋃ (i : ι), U i) :
∃ (f : bump_covering ι X s), f.is_subordinate U

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.

noncomputable def bump_covering.ind {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (x : X) (hx : x s) :
ι

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

Equations
theorem bump_covering.eventually_eq_one {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (x : X) (hx : x s) :
(f (f.ind x hx)) =ᶠ[nhds x] 1
theorem bump_covering.ind_apply {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (x : X) (hx : x s) :
(f (f.ind x hx)) x = 1
noncomputable def bump_covering.to_pou_fun {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (i : ι) (x : X) :

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 (<).

Equations
theorem bump_covering.to_pou_fun_zero_of_zero {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) {i : ι} {x : X} (h : (f i) x = 0) :
f.to_pou_fun i x = 0
theorem bump_covering.support_to_pou_fun_subset {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (i : ι) :
theorem bump_covering.to_pou_fun_eq_mul_prod {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (i : ι) (x : X) (t : finset ι) (ht : ∀ (j : ι), well_ordering_rel j i(f j) x 0j t) :
f.to_pou_fun i x = (f i) x * (finset.filter (λ (j : ι), well_ordering_rel j i) t).prod (λ (j : ι), 1 - (f j) x)
theorem bump_covering.sum_to_pou_fun_eq {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (x : X) :
finsum (λ (i : ι), f.to_pou_fun i x) = 1 - finprod (λ (i : ι), 1 - (f i) x)
theorem bump_covering.exists_finset_to_pou_fun_eventually_eq {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (i : ι) (x : X) :
∃ (t : finset ι), f.to_pou_fun i =ᶠ[nhds x] (f i) * (finset.filter (λ (j : ι), well_ordering_rel j i) t).prod (λ (j : ι), 1 - (f j))
theorem bump_covering.continuous_to_pou_fun {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (i : ι) :
noncomputable def bump_covering.to_partition_of_unity {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) :

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
theorem bump_covering.to_partition_of_unity_apply {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (i : ι) (x : X) :
((f.to_partition_of_unity) i) x = (f i) x * finprod (λ (j : ι), finprod (λ (hj : well_ordering_rel j i), 1 - (f j) x))
theorem bump_covering.to_partition_of_unity_eq_mul_prod {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (i : ι) (x : X) (t : finset ι) (ht : ∀ (j : ι), well_ordering_rel j i(f j) x 0j t) :
((f.to_partition_of_unity) i) x = (f i) x * (finset.filter (λ (j : ι), well_ordering_rel j i) t).prod (λ (j : ι), 1 - (f j) x)
theorem bump_covering.exists_finset_to_partition_of_unity_eventually_eq {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (i : ι) (x : X) :
∃ (t : finset ι), ((f.to_partition_of_unity) i) =ᶠ[nhds x] (f i) * (finset.filter (λ (j : ι), well_ordering_rel j i) t).prod (λ (j : ι), 1 - (f j))
theorem bump_covering.to_partition_of_unity_zero_of_zero {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) {i : ι} {x : X} (h : (f i) x = 0) :
theorem bump_covering.sum_to_partition_of_unity_eq {ι : Type u} {X : Type v} [topological_space X] {s : set X} (f : bump_covering ι X s) (x : X) :
finsum (λ (i : ι), ((f.to_partition_of_unity) i) x) = 1 - finprod (λ (i : ι), 1 - (f i) x)
theorem bump_covering.is_subordinate.to_partition_of_unity {ι : Type u} {X : Type v} [topological_space X] {s : set X} {f : bump_covering ι X s} {U : ι → set X} (h : f.is_subordinate U) :
@[protected, instance]
noncomputable def partition_of_unity.inhabited {ι : Type u} {X : Type v} [topological_space X] {s : set X} [inhabited ι] :
Equations
theorem partition_of_unity.exists_is_subordinate_of_locally_finite {ι : Type u} {X : Type v} [topological_space X] {s : set X} [normal_space X] (hs : is_closed s) (U : ι → set X) (ho : ∀ (i : ι), is_open (U i)) (hf : locally_finite U) (hU : s ⋃ (i : ι), U i) :
∃ (f : partition_of_unity ι X s), f.is_subordinate 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 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.

theorem partition_of_unity.exists_is_subordinate {ι : Type u} {X : Type v} [topological_space X] {s : set X} [normal_space X] [paracompact_space X] (hs : is_closed s) (U : ι → set X) (ho : ∀ (i : ι), is_open (U i)) (hU : s ⋃ (i : ι), U i) :
∃ (f : partition_of_unity ι X s), f.is_subordinate U

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.