Fibre-preserving maps of a product, and readouts that read the fibre only

Category: 1-Mathlib (CSD-free upstream candidate). BACKLOG #19-A; consumed by RecordLayer/BackReactionNecessity.lean.

A map Φ : B × F → B × F is fibre-preserving for a measure ν on F if it fixes the base coordinate and acts on the fibre over each base point by a ν-preserving map (FibrePreserving). A set S ⊆ B × F reads the fibre only if it is univ ×ˢ R.

The one theorem: under the Dirac-at-b preparation (dirac b).prod ν, the mass a fibre-preserving map sends into a fibre-only readout is ν R, whatever b is (FibrePreserving.measure_preimage_univ_prod). So the statistics of such a readout under such a dynamics cannot depend on the base point. A corollary says the same for Φ = id: a fibre-only set has base-independent Dirac-product measure (measure_dirac_prod_univ_prod).

References: Mathlib/MeasureTheory/Measure/Prod.lean (Measure.dirac_prod); specs/BACKLOG.md #19.

structure MeasureTheory.FibrePreserving {B : Type u_1} {F : Type u_2} [MeasurableSpace F] (Φ : B × F → B × F) (ν : Measure F) : Prop

Φ is fibre-preserving for ν: it fixes the base coordinate and acts on the fibre over each base point by a ν-preserving map.

• fst_eq (x : B × F) : (Φ x).1 = x.1

  The base coordinate is fixed.

• measurePreserving_snd (b : B) : MeasurePreserving (fun (y : F) => (Φ (b, y)).2) ν ν

  Over each base point the fibre map preserves ν.

theorem MeasureTheory.measure_dirac_prod_univ_prod {B : Type u_1} {F : Type u_2} [MeasurableSpace B] [MeasurableSpace F] (ν : Measure F) [SFinite ν] (b : B) {R : Set F} (hR : MeasurableSet R) : ((Measure.dirac b).prod ν) (Set.univ ×ˢ R) = ν R

A fibre-only set has base-independent measure under every Dirac-product preparation.

theorem MeasureTheory.FibrePreserving.measure_preimage_univ_prod {B : Type u_1} {F : Type u_2} [MeasurableSpace B] [MeasurableSpace F] {Φ : B × F → B × F} {ν : Measure F} [SFinite ν] (hΦ : FibrePreserving Φ ν) (hm : Measurable Φ) (b : B) {R : Set F} (hR : MeasurableSet R) : ((Measure.dirac b).prod ν) (Φ ⁻¹' Set.univ ×ˢ R) = ν R

★ A fibre-preserving map cannot make a fibre-only readout depend on the base point: under the preparation (dirac b).prod ν, the mass sent into univ ×ˢ R is ν R for every b.

theorem MeasureTheory.fibrePreserving_id {B : Type u_1} {F : Type u_2} [MeasurableSpace F] (ν : Measure F) : FibrePreserving id ν

The identity is fibre-preserving.

theorem MeasureTheory.fibrePreserving_of_measurePreserving {B : Type u_1} {F : Type u_2} [MeasurableSpace F] {φ : B → F → F} {ν : Measure F} (h : ∀ (b : B), MeasurePreserving (φ b) ν ν) : FibrePreserving (fun (x : B × F) => (x.1, φ x.1 x.2)) ν

A map that translates the fibre over each base point by a base-dependent amount is fibre-preserving whenever each translation preserves ν.