The σ-algebra of two coordinates is part of that of a set of coordinates #
Mathlib's Set.measurable_restrict says that restricting a function x : ∀ i, π i to the
coordinates in a set D is measurable. Phrased in terms of the σ-algebras the maps generate: the
information carried by D.domRestrict contains the information carried by any coordinate in D.
This file records the version for a pair of coordinates a, b ∈ D, read simultaneously as
(x a, x b), which is how a two-entry block of a random array is compared with the σ-algebra of a
larger set of entries.
Main result #
TauCeti.MeasureTheory.comap_pair_le_comap_domRestrict— fora, b ∈ D, the σ-algebra generated byx ↦ (x a, x b)is contained in the one generated byD.domRestrict.
theorem
TauCeti.MeasureTheory.comap_pair_le_comap_domRestrict
{ι : Type u_1}
{π : ι → Type u_2}
[(i : ι) → MeasurableSpace (π i)]
(D : Set ι)
{a b : ι}
(ha : a ∈ D)
(hb : b ∈ D)
:
MeasurableSpace.comap (fun (x : (i : ι) → π i) => (x a, x b)) inferInstance ≤ MeasurableSpace.comap D.domRestrict inferInstance
The information in two coordinates is part of the information in any set of coordinates
containing both: for a, b ∈ D, the σ-algebra generated by x ↦ (x a, x b) is contained in the
one generated by the restriction to D.