Commit 2023-11-21 21:57 3f12ad8e

View on Github →

feat: Real Exponential Distribution (#8253) Introduction of the real-valued exponential PDF and CDF

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Distributions/Exponential.lean

added def ProbabilityTheory.expMeasure

added theorem ProbabilityTheory.exp_neg_integrableOn_Ioc

added def ProbabilityTheory.exponentialCdfReal

added theorem ProbabilityTheory.exponentialCdfReal_eq

added theorem ProbabilityTheory.exponentialCdfReal_eq_integral

added theorem ProbabilityTheory.exponentialCdfReal_eq_lintegral

added def ProbabilityTheory.exponentialPdf

added def ProbabilityTheory.exponentialPdfReal

added theorem ProbabilityTheory.exponentialPdfReal_nonneg

added theorem ProbabilityTheory.exponentialPdfReal_pos

added theorem ProbabilityTheory.exponentialPdf_eq

added theorem ProbabilityTheory.exponentialPdf_of_neg

added theorem ProbabilityTheory.exponentialPdf_of_nonneg

added theorem ProbabilityTheory.hasDerivAt_exp_neg

added theorem ProbabilityTheory.hasDerivAt_neg_exp_mul_exp

added theorem ProbabilityTheory.lintegral_exponentialPdf_eq_antiDeriv

added theorem ProbabilityTheory.lintegral_exponentialPdf_eq_one

added theorem ProbabilityTheory.lintegral_exponentialPdf_of_nonpos

added theorem ProbabilityTheory.measurable_exponentialPdfReal

added theorem ProbabilityTheory.stronglyMeasurable_exponentialPdfReal

added theorem lintegral_Iic_eq_lintegral_Iio_add_Icc

added theorem lintegral_eq_lintegral_Ici_add_Iio