Commit 2026-02-16 09:07 c18ef685

View on Github →

feat(Probability): Add Cauchy distribution (#33860)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Distributions/Cauchy.lean

added theorem Probability.cauchyMeasure_of_scale_ne_zero

added theorem Probability.cauchyMeasure_zero_scale

added theorem Probability.cauchyPDFReal_def'

added theorem Probability.cauchyPDFReal_def

added theorem Probability.cauchyPDFReal_scale_zero

added theorem Probability.cauchyPDF_def

added theorem Probability.cauchyPDF_pos

added theorem Probability.cauchyPDF_scale_zero

added theorem Probability.integrable_cauchyPDFReal

added theorem Probability.integral_cauchyPDFReal

added theorem Probability.lintegral_cauchyPDF_eq_one

added theorem Probability.measurable_cauchyPDF

added theorem Probability.measurable_cauchyPDFReal

added theorem Probability.stronglyMeasurable_cauchyPDF

added theorem Probability.stronglyMeasurable_cauchyPDFReal