Commit 2024-01-09 19:00 de2a15be

View on Github →

refactor(Probability/Distributions/Exponential): exponential distrubtion as special case of Gamma distribution (#9462) Refactor most proofs of Probability/Distributions/Exponential.lean in terms of the proofs in Probability/Distributions/Gamma.lean, as the exponential distribution is a special case of the Gamma distribution. Adds stronglyMeasurable_gammaPdfReal to Probability/Distributions/Gamma and [@measurability] tags to the necessary results in Probability/Distributions/Gamma and Probability/Distributions/Exponential. Style : improve consistency in notation.

Estimated changes

Modified Mathlib/Probability/Distributions/Exponential.lean

modified def ProbabilityTheory.expMeasure

modified theorem ProbabilityTheory.exponentialCdfReal_eq

modified theorem ProbabilityTheory.exponentialCdfReal_eq_integral

modified theorem ProbabilityTheory.exponentialCdfReal_eq_lintegral

modified theorem ProbabilityTheory.exponentialPdfReal_pos

modified theorem ProbabilityTheory.exponentialPdf_of_neg

deleted theorem ProbabilityTheory.hasDerivAt_exp_neg

added theorem ProbabilityTheory.isProbabilityMeasureExponential

modified theorem ProbabilityTheory.lintegral_exponentialPdf_eq_antiDeriv

modified theorem ProbabilityTheory.lintegral_exponentialPdf_eq_one

modified theorem ProbabilityTheory.measurable_exponentialPdfReal

modified theorem ProbabilityTheory.stronglyMeasurable_exponentialPdfReal

deleted theorem lintegral_eq_lintegral_Ici_add_Iio

Modified Mathlib/Probability/Distributions/Gamma.lean

added theorem ProbabilityTheory.stronglyMeasurable_gammaPdfReal