Commit 2023-07-29 10:10 8bbef902

View on Github →

feat(Probability/Cdf): 2 probability measures are equal iff their cdf are equal (#6122)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

added theorem StieltjesFunction.eq_of_measure_of_eq

added theorem StieltjesFunction.eq_of_measure_of_tendsto_atBot

added theorem StieltjesFunction.ext

Modified Mathlib/Probability/Cdf.lean

added theorem MeasureTheory.Measure.cdf_eq_iff

added theorem MeasureTheory.Measure.eq_of_cdf

deleted theorem MeasureTheory.Measure.ext_of_cdf

added theorem ProbabilityTheory.cdf_measure_stieltjesFunction