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
๐Ÿ”ธ coverage
@[implicit_reducible]
noncomputable instance unitInterval.instMeasureSpaceElemReal :
MeasureTheory.MeasureSpace โ†‘unitInterval
source
๐Ÿ“ coverage
theorem unitInterval.volume_def :
MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
source
๐Ÿ“ coverage
instance unitInterval.instIsProbabilityMeasureElemRealVolume :
MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
source
๐Ÿ“ coverage
theorem unitInterval.measurableEmbedding_coe :
MeasurableEmbedding Subtype.val
source
๐Ÿ“ coverage
theorem unitInterval.volume_apply {s : Set โ†‘unitInterval} :
MeasureTheory.volume s = MeasureTheory.volume (Subtype.val '' s)
source
๐Ÿ“ coverage
theorem unitInterval.measurePreserving_coe :
MeasureTheory.MeasurePreserving Subtype.val MeasureTheory.volume (MeasureTheory.volume.restrict unitInterval)
source
๐Ÿ“ coverage
instance unitInterval.instNoAtomsElemRealVolume :
MeasureTheory.NoAtoms MeasureTheory.volume
source
๐Ÿ“ coverage
theorem unitInterval.measurable_symm :
Measurable symm
source
๐Ÿ”ธ coverage
def unitInterval.symmMeasurableEquiv :
โ†‘unitInterval โ‰ƒแต โ†‘unitInterval

unitInterval.symm bundled as a measurable equivalence.

Instances For
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.symmMeasurableEquiv_symm_apply (aโœ : โ†‘unitInterval) :
    symmMeasurableEquiv.symm aโœ = symm aโœ
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.symmMeasurableEquiv_apply (aโœ : โ†‘unitInterval) :
    symmMeasurableEquiv aโœ = symm aโœ
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.symm_symmMeasurableEquiv :
    symmMeasurableEquiv.symm = symmMeasurableEquiv
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.coe_symmMeasurableEquiv :
    โ‡‘symmMeasurableEquiv = symm
    source
    ๐Ÿ“ coverage
    theorem unitInterval.measurePreserving_symm :
    MeasureTheory.MeasurePreserving symm MeasureTheory.volume MeasureTheory.volume
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_Iic (x : โ†‘unitInterval) :
    MeasureTheory.volume (Set.Iic x) = ENNReal.ofReal โ†‘x
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_Iio (x : โ†‘unitInterval) :
    MeasureTheory.volume (Set.Iio x) = ENNReal.ofReal โ†‘x
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_Ici (x : โ†‘unitInterval) :
    MeasureTheory.volume (Set.Ici x) = ENNReal.ofReal (1 - โ†‘x)
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_Ioi (x : โ†‘unitInterval) :
    MeasureTheory.volume (Set.Ioi x) = ENNReal.ofReal (1 - โ†‘x)
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_Icc (x y : โ†‘unitInterval) :
    MeasureTheory.volume (Set.Icc x y) = ENNReal.ofReal (โ†‘y - โ†‘x)
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_uIcc (x y : โ†‘unitInterval) :
    MeasureTheory.volume (Set.uIcc x y) = edist y x
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_Ico (x y : โ†‘unitInterval) :
    MeasureTheory.volume (Set.Ico x y) = ENNReal.ofReal (โ†‘y - โ†‘x)
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_Ioc (x y : โ†‘unitInterval) :
    MeasureTheory.volume (Set.Ioc x y) = ENNReal.ofReal (โ†‘y - โ†‘x)
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_uIoc (x y : โ†‘unitInterval) :
    MeasureTheory.volume (Set.uIoc x y) = edist y x
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_Ioo (x y : โ†‘unitInterval) :
    MeasureTheory.volume (Set.Ioo x y) = ENNReal.ofReal (โ†‘y - โ†‘x)
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem unitInterval.volume_uIoo (x y : โ†‘unitInterval) :
    MeasureTheory.volume (Set.uIoo x y) = edist y x