Commit 2024-02-12 12:42 7ccf57f9

View on Github →

feat : Move various notions of uniform probability distributions to one file. (#10451) feat : collect uniform distribution for measures and uniform PMF in one file. This collects the various notions of uniform distribution in one file, to unify them with a forthcoming PR.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Probability/Density.lean

deleted theorem MeasureTheory.pdf.IsUniform.absolutelyContinuous

deleted theorem MeasureTheory.pdf.IsUniform.aemeasurable

deleted theorem MeasureTheory.pdf.IsUniform.hasPDF

deleted theorem MeasureTheory.pdf.IsUniform.integral_eq

deleted theorem MeasureTheory.pdf.IsUniform.isProbabilityMeasure

deleted theorem MeasureTheory.pdf.IsUniform.measure_preimage

deleted theorem MeasureTheory.pdf.IsUniform.mul_pdf_integrable

deleted theorem MeasureTheory.pdf.IsUniform.pdf_eq

deleted theorem MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_top

deleted theorem MeasureTheory.pdf.IsUniform.pdf_toReal_ae_eq

deleted theorem MeasureTheory.pdf.IsUniform.toMeasurable_iff

deleted def MeasureTheory.pdf.IsUniform

Renamed Mathlib/Probability/ProbabilityMassFunction/Uniform.lean to Mathlib/Probability/Distributions/Uniform.lean

added theorem MeasureTheory.pdf.IsUniform.absolutelyContinuous

added theorem MeasureTheory.pdf.IsUniform.aemeasurable

added theorem MeasureTheory.pdf.IsUniform.hasPDF

added theorem MeasureTheory.pdf.IsUniform.integral_eq

added theorem MeasureTheory.pdf.IsUniform.isProbabilityMeasure

added theorem MeasureTheory.pdf.IsUniform.measure_preimage

added theorem MeasureTheory.pdf.IsUniform.mul_pdf_integrable

added theorem MeasureTheory.pdf.IsUniform.pdf_eq

added theorem MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_top

added theorem MeasureTheory.pdf.IsUniform.pdf_toReal_ae_eq

added theorem MeasureTheory.pdf.IsUniform.toMeasurable_iff

added def MeasureTheory.pdf.IsUniform