Piecewise measure-preserving maps, and coordinate swaps with a pi factor

Category: 1-Mathlib (CSD-free upstream candidates).

Three reusable measure lemmas the record layer's swap witness needs, stated with no CSD content:

• measurePreserving_of_partition — a map agreeing on each piece of a countable measurable partition with a measure-preserving map that fixes that piece (as a preimage) is itself measure-preserving. The natural tool for piecewise-defined dynamics such as record-triggered interactions.
• Measure.map_eval_pi' — the pushforward of a finite product of probability measures under a coordinate evaluation is that coordinate's measure.
• measurePreserving_swapSlot — exchanging an external factor with one coordinate of a pi factor (all factors carrying the same measure) preserves the product measure. The map (s, a) ↦ (a j, update a j s) is an involutive measurable map of α × (ι → α), proved measure-preserving by conjugating through piEquivPiSubtypeProd (· = j): the pi factor splits as (slot j) × (the rest) and the swap becomes Prod.swap on the first two factors.

Provenance

Staged as upstream Mathlib material; no CsdLean4-namespace content.

theorem MeasureTheory.measurable_of_partition {X : Type u_1} [MeasurableSpace X] {ι : Type u_2} [Countable ι] {A : ι → Set X} (hAmeas : ∀ (k : ι), MeasurableSet (A k)) (hAcover : ⋃ (k : ι), A k = Set.univ) {T : X → X} {Tk : ι → X → X} (hTk : ∀ (k : ι), Measurable (Tk k)) (hagree : ∀ (k : ι), ∀ x ∈ A k, T x = Tk k x) : Measurable T

A map defined piecewise on a countable measurable partition is measurable, when each piece's map is. Companion to measurePreserving_of_partition.

theorem MeasureTheory.measurePreserving_of_partition {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {ι : Type u_2} [Countable ι] {A : ι → Set X} (hAmeas : ∀ (k : ι), MeasurableSet (A k)) (hAdisj : Pairwise (Function.onFun Disjoint A)) (hAcover : ⋃ (k : ι), A k = Set.univ) {T : X → X} (hTmeas : Measurable T) {Tk : ι → X → X} (hTk : ∀ (k : ι), MeasurePreserving (Tk k) μ μ) (hagree : ∀ (k : ι), ∀ x ∈ A k, T x = Tk k x) (hfix : ∀ (k : ι), Tk k ⁻¹' A k = A k) : MeasurePreserving T μ μ

A piecewise measure-preserving map is measure-preserving. If {A k} is a countable measurable partition, each T k preserves μ and fixes its own piece as a preimage (T k ⁻¹' A k = A k), and T agrees with T k on A k, then T preserves μ.

theorem MeasureTheory.Measure.map_eval_pi' {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), IsProbabilityMeasure (μ i)] (i : ι) : map (Function.eval i) (Measure.pi μ) = μ i

Evaluation pushes a finite product of probability measures to its factor.

def MeasureTheory.swapSlot {α : Type u_1} {ι : Type u_2} [DecidableEq ι] (j : ι) : α × (ι → α) → α × (ι → α)

The slot-swap map (s, a) ↦ (a j, update a j s) on α × (ι → α). An involution.

Equations

• MeasureTheory.swapSlot j x = (x.2 j, Function.update x.2 j x.1)

theorem MeasureTheory.swapSlot_involutive {α : Type u_1} {ι : Type u_2} [DecidableEq ι] (j : ι) : Function.Involutive (swapSlot j)

theorem MeasureTheory.measurable_swapSlot {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [DecidableEq ι] (j : ι) : Measurable (swapSlot j)

theorem MeasureTheory.Fin.insertNth_removeNth_eq_update {n : ℕ} {α : Type u_1} (j : Fin (n + 1)) (a : Fin (n + 1) → α) (s : α) : (j.insertNth s fun (k : Fin n) => a (j.succAbove k)) = Function.update a j s

Inserting a value back into its removed slot is Function.update.

theorem MeasureTheory.measurePreserving_swapSlot {α : Type u_1} [MeasurableSpace α] {K : ℕ} (μ : Measure α) [IsProbabilityMeasure μ] (j : Fin K) : MeasurePreserving (swapSlot j) (μ.prod (Measure.pi fun (x : Fin K) => μ)) (μ.prod (Measure.pi fun (x : Fin K) => μ))

Swapping an external factor with one pi coordinate preserves the product measure, when every factor carries the same measure. Stated for Fin K (the record layer's index type); proved by splitting the pi factor at the slot with piFinSuccAbove, under which the swap becomes Prod.swap on the first two factors.