Gluing measure-preserving pieces along a finite partition

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #137; consumed by RecordLayer/SkewReroute.lean.

A map defined piecewise — f i on the i-th cell P i of a finite exact partition — is measure-preserving as soon as each piece pushes μ.restrict (P i) onto μ.restrict (Q i) for a second exact partition Q. This is the "cut and move the pieces" principle behind interval and rectangle exchanges: the preimage of a set splits along P, each part is computed by the piece's transport law, and the parts reassemble along Q.

• glueIdx hP x — the cell of x; glue hP f x = f (glueIdx hP x) x;
• glue_eq_of_mem — on P i the glued map is f i;
• preimage_glue — glue⁻¹ S = ⋃ i, f i ⁻¹' S ∩ P i;
• ★★ measurePreserving_glue — the gluing theorem.

Honest scope

The partitions are exact (every point in exactly one cell), not almost-everywhere: the consumers have exact tilings, and the exact form keeps the pointwise statement glue_eq_of_mem available for readout invariance, which an a.e. version would not give.

References: specs/BACKLOG.md #137.

noncomputable def MeasureTheory.glueIdx {α : Type u_1} {ι : Type u_2} {P : ι → Set α} (hP : ∀ (x : α), ∃! i : ι, x ∈ P i) (x : α) : ι

The cell of an exact partition that contains x.

Equations

• MeasureTheory.glueIdx hP x = ⋯.choose

theorem MeasureTheory.mem_glueIdx {α : Type u_1} {ι : Type u_2} {P : ι → Set α} (hP : ∀ (x : α), ∃! i : ι, x ∈ P i) (x : α) : x ∈ P (glueIdx hP x)

theorem MeasureTheory.glueIdx_eq {α : Type u_1} {ι : Type u_2} {P : ι → Set α} (hP : ∀ (x : α), ∃! i : ι, x ∈ P i) {x : α} {i : ι} (hx : x ∈ P i) : glueIdx hP x = i

noncomputable def MeasureTheory.glue {α : Type u_1} {ι : Type u_2} {P : ι → Set α} (hP : ∀ (x : α), ∃! i : ι, x ∈ P i) (f : ι → α → α) (x : α) : α

The glued map: f i on the cell P i.

Equations

• MeasureTheory.glue hP f x = f (MeasureTheory.glueIdx hP x) x

theorem MeasureTheory.glue_eq_of_mem {α : Type u_1} {ι : Type u_2} {P : ι → Set α} (hP : ∀ (x : α), ∃! i : ι, x ∈ P i) (f : ι → α → α) {x : α} {i : ι} (hx : x ∈ P i) : glue hP f x = f i x

theorem MeasureTheory.pairwise_disjoint_of_existsUnique {α : Type u_1} {ι : Type u_2} {P : ι → Set α} (hP : ∀ (x : α), ∃! i : ι, x ∈ P i) : Pairwise (Function.onFun Disjoint P)

Cells of an exact partition are pairwise disjoint.

theorem MeasureTheory.preimage_glue {α : Type u_1} {ι : Type u_2} {P : ι → Set α} (hP : ∀ (x : α), ∃! i : ι, x ∈ P i) (f : ι → α → α) (S : Set α) : glue hP f ⁻¹' S = ⋃ (i : ι), f i ⁻¹' S ∩ P i

The preimage of a set under the glued map splits along the partition.

theorem MeasureTheory.measurable_glue {α : Type u_1} {ι : Type u_2} {P : ι → Set α} [MeasurableSpace α] [Fintype ι] (hP : ∀ (x : α), ∃! i : ι, x ∈ P i) (hPm : ∀ (i : ι), MeasurableSet (P i)) {f : ι → α → α} (hf : ∀ (i : ι), Measurable (f i)) : Measurable (glue hP f)

The glued map is measurable when the pieces and the cells are.

theorem MeasureTheory.measurePreserving_glue {α : Type u_1} {ι : Type u_2} {P : ι → Set α} [MeasurableSpace α] [Fintype ι] (μ : Measure α) (hP : ∀ (x : α), ∃! i : ι, x ∈ P i) (hPm : ∀ (i : ι), MeasurableSet (P i)) {Q : ι → Set α} (hQ : ∀ (y : α), ∃! i : ι, y ∈ Q i) (hQm : ∀ (i : ι), MeasurableSet (Q i)) {f : ι → α → α} (hf : ∀ (i : ι), Measurable (f i)) (hmap : ∀ (i : ι), Measure.map (f i) (μ.restrict (P i)) = μ.restrict (Q i)) : MeasurePreserving (glue hP f) μ μ

★★ The gluing theorem. If each piece f i pushes μ.restrict (P i) onto μ.restrict (Q i), for exact partitions P and Q, the glued map preserves μ.