This module contains various functions to and from standard borel spaces.

noncomputable def MeasureTheory.pack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] : A → ℝ

Packs a natural number and a real number into a single real number.

Equations

• MeasureTheory.pack = if h : Countable A then MeasureTheory.embeddingReal A else ⇑(PolishSpace.measurableEquivOfNotCountable h ⋯)

noncomputable def MeasureTheory.unpack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] : ℝ → A

Unpacks a natural number and a real number from a single real number.

Equations

• MeasureTheory.unpack = if h : Countable A then ⋯.invFun else ⇑(PolishSpace.measurableEquivOfNotCountable h ⋯).symm

@[simp]

theorem MeasureTheory.unpack_pack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] (x : A) : unpack (pack x) = x

@[simp]

theorem MeasureTheory.pack_unpack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] (h : ¬Countable A) (x : ℝ) : pack (unpack x) = x

@[simp]

theorem MeasureTheory.measurable_pack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] : Measurable pack

@[simp]

theorem MeasureTheory.measurable_unpack {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] : Measurable unpack

noncomputable def MeasureTheory.split : ↑unitInterval → ↑unitInterval × ↑unitInterval

Equations

• MeasureTheory.split = MeasureTheory.split._proof_1✝.choose

@[simp]

theorem MeasureTheory.measurable_split : Measurable split

theorem MeasureTheory.lintegral_split {f : ↑unitInterval → ↑unitInterval → ENNReal} (hf : Measurable fun (x : ↑unitInterval × ↑unitInterval) => match x with | (a, b) => f a b) : ∫⁻ (i : ↑unitInterval), f (split i).1 (split i).2 = ∫⁻ (i : ↑unitInterval) (j : ↑unitInterval), f i j