Commit 2023-10-16 15:56 7de02716

View on Github →

feat: add a Gaussian probability distribution over ℝ (#7671)

Create a new Distributions folder for particular probability distributions.
Define a Gaussian distribution over ℝ by its pdf From a project started at LftCM 2023.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

added theorem MeasureTheory.mutuallySingular_dirac

Created Mathlib/Probability/Distributions/Gaussian.lean

added def ProbabilityTheory.gaussianPdf

added def ProbabilityTheory.gaussianPdfReal

added theorem ProbabilityTheory.gaussianPdfReal_def

added theorem ProbabilityTheory.gaussianPdfReal_nonneg

added theorem ProbabilityTheory.gaussianPdfReal_pos

added theorem ProbabilityTheory.gaussianPdfReal_zero_var

added theorem ProbabilityTheory.gaussianPdf_def

added theorem ProbabilityTheory.gaussianPdf_pos

added theorem ProbabilityTheory.gaussianPdf_zero_var

added def ProbabilityTheory.gaussianReal

added theorem ProbabilityTheory.gaussianReal_absolutelyContinuous'

added theorem ProbabilityTheory.gaussianReal_absolutelyContinuous

added theorem ProbabilityTheory.gaussianReal_apply

added theorem ProbabilityTheory.gaussianReal_apply_eq_integral

added theorem ProbabilityTheory.gaussianReal_of_var_ne_zero

added theorem ProbabilityTheory.gaussianReal_zero_var

added theorem ProbabilityTheory.integrable_gaussianPdfReal

added theorem ProbabilityTheory.integral_gaussianPdfReal_eq_one

added theorem ProbabilityTheory.lintegral_gaussianPdfReal_eq_one

added theorem ProbabilityTheory.lintegral_gaussianPdf_eq_one

added theorem ProbabilityTheory.measurable_gaussianPdf

added theorem ProbabilityTheory.measurable_gaussianPdfReal

added theorem ProbabilityTheory.rnDeriv_gaussianReal

added theorem ProbabilityTheory.stronglyMeasurable_gaussianPdfReal