Documentation

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
Instances For
    source
    @[simp]
    theorem MeasureTheory.Measure.measurable_normalize (r : ℝ) :
    Measurable normalize
    source
    theorem MeasureTheory.Measure.injective_normalize (r : ℝ) :
    Function.Injective normalize
    source
    noncomputable instance MeasureTheory.Measure.instMeasureSpaceElemRealIcoOfNat_quasiBorelSpaces (r : ℝ) :
    MeasureSpace ↑(Set.Ico 0 r)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance MeasureTheory.Measure.instIsEmptyElemRealIcoOfNat_quasiBorelSpaces :
    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.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
    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)) :
      A

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

      Equations
      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
        Equations
        Instances For
          source
          @[simp]
          theorem MeasureTheory.measurable_splitI :
          Measurable splitI
          source
          theorem MeasureTheory.measurePreserving_splitI :
          MeasurePreserving splitI volume volume