Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-10 09:54 3d438baf

View on Github →

feat(probability_theory/density): add continuous uniform distribution (#9385)

Estimated changes

Modified src/algebra/indicator_function.lean

added theorem set.mul_indicator_eq_one_iff

Modified src/measure_theory/measure/measure_space_def.lean

added theorem set.mul_indicator_ae_eq_one

Modified src/probability_theory/density.lean

added theorem measure_theory.has_pdf_of_pdf_ne_zero

added theorem measure_theory.pdf.is_uniform.has_pdf

added theorem measure_theory.pdf.is_uniform.integral_eq

added theorem measure_theory.pdf.is_uniform.mul_pdf_integrable

added theorem measure_theory.pdf.is_uniform.pdf_to_real_ae_eq

added def measure_theory.pdf.is_uniform