Documentation Verification Report

CDF

📁 Source: Mathlib/Probability/CDF.lean

Statistics

Metric	Count
Definitions `cdf`	1
Theorems `cdf_eq_iff`, `eq_of_cdf`, `cdf_eq_real`, `cdf_le_one`, `cdf_measure_stieltjesFunction`, `cdf_nonneg`, `instIsProbabilityMeasurecdf`, `measure_cdf`, `monotone_cdf`, `ofReal_cdf`, `tendsto_cdf_atBot`, `tendsto_cdf_atTop`, `cdf_eq_real`	13
Total	14

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cdf_eq_iff` 📖	mathematical	—	`ProbabilityTheory.cdf`	—	`eq_of_cdf`
`eq_of_cdf` 📖	—	`ProbabilityTheory.cdf`	—	—	`instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `ProbabilityTheory.measure_cdf`

ProbabilityTheory

Definitions

Name	Category	Theorems
`cdf` 📖	CompOp	19 math math: `cdf_measure_stieltjesFunction`, `unitInterval.cdf_eq_real`, `cdf_paretoMeasure_eq_integral`, `cdf_expMeasure_eq`, `monotone_cdf`, `cdf_eq_real`, `cdf_nonneg`, `cdf_le_one`, `cdf_gammaMeasure_eq_lintegral`, `cdf_expMeasure_eq_integral`, `measure_cdf`, `tendsto_cdf_atTop`, `cdf_expMeasure_eq_lintegral`, `cdf_paretoMeasure_eq_lintegral`, `MeasureTheory.Measure.cdf_eq_iff`, `tendsto_cdf_atBot`, `cdf_gammaMeasure_eq_integral`, `ofReal_cdf`, `instIsProbabilityMeasurecdf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cdf_eq_real` 📖	mathematical	—	`StieltjesFunction.toFun` `Real` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `MeasureTheory.Measure.real` `Real.measurableSpace` `Set.Iic` `Real.instPreorder`	—	`MeasureTheory.measureReal_def` `ofReal_cdf` `ENNReal.toReal_ofReal` `cdf_nonneg`
`cdf_le_one` 📖	mathematical	—	`Real` `Real.instLE` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `Real.instOne`	—	`condCDF_le_one`
`cdf_measure_stieltjesFunction` 📖	mathematical	`Filter.Tendsto` `Real` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Filter.atBot` `Real.instPreorder` `nhds` `Real.instZero` `Filter.atTop` `Real.instOne`	`cdf` `StieltjesFunction.measure` `Real` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.instConditionallyCompleteLinearOrder` `Real.measurableSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `Field.toSemifield` `Real.instField` `Real.partialOrder` `PosMulReflectLE.toPosMulReflectLT` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `PosMulStrictMono.toPosMulReflectLE` `MulZeroClass.toMul` `MulZeroClass.toZero` `IsStrictOrderedRing.toPosMulStrictMono` `Real.semiring` `Real.instIsStrictOrderedRing`	—	`StieltjesFunction.eq_of_measure_of_tendsto_atBot` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `StieltjesFunction.measure_univ` `sub_zero` `ENNReal.ofReal_one` `measure_cdf` `tendsto_cdf_atBot`
`cdf_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf`	—	`condCDF_nonneg`
`instIsProbabilityMeasurecdf` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `Real` `Real.measurableSpace` `StieltjesFunction.measure` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.instConditionallyCompleteLinearOrder` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `Field.toSemifield` `Real.instField` `Real.partialOrder` `PosMulReflectLE.toPosMulReflectLT` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `PosMulStrictMono.toPosMulReflectLE` `MulZeroClass.toMul` `MulZeroClass.toZero` `IsStrictOrderedRing.toPosMulStrictMono` `Real.semiring` `Real.instIsStrictOrderedRing`	—	`instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `StieltjesFunction.measure_univ` `tendsto_cdf_atBot` `tendsto_cdf_atTop` `sub_zero` `ENNReal.ofReal_one`
`measure_cdf` 📖	mathematical	—	`StieltjesFunction.measure` `Real` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.instConditionallyCompleteLinearOrder` `Real.measurableSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `Field.toSemifield` `Real.instField` `Real.partialOrder` `PosMulReflectLE.toPosMulReflectLT` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `PosMulStrictMono.toPosMulReflectLE` `MulZeroClass.toMul` `MulZeroClass.toZero` `IsStrictOrderedRing.toPosMulStrictMono` `Real.semiring` `Real.instIsStrictOrderedRing`	—	`MeasureTheory.Measure.ext_of_Iic` `instSecondCountableTopologyReal` `instOrderTopologyReal` `Real.borelSpace` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasurecdf` `StieltjesFunction.measure_Iic` `tendsto_cdf_atBot` `sub_zero` `ofReal_cdf`
`monotone_cdf` 📖	mathematical	—	`Monotone` `Real` `Real.instPreorder` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf`	—	`StieltjesFunction.mono`
`ofReal_cdf` 📖	mathematical	—	`ENNReal.ofReal` `StieltjesFunction.toFun` `Real` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `DFunLike.coe` `MeasureTheory.Measure` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.Iic` `Real.instPreorder`	—	`lintegral_condCDF` `MeasureTheory.Measure.prod.instIsFiniteMeasure` `MeasureTheory.Measure.dirac.instIsFiniteMeasure` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasureTheory.Measure.fst_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `instSecondCountableTopologyReal` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.lintegral_dirac` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Unit.borelSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountablePUnit` `PseudoEMetricSpace.pseudoMetrizableSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.Measure.prod_prod` `MeasureTheory.IsProbabilityMeasure.measure_univ` `MeasureTheory.Measure.dirac.isProbabilityMeasure` `one_mul`
`tendsto_cdf_atBot` 📖	mathematical	—	`Filter.Tendsto` `Real` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `Filter.atBot` `Real.instPreorder` `nhds` `Real.instZero`	—	`tendsto_condCDF_atBot`
`tendsto_cdf_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cdf` `Filter.atTop` `Real.instPreorder` `nhds` `Real.instOne`	—	`tendsto_condCDF_atTop`

ProbabilityTheory.unitInterval

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cdf_eq_real` 📖	mathematical	—	`StieltjesFunction.toFun` `Real` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ProbabilityTheory.cdf` `MeasureTheory.Measure.map` `Set` `Set.instMembership` `unitInterval` `Subtype.instMeasurableSpace` `Real.measurableSpace` `MeasureTheory.Measure.real` `Set.Elem` `Set.Icc` `Subtype.preorder` `Real.instPreorder` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `ProbabilityTheory.cdf_eq_real` `MeasureTheory.Measure.isProbabilityMeasure_map` `Measurable.aemeasurable` `Measurable.subtype_coe` `measurable_id'` `MeasureTheory.map_measureReal_apply` `measurable_subtype_coe` `measurableSet_Iic` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `unitInterval.subtype_Iic_eq_Icc`

---

← Back to Index