Documentation

Mathlib.MeasureTheory.Constructions.UnitInterval

The canonical measure on the unit interval #

This file provides a MeasureTheory.MeasureSpace instance on unitInterval, and shows it is a probability measure with no atoms.

It also contains some basic results on the volume of various interval sets.

source
noncomputable instance unitInterval.instMeasureSpaceElemReal :
MeasureTheory.MeasureSpace ↑unitInterval
Equations
source
theorem unitInterval.volume_def :
MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
source
instance unitInterval.instIsProbabilityMeasureElemRealVolume :
MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
source
theorem unitInterval.measurableEmbedding_coe :
MeasurableEmbedding Subtype.val
source
theorem unitInterval.volume_apply {s : Set ↑unitInterval} :
MeasureTheory.volume s = MeasureTheory.volume (Subtype.val '' s)
source
theorem unitInterval.measurePreserving_coe :
MeasureTheory.MeasurePreserving Subtype.val MeasureTheory.volume (MeasureTheory.volume.restrict unitInterval)
source
instance unitInterval.instNoAtomsElemRealVolume :
MeasureTheory.NoAtoms MeasureTheory.volume
source
theorem unitInterval.measurable_symm :
Measurable symm
source
def unitInterval.symmMeasurableEquiv :
↑unitInterval ≃ᵐ ↑unitInterval

unitInterval.symm bundled as a measurable equivalence.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem unitInterval.symmMeasurableEquiv_apply (a✝ : ↑unitInterval) :
    symmMeasurableEquiv a✝ = symm a✝
    source
    @[simp]
    theorem unitInterval.symmMeasurableEquiv_symm_apply (a✝ : ↑unitInterval) :
    symmMeasurableEquiv.symm a✝ = symm a✝
    source
    @[simp]
    theorem unitInterval.symm_symmMeasurableEquiv :
    symmMeasurableEquiv.symm = symmMeasurableEquiv
    source
    @[simp]
    theorem unitInterval.coe_symmMeasurableEquiv :
    ⇑symmMeasurableEquiv = symm
    source
    theorem unitInterval.measurePreserving_symm :
    MeasureTheory.MeasurePreserving symm MeasureTheory.volume MeasureTheory.volume
    source
    @[simp]
    theorem unitInterval.volume_Iic (x : ↑unitInterval) :
    MeasureTheory.volume (Set.Iic x) = ENNReal.ofReal ↑x
    source
    @[simp]
    theorem unitInterval.volume_Iio (x : ↑unitInterval) :
    MeasureTheory.volume (Set.Iio x) = ENNReal.ofReal ↑x
    source
    @[simp]
    theorem unitInterval.volume_Ici (x : ↑unitInterval) :
    MeasureTheory.volume (Set.Ici x) = ENNReal.ofReal (1 - ↑x)
    source
    @[simp]
    theorem unitInterval.volume_Ioi (x : ↑unitInterval) :
    MeasureTheory.volume (Set.Ioi x) = ENNReal.ofReal (1 - ↑x)
    source
    @[simp]
    theorem unitInterval.volume_Icc (x y : ↑unitInterval) :
    MeasureTheory.volume (Set.Icc x y) = ENNReal.ofReal (↑y - ↑x)
    source
    @[simp]
    theorem unitInterval.volume_uIcc (x y : ↑unitInterval) :
    MeasureTheory.volume (Set.uIcc x y) = edist y x
    source
    @[simp]
    theorem unitInterval.volume_Ico (x y : ↑unitInterval) :
    MeasureTheory.volume (Set.Ico x y) = ENNReal.ofReal (↑y - ↑x)
    source
    @[simp]
    theorem unitInterval.volume_Ioc (x y : ↑unitInterval) :
    MeasureTheory.volume (Set.Ioc x y) = ENNReal.ofReal (↑y - ↑x)
    source
    @[simp]
    theorem unitInterval.volume_uIoc (x y : ↑unitInterval) :
    MeasureTheory.volume (Set.uIoc x y) = edist y x
    source
    @[simp]
    theorem unitInterval.volume_Ioo (x y : ↑unitInterval) :
    MeasureTheory.volume (Set.Ioo x y) = ENNReal.ofReal (↑y - ↑x)
    source
    @[simp]
    theorem unitInterval.volume_uIoo (x y : ↑unitInterval) :
    MeasureTheory.volume (Set.uIoo x y) = edist y x