Boolean coordinates for a measurable function on a product

A measurable function f : α × β → γ into a nonempty standard Borel space depends on only countably many measurable sets of each factor, so it factors through a pair of maps into the Cantor space ℕ → Bool: there are measurable q : α → ℕ → Bool, r : β → ℕ → Bool and a measurable g : (ℕ → Bool) × (ℕ → Bool) → γ with f = g ∘ Prod.map q r (Measurable.exists_eq_measurable_comp_prodMap). When both factors are the same space one map suffices (Measurable.exists_eq_measurable_comp_prodMap_self), which is the form a symmetric kernel needs.

This is the measure-theoretic half of Janson's Lemma 7.3 for graphons, and the reason no hypothesis on α or β is needed anywhere: the two factors are replaced by a standard Borel model before any measure enters.

The argument has three steps. The σ-algebra pulled back along f is countably generated, because the target is; each of its countably many generators lies in the σ-algebra generated by countably many measurable rectangles (MeasurableSet.exists_countable_subset_generateFrom); and a map to the Cantor space makes all the countably many sides measurable in the pulled-back σ-algebra. Doob--Dynkin (Measurable.exists_eq_measurable_comp) then produces g.

Main results

• MeasurableSet.exists_countable_subset_generateFrom — a set measurable for a generated σ-algebra is already measurable for the σ-algebra generated by countably many of the generators;
• TauCeti.MeasureTheory.exists_measurable_generateFrom_le_comap — countably many measurable sets become measurable for the σ-algebra pulled back along one map to the Cantor space;
• Measurable.exists_eq_measurable_comp_prodMap — the factorization through Boolean coordinates of each factor;
• Measurable.exists_eq_measurable_comp_prodMap_self — its diagonal form, with a single coordinate map.

References

• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), Lemma 7.3.

theorem MeasurableSet.exists_countable_subset_generateFrom {α : Type u_1} {C : Set (Set α)} {s : Set α} (hs : MeasurableSet s) : ∃ D ⊆ C, D.Countable ∧ MeasurableSet s

A generated σ-algebra is exhausted by its countable subfamilies. A set measurable for generateFrom C is measurable for generateFrom D for some countable D ⊆ C: each of the three constructors of a generated σ-algebra consumes only countably many sets.

theorem TauCeti.MeasureTheory.exists_measurable_generateFrom_le_comap {α : Type u_1} [MeasurableSpace α] {C : Set (Set α)} (hC : C.Countable) (hmeas : ∀ s ∈ C, MeasurableSet s) : ∃ (q : α → ℕ → Bool), Measurable q ∧ MeasurableSpace.generateFrom C ≤ MeasurableSpace.comap q inferInstance

Countably many measurable sets become measurable through one map to the Cantor space. The σ-algebra a countable family of measurable sets generates is contained in the one pulled back along a measurable map to the Cantor space. Mathlib's MeasurableSpace.mapNatBool, applied to the generated σ-algebra, provides Boolean coordinates that generate enough measurable sets.

MeasurableSpace.measurable_mapNatBool gives the other inclusion, for the σ-algebra of the ambient space; here the family need not generate it.

theorem Measurable.exists_eq_measurable_comp_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [StandardBorelSpace γ] [Nonempty γ] {f : α × β → γ} (hf : Measurable f) : ∃ (q : α → ℕ → Bool) (r : β → ℕ → Bool) (g : (ℕ → Bool) × (ℕ → Bool) → γ), Measurable q ∧ Measurable r ∧ Measurable g ∧ f = g ∘ Prod.map q r

A measurable function on a product factors through Boolean coordinates. A measurable f : α × β → γ into a nonempty standard Borel space is a measurable function of countably many Boolean coordinates of each argument: no hypothesis on α or β is needed, which is what lets a kernel on an arbitrary carrier be transported to a standard Borel one.

theorem Measurable.exists_eq_measurable_comp_prodMap_self {α : Type u_1} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace γ] [StandardBorelSpace γ] [Nonempty γ] {f : α × α → γ} (hf : Measurable f) : ∃ (q : α → ℕ → Bool) (g : (ℕ → Bool) × (ℕ → Bool) → γ), Measurable q ∧ Measurable g ∧ f = g ∘ Prod.map q q

A measurable function on a square factors through one set of Boolean coordinates. For a nonempty standard Borel target, the diagonal form of Measurable.exists_eq_measurable_comp_prodMap uses a measurable equivalence to combine the two coordinate maps into one, which is what a symmetric function of two arguments needs.