Commit 2023-06-23 09:36 eff6c1d0

View on Github →

feat(Probability/Cdf): cumulative distribution function of a probability measure (#5392)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

added theorem MeasureTheory.Measure.fst_prod

added theorem MeasureTheory.Measure.snd_prod

Created Mathlib/Probability/Cdf.lean

added theorem MeasureTheory.Measure.ext_of_cdf

added def ProbabilityTheory.cdf

added theorem ProbabilityTheory.cdf_eq_toReal

added theorem ProbabilityTheory.cdf_le_one

added theorem ProbabilityTheory.cdf_nonneg

added theorem ProbabilityTheory.measure_cdf

added theorem ProbabilityTheory.monotone_cdf

added theorem ProbabilityTheory.ofReal_cdf

added theorem ProbabilityTheory.tendsto_cdf_atBot

added theorem ProbabilityTheory.tendsto_cdf_atTop