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
instance unitInterval.instNoAtomsElemRealVolume :
MeasureTheory.NoAtoms MeasureTheory.volume
source
theorem unitInterval.measurable_symm :
Measurable symm
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