Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-31 15:17 9c473c1d

View on Github →

feat(probability/density): probability of event in uniform distribution (#15678)

Estimated changes

Modified src/probability/density.lean

modified theorem measure_theory.pdf.is_uniform.integral_eq

added theorem measure_theory.pdf.is_uniform.is_probability_measure

added theorem measure_theory.pdf.is_uniform.measure_preimage

modified theorem measure_theory.pdf.is_uniform.mul_pdf_integrable