Documentation

Verification.UnitCDFInverse

← Mathematical handbook
source
noncomputable def Verification.unitCDF (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] (t : ↑unitInterval) :
↑unitInterval
Equations
Instances For
    source
    theorem Verification.unitCDF_eq (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] (t : ↑unitInterval) :
    unitCDF μ t = ProbabilityTheory.cdfUnit (MeasureTheory.Measure.map Subtype.val μ) ↑t
    source
    theorem Verification.unitCDF_real_atomless (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.NullSingletonClass μ] :
    MeasureTheory.NullSingletonClass (MeasureTheory.Measure.map Subtype.val μ)
    source
    theorem Verification.unitCDF_continuous (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] :
    Continuous (unitCDF μ)
    source
    theorem Verification.unitCDF_map (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] :
    MeasureTheory.Measure.map (unitCDF μ) μ = MeasureTheory.volume
    source
    theorem Verification.unitCDF_zero (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] :
    unitCDF μ 0 = 0
    source
    theorem Verification.unitCDF_one (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] :
    unitCDF μ 1 = 1
    source
    theorem Verification.unitCDF_surjective (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] :
    Function.Surjective (unitCDF μ)
    source
    theorem Verification.unitCDF_quantile (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] (v : ↑unitInterval) :
    unitCDF μ (ProbabilityTheory.unitQuantile μ v) = v
    source
    theorem Verification.quantile_unitCDF_ae (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] :
    (fun (t : ↑unitInterval) => ProbabilityTheory.unitQuantile μ (unitCDF μ t)) =ᵐ[μ] id

    Flat intervals are harmless: the quantile is a left inverse almost surely.