Normalizing locally finite positive families and shrinking supports of partitions of unity

A locally finite family of nonnegative continuous functions (f i)_{i ∈ ι} on a topological space X that is positive at each point normalizes to a partition of unity PartitionOfUnity.ofExistsPos with weights f i x / ∑ᶠ j, f j x and the same open and closed supports as f.

Applying this normalization to the truncated weights max 0 (ρ i x - (⨆ j, ρ j x) / 2) of any partition of unity ρ : PartitionOfUnity ι X yields a shrunken partition of unity ρ.shrink whose closed supports lie inside the open supports of ρ: tsupport (ρ.shrink i) ⊆ support (ρ i). In particular, if every open support support (ρ i) lies in U i, then ρ.shrink is subordinate to U in the closed-support sense (PartitionOfUnity.IsSubordinate). Neither separation nor normality of X, nor openness of the sets U i, is used.

Main definitions and results

• PartitionOfUnity.ofExistsPos: normalize a locally finite nonnegative family positive at every point into a partition of unity.
• PartitionOfUnity.shrink: shrink the closed supports of a partition of unity on X inside its open supports, with weights given by PartitionOfUnity.shrink_apply.
• PartitionOfUnity.shrink_pos_iff and PartitionOfUnity.support_shrink: ρ.shrink i is positive (equivalently, supported) at x precisely when (⨆ j, ρ j x) / 2 < ρ i x.
• PartitionOfUnity.tsupport_shrink_subset_support: tsupport (ρ.shrink i) ⊆ support (ρ i).
• PartitionOfUnity.isSubordinate_shrink: open-support subordination ∀ i, support (ρ i) ⊆ U i upgrades to ρ.shrink.IsSubordinate U.

References

• A. Dold, Partitions of unity in the theory of fibrations, Ann. of Math. (2) 78 (1963), 223–255, §2.

noncomputable def PartitionOfUnity.ofExistsPos {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (f : ι → C(X, ℝ)) (hlf : LocallyFinite fun (i : ι) => Function.support ⇑(f i)) (hnn : ∀ (i : ι) (x : X), 0 ≤ (f i) x) (hpos : ∀ (x : X), ∃ (i : ι), 0 < (f i) x) : PartitionOfUnity ι X

Normalize a locally finite family of nonnegative continuous functions that is positive at every point into a partition of unity on X.

@[simp]

theorem PartitionOfUnity.ofExistsPos_apply {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (f : ι → C(X, ℝ)) (hlf : LocallyFinite fun (i : ι) => Function.support ⇑(f i)) (hnn : ∀ (i : ι) (x : X), 0 ≤ (f i) x) (hpos : ∀ (x : X), ∃ (i : ι), 0 < (f i) x) (i : ι) (x : X) : ((ofExistsPos f hlf hnn hpos) i) x = (f i) x / ∑ᶠ (j : ι), (f j) x

Each weight of PartitionOfUnity.ofExistsPos is f i x divided by the finite sum ∑ᶠ j, f j x.

theorem PartitionOfUnity.ofExistsPos_pos_iff {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (f : ι → C(X, ℝ)) (hlf : LocallyFinite fun (i : ι) => Function.support ⇑(f i)) (hnn : ∀ (i : ι) (x : X), 0 ≤ (f i) x) (hpos : ∀ (x : X), ∃ (i : ι), 0 < (f i) x) (i : ι) (x : X) : 0 < ((ofExistsPos f hlf hnn hpos) i) x ↔ 0 < (f i) x

A normalized weight of PartitionOfUnity.ofExistsPos is positive if and only if the original weight is positive.

@[simp]

theorem PartitionOfUnity.support_ofExistsPos {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (f : ι → C(X, ℝ)) (hlf : LocallyFinite fun (i : ι) => Function.support ⇑(f i)) (hnn : ∀ (i : ι) (x : X), 0 ≤ (f i) x) (hpos : ∀ (x : X), ∃ (i : ι), 0 < (f i) x) (i : ι) : Function.support ⇑((ofExistsPos f hlf hnn hpos) i) = Function.support ⇑(f i)

Normalization via PartitionOfUnity.ofExistsPos preserves open supports.

@[simp]

theorem PartitionOfUnity.tsupport_ofExistsPos {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (f : ι → C(X, ℝ)) (hlf : LocallyFinite fun (i : ι) => Function.support ⇑(f i)) (hnn : ∀ (i : ι) (x : X), 0 ≤ (f i) x) (hpos : ∀ (x : X), ∃ (i : ι), 0 < (f i) x) (i : ι) : tsupport ⇑((ofExistsPos f hlf hnn hpos) i) = tsupport ⇑(f i)

Normalization via PartitionOfUnity.ofExistsPos preserves closed supports.

noncomputable def PartitionOfUnity.shrink {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (ρ : PartitionOfUnity ι X) : PartitionOfUnity ι X

Shrink a partition of unity ρ on X by truncating each weight below half of the pointwise maximum weight and renormalizing, so that every closed support lies in the corresponding open support of ρ.

theorem PartitionOfUnity.shrink_apply {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (ρ : PartitionOfUnity ι X) (i : ι) (x : X) : (ρ.shrink i) x = max 0 ((ρ i) x - (⨆ (j : ι), (ρ j) x) / 2) / ∑ᶠ (k : ι), max 0 ((ρ k) x - (⨆ (j : ι), (ρ j) x) / 2)

Each weight of ρ.shrink is the truncated excess max 0 (ρ i x - (⨆ j, ρ j x) / 2) divided by the finite sum of those truncated excesses.

theorem PartitionOfUnity.shrink_pos_iff {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {ρ : PartitionOfUnity ι X} {i : ι} {x : X} : 0 < (ρ.shrink i) x ↔ (⨆ (j : ι), (ρ j) x) / 2 < (ρ i) x

A shrunken weight ρ.shrink i x is positive if and only if ρ i x strictly exceeds half of the pointwise supremum ⨆ j, ρ j x.

theorem PartitionOfUnity.support_shrink {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (ρ : PartitionOfUnity ι X) (i : ι) : Function.support ⇑(ρ.shrink i) = {x : X | (⨆ (j : ι), (ρ j) x) / 2 < (ρ i) x}

The open support of ρ.shrink i is the set of points where ρ i strictly exceeds half of the pointwise supremum ⨆ j, ρ j x.

theorem PartitionOfUnity.support_shrink_subset {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (ρ : PartitionOfUnity ι X) (i : ι) : Function.support ⇑(ρ.shrink i) ⊆ Function.support ⇑(ρ i)

Every open support of ρ.shrink is contained in the open support of ρ.

theorem PartitionOfUnity.tsupport_shrink_subset_support {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] (ρ : PartitionOfUnity ι X) (i : ι) : tsupport ⇑(ρ.shrink i) ⊆ Function.support ⇑(ρ i)

Every closed support of ρ.shrink is contained in the open support of ρ.

theorem PartitionOfUnity.isSubordinate_shrink {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {ρ : PartitionOfUnity ι X} {U : ι → Set X} (hU : ∀ (i : ι), Function.support ⇑(ρ i) ⊆ U i) : ρ.shrink.IsSubordinate U

If every open support support (ρ i) lies in U i, then ρ.shrink is subordinate to U in the closed-support sense.