Theorem ProbabilityTheory.isProbabilityMeasure_paretoMeasure

Modification history

2024-09-26 17:42
Mathlib/Probability/Distributions/Pareto.lean
feat(Probability/Distributions): formalize Pareto distribution (#16713) …
Added ProbabilityTheory.isProbabilityMeasure_paretoMeasureView on Github →