LeanPool.QuasiBorelSpaces.MeasureTheory.Randomization #

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.MeasureTheory.Randomization.

source

noncomputable def MeasureTheory.Measure.normalize {r : ℝ} (x : ↑(Set.Ico 0 r)) :

↑unitInterval

normalize is the canonical injection from [0, r) to [0, 1].

Equations

MeasureTheory.Measure.normalize x = ⟨↑x / r, ⋯⟩

Instances For

source

@[simp]

theorem MeasureTheory.Measure.measurable_normalize (r : ℝ) :

Measurable normalize

source

theorem MeasureTheory.Measure.injective_normalize (r : ℝ) :

Function.Injective normalize

source

@[instance_reducible]

noncomputable instance MeasureTheory.Measure.instMeasureSpaceElemRealIcoOfNatLeanPool (r : ℝ) :

MeasureSpace ↑(Set.Ico 0 r)

Equations

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

source

instance MeasureTheory.Measure.instIsEmptyElemRealIcoOfNat_leanPool :

IsEmpty ↑(Set.Ico 0 0)

source

@[simp]

theorem MeasureTheory.Measure.volume_zero :

volume = 0

source

@[simp]

theorem MeasureTheory.Measure.measurableEmbedding_normalize (r : ℝ) :

MeasurableEmbedding normalize

source

@[simp]

theorem MeasureTheory.Measure.range_normalize {r : ℝ} (hr : 0 < r) :

Set.range normalize = Set.Ico 0 1

source

@[simp]

theorem MeasureTheory.Measure.volume_restrict_normalize :

volume.restrict (Set.Ico 0 1) = volume

source

noncomputable def MeasureTheory.Measure.packI {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] :

A → ↑unitInterval

Encode a standard Borel space into the unit interval.

Equations

MeasureTheory.Measure.packI = MeasureTheory.unpack ∘ MeasureTheory.pack

Instances For

source

noncomputable def MeasureTheory.Measure.unpackI {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] [Nonempty A] :

↑unitInterval → A

Decode the unit-interval representation of a nonempty standard Borel space.

Equations

MeasureTheory.Measure.unpackI = MeasureTheory.unpack ∘ MeasureTheory.pack

Instances For

source

noncomputable def MeasureTheory.Measure.det {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] (μ : Measure A) [IsProbabilityMeasure μ] :

↑unitInterval → A

The function det μ is a function such that volume.map (det μ) = μ.

Equations

μ.det = MeasureTheory.Measure.unpackI ∘ MeasureTheory.quantile (MeasureTheory.Measure.map MeasureTheory.Measure.packI μ)

Instances For

source

theorem MeasureTheory.Measure.measurable_det {A : Type u_2} {B : Type u_1} [MeasurableSpace A] [MeasurableSpace B] [StandardBorelSpace B] {μ : A → Measure B} [∀ (x : A), IsProbabilityMeasure (μ x)] (hμ : Measurable μ) {i : A → ↑unitInterval} (hi : Measurable i) :

Measurable fun (x : A) => (μ x).det (i x)

source

@[simp]

theorem MeasureTheory.Measure.eq_det_volume {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] (μ : Measure A) [IsProbabilityMeasure μ] :

map μ.det volume = μ

source

noncomputable def MeasureTheory.Measure.detf {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] (μ : Measure A) [IsFiniteMeasure μ] (r : ↑(Set.Ico 0 (μ Set.univ).toReal)) :

The function detf μ is a function such that volume.map (detf μ) = μ.

Equations

μ.detf r = ((μ Set.univ)⁻¹ • μ).det (MeasureTheory.Measure.normalize r)

Instances For

source

theorem MeasureTheory.Measure.measurable_detf {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] {μ : Measure A} [IsFiniteMeasure μ] :

Measurable μ.detf

source

@[simp]

theorem MeasureTheory.Measure.eq_detf_volume {A : Type u_1} [MeasurableSpace A] [StandardBorelSpace A] (μ : Measure A) [IsFiniteMeasure μ] :

map μ.detf volume = μ

source

noncomputable def MeasureTheory.splitI :

↑unitInterval → ↑unitInterval × ↑unitInterval

Splits I into two independent copies of I via the determinizing map of the product Lebesgue measure on I × I.

Equations

MeasureTheory.splitI = MeasureTheory.volume.det

Instances For

source

@[simp]

theorem MeasureTheory.measurable_splitI :

Measurable splitI

source

theorem MeasureTheory.measurePreserving_splitI :

MeasurePreserving splitI volume volume