Measure-preserving isomorphisms modulo null sets

Mod0MeasureIso bundles two measurable maps between measured spaces which push the two measures forward onto one another and which are mutually inverse outside a null set. It is the modulo-null-set counterpart of MeasurePreserving, for the situation in which two spaces carry the same law only up to null sets, as happens when standard transport constructions are composed.

The packaging is adapted from Cameron Freer's independent implementation in Graphon/MeasureIso.lean at commit 9f7be59fa754d260a544b4cfd83d6a5b94f7552e: https://github.com/cameronfreer/graphon/commit/9f7be59fa754d260a544b4cfd83d6a5b94f7552e. The original work is copyright Cameron Freer and licensed under Apache 2.0.

Main results

• TauCeti.Mod0MeasureIso is the structure; TauCeti.Mod0MeasureIso.measurePreserving and TauCeti.Mod0MeasureIso.measurePreserving_invFun read off the two measure-preserving maps, TauCeti.Mod0MeasureIso.symm inverts an isomorphism, and TauCeti.Mod0MeasureIso.trans composes two of them;
• TauCeti.embeddingRealMod0MeasureIso transports a standard-Borel space into ℝ by embeddingReal;
• TauCeti.mod0MeasureIso_to_unitInterval turns a mod-zero isomorphism into ℝ carrying the unit interval measure into measure-preserving maps in both directions between that space and the unit interval.

The instance built from the cumulative distribution function and the quantile of an atomless real law is MeasureTheory.Measure.realMod0MeasureIso, in TauCeti.Probability.Quantile.

structure TauCeti.Mod0MeasureIso (α : Type u_1) (β : Type u_2) [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β) : Type (max u_1 u_2)

Two measurable maps that push μ and ν forward onto one another and that are mutually inverse outside a null set: a measure-preserving isomorphism of the two measured spaces modulo null sets.

• toFun : α → β

  The forward map, which pushes μ forward to ν.

• invFun : β → α

  The backward map, which pushes ν forward to μ.

• measurable_toFun : Measurable self.toFun
• measurable_invFun : Measurable self.invFun
• map_toFun : MeasureTheory.Measure.map self.toFun μ = ν
• map_invFun : MeasureTheory.Measure.map self.invFun ν = μ
• left_inv_ae : (fun (x : α) => self.invFun (self.toFun x)) =ᵐ[μ] id
• right_inv_ae : (fun (y : β) => self.toFun (self.invFun y)) =ᵐ[ν] id

theorem TauCeti.Mod0MeasureIso.measurePreserving {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : Mod0MeasureIso α β μ ν) : MeasureTheory.MeasurePreserving e.toFun μ ν

The forward map of a mod-zero isomorphism preserves the measure.

theorem TauCeti.Mod0MeasureIso.measurePreserving_invFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : Mod0MeasureIso α β μ ν) : MeasureTheory.MeasurePreserving e.invFun ν μ

The backward map of a mod-zero isomorphism preserves the measure.

def TauCeti.Mod0MeasureIso.symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : Mod0MeasureIso α β μ ν) : Mod0MeasureIso β α ν μ

The inverse of a mod-zero isomorphism is a mod-zero isomorphism between the reversed spaces, with the two maps interchanged.

Equations

• e.symm = { toFun := e.invFun, invFun := e.toFun, measurable_toFun := ⋯, measurable_invFun := ⋯, map_toFun := ⋯, map_invFun := ⋯, left_inv_ae := ⋯, right_inv_ae := ⋯ }

@[simp]

theorem TauCeti.Mod0MeasureIso.symm_toFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : Mod0MeasureIso α β μ ν) : e.symm.toFun = e.invFun

@[simp]

theorem TauCeti.Mod0MeasureIso.symm_invFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (e : Mod0MeasureIso α β μ ν) : e.symm.invFun = e.toFun

def TauCeti.Mod0MeasureIso.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {ξ : MeasureTheory.Measure γ} (e : Mod0MeasureIso α β μ ν) (f : Mod0MeasureIso β γ ν ξ) : Mod0MeasureIso α γ μ ξ

The composition of two mod-zero isomorphisms is again a mod-zero isomorphism.

Equations

• e.trans f = { toFun := f.toFun ∘ e.toFun, invFun := e.invFun ∘ f.invFun, measurable_toFun := ⋯, measurable_invFun := ⋯, map_toFun := ⋯, map_invFun := ⋯, left_inv_ae := ⋯, right_inv_ae := ⋯ }

@[simp]

theorem TauCeti.Mod0MeasureIso.trans_toFun {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {ξ : MeasureTheory.Measure γ} (e : Mod0MeasureIso α β μ ν) (f : Mod0MeasureIso β γ ν ξ) : (e.trans f).toFun = f.toFun ∘ e.toFun

@[simp]

theorem TauCeti.Mod0MeasureIso.trans_invFun {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {ξ : MeasureTheory.Measure γ} (e : Mod0MeasureIso α β μ ν) (f : Mod0MeasureIso β γ ν ξ) : (e.trans f).invFun = e.invFun ∘ f.invFun

noncomputable def TauCeti.embeddingRealMod0MeasureIso (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] (μ : MeasureTheory.Measure α) [Nonempty α] : Mod0MeasureIso α ℝ μ (MeasureTheory.Measure.map (MeasureTheory.embeddingReal α) μ)

Transporting a standard-Borel space into ℝ by embeddingReal is a mod-zero isomorphism onto the pushforward of the measure.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.embeddingRealMod0MeasureIso_toFun (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] (μ : MeasureTheory.Measure α) [Nonempty α] : (embeddingRealMod0MeasureIso α μ).toFun = MeasureTheory.embeddingReal α

@[simp]

theorem TauCeti.embeddingRealMod0MeasureIso_invFun (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] (μ : MeasureTheory.Measure α) [Nonempty α] : (embeddingRealMod0MeasureIso α μ).invFun = ⋯.invFun

theorem TauCeti.mod0MeasureIso_to_unitInterval {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (e : Mod0MeasureIso α ℝ μ (MeasureTheory.volume.restrict (Set.Icc 0 1))) : ∃ (f : α → ↑unitInterval) (g : ↑unitInterval → α), MeasureTheory.MeasurePreserving f μ MeasureTheory.volume ∧ MeasureTheory.MeasurePreserving g MeasureTheory.volume μ ∧ (∀ᵐ (x : α) ∂μ, g (f x) = x) ∧ ∀ᵐ (y : ↑unitInterval), f (g y) = y

A mod-zero isomorphism into ℝ carrying the unit interval measure gives measure-preserving maps in both directions between the space and the unit interval: the forward map clipped to the unit interval, and the backward map composed with the coercion. Since the forward map takes values in the unit interval outside a null set, the two maps are mutually inverse almost everywhere.