Measurable discretization of pseudometric spaces

This file provides measurable maps onto finitely many points of a pseudometric space whose open sets are measurable: a nearest-point projection onto any nonempty finite set, a finite measurable approximation of a totally bounded space, and a measurable partition of a measurable totally bounded set into finitely many small cells. Such a partition of a compact set approximates a function continuous on a compact product uniformly by functions that are piecewise constant in the first variable.

Main statements

• TauCeti.exists_measurable_edist_eq_infEDist — a nonempty finite set carries a measurable nearest-point projection, sending every point to a point of the set at minimal distance.
• TauCeti.exists_measurable_dist_lt — a totally bounded pseudometric space admits a measurable map to a finite type whose indexed approximation point is uniformly close to every point.
• TotallyBounded.exists_measurable_dist_lt — a measurable totally bounded set is the union of finitely many measurable cells of small diameter, labelled by a measurable map that gives its complement a label of its own.
• TotallyBounded.exists_measurable_partition_ball — a measurable totally bounded set is the disjoint union of finitely many measurable pieces, each inside a small ball centred in the set.
• IsCompact.exists_enorm_sub_sum_indicator_le — a function continuous on a product of compact sets and zero outside it is uniformly close to a function that is piecewise constant in the first variable on a finite measurable partition, with values the slices at the centres.

theorem TauCeti.exists_measurable_edist_eq_infEDist {X : Type u} [PseudoEMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {s : Finset X} (hs : s.Nonempty) : ∃ (T : X → X), Measurable T ∧ (∀ (x : X), T x ∈ s) ∧ ∀ (x : X), edist x (T x) = Metric.infEDist x ↑s

A measurable nearest-point projection onto a finite set. In a pseudo-extended-metric space whose open sets are measurable, every nonempty finite set s is the target of a measurable map T that sends each point x to a point of s nearest to it: edist x (T x) = infEDist x s.

theorem TauCeti.exists_measurable_dist_lt (X : Type u) [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (hX : TotallyBounded Set.univ) {δ : ℝ} (hδ : 0 < δ) : ∃ (n : ℕ) (v : Fin n → X) (q : X → Fin n), Measurable q ∧ ∀ (x : X), dist x (v (q x)) < δ

A totally bounded pseudometric space admits, up to any positive error, an indexed finite family of approximation points and a measurable map assigning every point to a nearby one.

theorem TotallyBounded.exists_measurable_dist_lt {X : Type u} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {s : Set X} (hs : TotallyBounded s) (hsm : MeasurableSet s) {δ : ℝ} (hδ : 0 < δ) : ∃ (n : ℕ) (q : X → Fin (n + 1)), Measurable q ∧ (∀ (x : X), q x = Fin.last n ↔ x ∉ s) ∧ ∀ x ∈ s, ∀ y ∈ s, q x = q y → dist x y < δ

A measurable partition of a totally bounded set into small cells. In a pseudometric space whose open sets are measurable, a measurable totally bounded set s admits, for every δ > 0, a measurable map q : X → Fin (n + 1) that gives the complement of s the label Fin.last n and gives two points of s the same label only when they are at distance less than δ.

theorem TotallyBounded.exists_measurable_partition_ball {X : Type u} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {s : Set X} (hs : TotallyBounded s) (hsm : MeasurableSet s) {δ : ℝ} (hδ : 0 < δ) : ∃ (n : ℕ) (c : Fin n → X) (P : Fin n → Set X), (∀ (i : Fin n), c i ∈ s) ∧ (∀ (i : Fin n), MeasurableSet (P i)) ∧ (∀ (i : Fin n), P i ⊆ s ∩ Metric.ball (c i) δ) ∧ Pairwise (Function.onFun Disjoint P) ∧ ⋃ (i : Fin n), P i = s

A measurable partition of a totally bounded set into pieces of small balls. In a pseudometric space whose open sets are measurable, a measurable totally bounded set s is, for every δ > 0, the union of finitely many pairwise disjoint measurable pieces P i ⊆ s ∩ ball (c i) δ with centres c i ∈ s.

theorem IsCompact.exists_enorm_sub_sum_indicator_le {α : Type u_1} {β : Type u_2} {E : Type u_3} [MetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [PseudoMetricSpace β] [SeminormedAddCommGroup E] {K : α → β → E} {s : Set α} {t : Set β} (hs : IsCompact s) (ht : IsCompact t) (hKc : ContinuousOn (Function.uncurry K) (s ×ˢ t)) (hK0 : ∀ (x : α) (y : β), (x, y) ∉ s ×ˢ t → K x y = 0) {ε : NNReal} (hε : 0 < ε) : ∃ (n : ℕ) (c : Fin n → α) (P : Fin n → Set α), (∀ (i : Fin n), c i ∈ s) ∧ (∀ (i : Fin n), MeasurableSet (P i)) ∧ (∀ (i : Fin n), P i ⊆ s) ∧ Pairwise (Function.onFun Disjoint P) ∧ ∀ (x : α) (y : β), ‖K x y - ∑ i : Fin n, (P i).indicator (fun (x : α) => K (c i) y) x‖ₑ ≤ s.indicator (fun (x : α) => t.indicator (fun (x : β) => ↑ε) y) x

Uniform approximation by functions piecewise constant in the first variable. A function K continuous on a product s ×ˢ t of compact sets and zero outside it is within ε of a function that is piecewise constant in the first variable on a finite measurable partition of s, equal on the piece P i to the slice K (c i) at a point c i ∈ s: the difference is at most ε on s ×ˢ t and vanishes outside it.