Commit 2024-01-05 13:07 cace5e5a

View on Github →

feat : Add Gamma distribution (#9408) Add pdf, CDF and measure of Gamma distribution. Add proof that this is indeed a probability distribution. Add proofs that relate the various definitions. TODO: Refactor Probability/Distributions/Exponential.lean using calls to the results in this file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

added theorem Complex.integral_cpow_mul_exp_neg_mul_Ioi

added theorem Real.integral_rpow_mul_exp_neg_mul_Ioi

Modified Mathlib/Probability/Distributions/Exponential.lean

deleted theorem lintegral_Iic_eq_lintegral_Iio_add_Icc

Created Mathlib/Probability/Distributions/Gamma.lean

added def ProbabilityTheory.gammaCdfReal

added theorem ProbabilityTheory.gammaCdfReal_eq_integral

added theorem ProbabilityTheory.gammaCdfReal_eq_lintegral

added def ProbabilityTheory.gammaMeasure

added def ProbabilityTheory.gammaPdf

added def ProbabilityTheory.gammaPdfReal

added theorem ProbabilityTheory.gammaPdfReal_nonneg

added theorem ProbabilityTheory.gammaPdfReal_pos

added theorem ProbabilityTheory.gammaPdf_eq

added theorem ProbabilityTheory.gammaPdf_of_neg

added theorem ProbabilityTheory.gammaPdf_of_nonneg

added theorem ProbabilityTheory.isProbabilityMeasureGamma

added theorem ProbabilityTheory.lintegral_gammaPdf_eq_one

added theorem ProbabilityTheory.lintegral_gammaPdf_of_nonpos

added theorem ProbabilityTheory.measurable_gammaPdfReal

added theorem lintegral_Iic_eq_lintegral_Iio_add_Icc