Switching between two maps with the same image law

Let f and g be almost-everywhere measurable maps with the same image law, μ.map f = μ.map g, and let t be a measurable set that f and g enter on the same points almost everywhere. Following f on the preimage of that set and g off it gives a map with the same image law again.

The typical use is with randomized codings: if two codings q ↦ (q.1, f q) and q ↦ (q.1, g q) of the same joint law keep the first coordinate, one may switch between them along any measurable event of the first coordinate.

Main results

• TauCeti.MeasureTheory.Measure.map_ite_mem_eq — switching between two maps with the same image law along an almost-everywhere common preimage of a measurable set does not change the image law.

theorem TauCeti.MeasureTheory.Measure.map_ite_mem_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f g : α → β} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) {t : Set β} [DecidablePred fun (x : β) => x ∈ t] (ht : MeasurableSet t) (hfgt : ∀ᵐ (a : α) ∂μ, f a ∈ t ↔ g a ∈ t) (hfg : MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g μ) : MeasureTheory.Measure.map (fun (a : α) => if f a ∈ t then f a else g a) μ = MeasureTheory.Measure.map f μ

Switching between two maps with the same image law. If f and g are μ-a.e. measurable with μ.map f = μ.map g, and enter the measurable set t on the same points μ-almost everywhere, then the map that follows f when the image lies in t and g otherwise has the same image law.