Commit 2024-02-16 14:44 2d36cb15

View on Github →

feat : refactor IsUniform through uniformMeasure (#10456) Refactor the definitions and proofs of IsUniform through the new uniformMeasure, which abstracts away from the need of a random variable and probability space. A future PR can refactor the PMF parts in terms of a uniformMeasure. This was #10141, which was split into a small PR to move the results (merged) and this one.

Estimated changes

Modified Mathlib/Probability/ConditionalProbability.lean

added theorem ProbabilityTheory.cond_absolutelyContinuous

added theorem ProbabilityTheory.cond_apply'

added theorem ProbabilityTheory.cond_isProbabilityMeasure_of_finite

added theorem ProbabilityTheory.cond_toMeasurable_eq

Modified Mathlib/Probability/Distributions/Uniform.lean

added theorem MeasureTheory.pdf.IsUniform.cond

modified def MeasureTheory.pdf.IsUniform

added def MeasureTheory.pdf.uniformPDF

added theorem MeasureTheory.pdf.uniformPDF_eq_pdf

added theorem MeasureTheory.pdf.uniformPDF_ite