Theorems · Definition · probability
ProbabilityTheory.gaussianReal
ℝ → NNReal → MeasureTheory.Measure ℝ
A Gaussian distribution on ℝ with mean μ and variance v.
- Cited by
- 77 results in Mathlib
- Foundations
- Depth 243 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- MeasureTheory.Measurestatement · cited by 10,939
- NNRealstatement and proof · cited by 4,310
- MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
- MeasureTheory.Measure.withDensityproof · cited by 265
- MeasureTheory.Measure.diracproof · cited by 210
- ProbabilityTheory.gaussianPDFproof · cited by 18
Cited by80
Results whose statement or proof uses this declaration.
- ProbabilityTheory.stdGaussianproof · cited by 14
- ProbabilityTheory.IsGaussian.charFunDual_eqproof · cited by 9
- ProbabilityTheory.charFun_gaussianRealstatement · cited by 7
- ProbabilityTheory.gaussianReal_of_var_ne_zerostatement · cited by 7
- ProbabilityTheory.gaussianReal_zero_varstatement · cited by 7
- ProbabilityTheory.integral_id_gaussianRealstatement · cited by 6
- ProbabilityTheory.IsGaussian.map_eq_gaussianRealstatement · cited by 6
- ProbabilityTheory.variance_id_gaussianRealstatement · cited by 4
- ProbabilityTheory.gaussianReal_map_const_mulstatement and proof · cited by 4
- ProbabilityTheory.isGaussian_iff_gaussian_charFunDualproof · cited by 4
- ProbabilityTheory.mgf_fun_id_gaussianRealstatement and proof · cited by 3
- ProbabilityTheory.mgf_gaussianRealstatement and proof · cited by 3