Theorems · Definition · probability

ProbabilityTheory.gaussianPDFReal

ℝ → NNReal → ℝ → ℝ

Probability density function of the Gaussian distribution with mean μ and variance v.

Defined in: Mathlib.Probability.Distributions.Gaussian.Real
Cited by: 24 results in Mathlib
Foundations: Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
NNRealstatement and proof · cited by 4,310
Real.piproof · cited by 1,774
NNReal.toRealproof · cited by 1,260
Real.expproof · cited by 871
Real.sqrtproof · cited by 545

Cited by25

Results whose statement or proof uses this declaration.

ProbabilityTheory.gaussianPDFproof · cited by 18
ProbabilityTheory.gaussianPDFReal_nonnegstatement · cited by 6
ProbabilityTheory.gaussianReal_map_const_mulproof · cited by 4
ProbabilityTheory.integrable_gaussianPDFRealstatement · cited by 4
ProbabilityTheory.gaussianReal_map_add_constproof · cited by 3
ProbabilityTheory.complexMGF_id_gaussianRealproof · cited by 3
ProbabilityTheory.measurable_uncurry_gaussianPDFRealstatement · cited by 3
ProbabilityTheory.gaussianPDFReal_substatement · cited by 2
ProbabilityTheory.gaussianPDF_defstatement · cited by 2
ProbabilityTheory.gaussianReal_apply_eq_integralstatement and proof · cited by 2
ProbabilityTheory.lintegral_gaussianPDFReal_eq_onestatement and proof · cited by 2
MeasurableEquiv.gaussianReal_map_symm_applystatement and proof · cited by 2