Commit 2024-01-26 20:18 781af012

View on Github →

feat: drop unneeded assumptions in IsUniform.integral_eq (#10021)

Estimated changes

Modified Mathlib/Probability/Density.lean

modified theorem MeasureTheory.pdf.IsUniform.hasPDF

deleted theorem MeasureTheory.pdf.IsUniform.hasPDF₀

modified theorem MeasureTheory.pdf.IsUniform.mul_pdf_integrable

modified theorem MeasureTheory.pdf.IsUniform.pdf_eq

added theorem MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_top

modified theorem MeasureTheory.pdf.IsUniform.pdf_toReal_ae_eq

added theorem MeasureTheory.pdf.IsUniform.toMeasurable_iff