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	26 math math: paretoCDFReal_eq_lintegral, cdf_measure_stieltjesFunction, unitInterval.cdf_eq_real, gammaCDFReal_eq_lintegral, cdf_paretoMeasure_eq_integral, cdf_expMeasure_eq, gammaCDFReal_eq_integral, monotone_cdf, cdf_eq_real, cdf_nonneg, cdf_le_one, cdf_gammaMeasure_eq_lintegral, exponentialCDFReal_eq_integral, cdf_expMeasure_eq_integral, paretoCDFReal_eq_integral, measure_cdf, exponentialCDFReal_eq, tendsto_cdf_atTop, cdf_expMeasure_eq_lintegral, cdf_paretoMeasure_eq_lintegral, MeasureTheory.Measure.cdf_eq_iff, tendsto_cdf_atBot, exponentialCDFReal_eq_lintegral, 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 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