Finite-subset gaps of a partition of unity and their countable recolouring

Let ρ be a partition of unity with weights (ρ i)_{i ∈ ι}, where ι may be uncountable. For a finite set E of indices, the gap of E at x is ρ.gap E x = max 0 (min_{i ∈ E} ρ i x - sup_{i ∉ E} ρ i x), with the supremum of an empty family read as 0; the gap of ∅ is 0.

A positive gap at x means that E is a strict top segment of the weights at x: every weight in E is positive and strictly exceeds every weight outside E. Consequently the sets with a positive gap at a point form a chain, so at most one of them has any prescribed cardinality. Informally, if the positive weights at x are listed with multiplicity as a₁ ≥ ⋯ ≥ aₘ > 0 and aₘ₊₁ = 0, the set of the first n indices has gap aₙ - aₙ₊₁, and ties give gap zero. The basic identity is that the gaps of the sets containing a fixed index j add up to ρ j x; summing over j gives ∑ᶠ E, #E * ρ.gap E x = ∑ᶠ i, ρ i x.

Each gap is continuous: near any point only finitely many weights are nonzero, and there the gap is a finite expression in continuous functions. Grouping the gaps by cardinality, the functions n * ∑ᶠ_{#E = n} ρ.gap E form a partition of unity indexed by ℕ, on the same set as ρ. Thus any partition of unity, indexed by an arbitrary type, gives a countable one, and wherever the n-th new weight is positive it is carried by a single set E of size n all of whose original weights are positive. When ρ is subordinate to a cover U, this means that x ∈ U i for all i ∈ E.

This is the countable colouring used to build classifying maps of numerable bundles into Grassmannians of ℕ →₀ 𝕜: on the region where a set E of size n has positive gap, a chart of any index in E provides a local frame, and the n-th colour weights these frames. The positivity sets of the gaps are the open sets used in the proof of Lemma 5.9 of Milnor–Stasheff, Characteristic classes, to refine a locally finite trivializing cover to a countable one.

Main definitions and results

• PartitionOfUnity.gap: the gap of a finite set of indices.
• PartitionOfUnity.continuous_gap: each gap is continuous.
• PartitionOfUnity.gap_pos_iff: E has positive gap exactly when it is a nonempty strict top segment of positive weights.
• PartitionOfUnity.eq_of_gap_pos_of_card_eq: two sets of equal size with positive gaps at the same point coincide.
• PartitionOfUnity.finsum_mem_gap: the gaps of the sets containing j sum to ρ j x.
• PartitionOfUnity.finsum_card_mul_gap: ∑ᶠ E, #E * ρ.gap E x = ∑ᶠ i, ρ i x.
• PartitionOfUnity.gapPartition: the partition of unity indexed by ℕ grouping gaps by size.
• PartitionOfUnity.gapPartition_card_eq: where E has positive gap, the colour of size #E is #E * ρ.gap E x.

noncomputable def PartitionOfUnity.gap {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (E : Finset ι) (x : X) : ℝ

The gap of a finite set E of indices of a partition of unity at x: the excess of the smallest weight in E over the largest weight outside E, truncated below at 0. The supremum over an empty complement is 0, and the gap of ∅ is 0.

theorem PartitionOfUnity.gap_def {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (E : Finset ι) (x : X) : ρ.gap E x = max 0 ((⨅ (i : ↥E), (ρ ↑i) x) - ⨆ (i : { i : ι // i ∉ E }), (ρ ↑i) x)

The defining equation of PartitionOfUnity.gap.

theorem PartitionOfUnity.gap_nonneg {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (E : Finset ι) (x : X) : 0 ≤ ρ.gap E x

Gaps are nonnegative.

Elementary bounds on the infimum and the supremum

Positive gaps

theorem PartitionOfUnity.lt_of_gap_pos {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {E : Finset ι} {x : X} (h : 0 < ρ.gap E x) {i j : ι} (hi : i ∈ E) (hj : j ∉ E) : (ρ j) x < (ρ i) x

If E has positive gap at x, every weight in E strictly exceeds every weight outside E.

theorem PartitionOfUnity.pos_of_gap_pos {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {E : Finset ι} {x : X} (h : 0 < ρ.gap E x) {i : ι} (hi : i ∈ E) : 0 < (ρ i) x

If E has positive gap at x, every weight in E is positive at x.

theorem PartitionOfUnity.subset_finsupport_of_gap_pos {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {E : Finset ι} {x : X} (h : 0 < ρ.gap E x) : E ⊆ ρ.finsupport x

A set with positive gap at x consists of indices whose weights are nonzero at x.

theorem PartitionOfUnity.gap_pos_iff_ne_zero {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {E : Finset ι} {x : X} : 0 < ρ.gap E x ↔ ρ.gap E x ≠ 0

Gaps are nonnegative, so a gap is positive exactly when it is nonzero.

theorem PartitionOfUnity.mem_of_gap_pos_of_le {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {E : Finset ι} {x : X} (h : 0 < ρ.gap E x) {i j : ι} (hj : j ∈ E) (hji : (ρ j) x ≤ (ρ i) x) : i ∈ E

A set with positive gap at x contains every index whose weight at x is at least the weight of one of its members.

@[simp]

theorem PartitionOfUnity.gap_empty {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} (x : X) : ρ.gap ∅ x = 0

theorem PartitionOfUnity.gap_pos_iff {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {E : Finset ι} {x : X} : 0 < ρ.gap E x ↔ E.Nonempty ∧ (∀ i ∈ E, 0 < (ρ i) x) ∧ ∀ i ∈ E, ∀ j ∉ E, (ρ j) x < (ρ i) x

A finite set has positive gap at x exactly when it is nonempty, its weights at x are positive, and they strictly exceed every weight outside it.

theorem PartitionOfUnity.subset_or_subset_of_gap_pos {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {E F : Finset ι} {x : X} (hE : 0 < ρ.gap E x) (hF : 0 < ρ.gap F x) : E ⊆ F ∨ F ⊆ E

Sets with positive gaps at the same point are nested.

theorem PartitionOfUnity.eq_of_gap_pos_of_card_eq {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {E F : Finset ι} {x : X} (hE : 0 < ρ.gap E x) (hF : 0 < ρ.gap F x) (hcard : E.card = F.card) : E = F

At each point, at most one set of each cardinality has positive gap.

theorem PartitionOfUnity.IsSubordinate.mem_of_gap_pos {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {U : ι → Set X} (hU : ρ.IsSubordinate U) {E : Finset ι} {x : X} (h : 0 < ρ.gap E x) {i : ι} (hi : i ∈ E) : x ∈ U i

If ρ is subordinate to U and E has positive gap at x, then x lies in U i for every i ∈ E.

Continuity

theorem PartitionOfUnity.continuous_gap {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} (E : Finset ι) : Continuous (ρ.gap E)

Each gap of a partition of unity is continuous.

The gap identities

theorem PartitionOfUnity.finite_support_gap {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} (x : X) : (Function.support fun (x_1 : Finset ι) => ρ.gap x_1 x).Finite

At each point only finitely many sets have nonzero gap.

The identity finsum_mem_gap is proved on the finite support T of the weights at x, by strong induction on the number of weights in T strictly below ρ j x. If there are none, only T itself contributes. Otherwise, if k carries the largest weight below ρ j x, the sets containing j with positive gap are the up-set of j, with gap ρ j x - ρ k x, and the sets containing k with positive gap.

theorem PartitionOfUnity.finsum_mem_gap {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} (x : X) (j : ι) : ∑ᶠ (E : Finset ι) (_ : j ∈ E), ρ.gap E x = (ρ j) x

The gaps of the finite sets containing a fixed index j sum to the weight ρ j x.

theorem PartitionOfUnity.finsum_card_mul_gap {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} (x : X) : ∑ᶠ (E : Finset ι), ↑E.card * ρ.gap E x = ∑ᶠ (i : ι), (ρ i) x

Weighting each gap by the size of its set recovers the total weight.

theorem PartitionOfUnity.finsum_card_mul_gap_eq_one {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {x : X} (hx : x ∈ s) : ∑ᶠ (E : Finset ι), ↑E.card * ρ.gap E x = 1

On the set of a partition of unity, the size-weighted gaps sum to one.

The countable partition of unity

noncomputable def PartitionOfUnity.gapPartition {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} : PartitionOfUnity ℕ X s

The countable partition of unity obtained from a partition of unity ρ by grouping its gaps by cardinality: its n-th weight is n * ∑ᶠ_{#E = n} ρ.gap E. The 0-th weight vanishes. It is a partition of unity on the same set as ρ, whatever the cardinality of the index type of ρ. At each point at most one set of size n has positive gap (eq_of_gap_pos_of_card_eq), so where the n-th weight is positive it is carried by a single set; see gapPartition_card_eq.

theorem PartitionOfUnity.gapPartition_apply {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (n : ℕ) (x : X) : (gapPartition n) x = ↑n * ∑ᶠ (E : Finset ι) (_ : E.card = n), ρ.gap E x

@[simp]

theorem PartitionOfUnity.gapPartition_zero {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} (x : X) : (gapPartition 0) x = 0

theorem PartitionOfUnity.gapPartition_card_eq {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {E : Finset ι} {x : X} (h : 0 < ρ.gap E x) : (gapPartition E.card) x = ↑E.card * ρ.gap E x

Where a set E has positive gap, the weight of gapPartition indexed by its size is carried by E alone.

theorem PartitionOfUnity.exists_gap_pos_of_gapPartition_pos {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {ρ : PartitionOfUnity ι X s} {n : ℕ} {x : X} (h : 0 < (gapPartition n) x) : ∃ (E : Finset ι), E.card = n ∧ 0 < ρ.gap E x

A positive weight of gapPartition at x is carried by a set of indices of that size with positive gap at x.