Commit 2024-09-26 17:42 c76e7c65

View on Github →

feat(Probability/Distributions): formalize Pareto distribution (#16713) Formalize Pareto distribution, using Gamma distribution as a reference.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Distributions/Pareto.lean

added theorem ProbabilityTheory.isProbabilityMeasure_paretoMeasure

added theorem ProbabilityTheory.lintegral_paretoPDF_eq_one

added theorem ProbabilityTheory.lintegral_paretoPDF_of_le

added theorem ProbabilityTheory.measurable_paretoPDFReal

added theorem ProbabilityTheory.paretoCDFReal_eq_integral

added theorem ProbabilityTheory.paretoCDFReal_eq_lintegral

added theorem ProbabilityTheory.paretoPDFReal_nonneg

added theorem ProbabilityTheory.paretoPDFReal_pos

added theorem ProbabilityTheory.paretoPDF_eq

added theorem ProbabilityTheory.paretoPDF_of_le

added theorem ProbabilityTheory.paretoPDF_of_lt

added theorem ProbabilityTheory.stronglyMeasurable_paretoPDFReal