Theorems · Definition · probability
ProbabilityTheory.gaussianPDF
ℝ → NNReal → ℝ → ENNReal
The pdf of a Gaussian distribution on ℝ with mean μ and variance v.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- ENNRealstatement · cited by 9,879
- NNRealstatement and proof · cited by 4,310
- ENNReal.ofRealproof · cited by 863
- ProbabilityTheory.gaussianPDFRealproof · cited by 24
Cited by19
Results whose statement or proof uses this declaration.
- ProbabilityTheory.gaussianRealproof · cited by 77
- ProbabilityTheory.gaussianReal_of_var_ne_zerostatement · cited by 7
- ProbabilityTheory.measurable_gaussianPDFstatement · cited by 3
- ProbabilityTheory.measurable_uncurry_gaussianPDFstatement · cited by 3
- ProbabilityTheory.gaussianPDF_defstatement · cited by 2
- ProbabilityTheory.gaussianPDF_posstatement · cited by 2
- ProbabilityTheory.gaussianReal_apply_eq_integralproof · cited by 2
- ProbabilityTheory.gaussianPDF_lt_topstatement · cited by 1
- ProbabilityTheory.gaussianPDF_zero_varstatement · cited by 1
- ProbabilityTheory.integral_gaussianReal_eq_integral_smulproof · cited by 1
- ProbabilityTheory.gaussianReal_applystatement and proof · cited by 1
- ProbabilityTheory.stronglyMeasurable_uncurry_gaussianPDFstatement · cited by 1