Theorems · Theorem · probability
ProbabilityTheory.gaussianPDFReal_inv_mul
∀ {μ : ℝ} {v : NNReal} {c : ℝ},
c ≠ 0 →
∀ (x : ℝ),
ProbabilityTheory.gaussianPDFReal μ v (c⁻¹ * x) =
|c| * ProbabilityTheory.gaussianPDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x- Cited by
- 2 results in Mathlib
- Foundations
- Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites31
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
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- Nat.cast_zeroproof · cited by 1,870
- absstatement and proof · cited by 1,814
- Real.piproof · cited by 1,774
- mul_assocproof · cited by 1,667
- NNReal.toRealproof · cited by 1,260
- le_of_ltproof · cited by 1,175
- one_ne_zeroproof · cited by 885
- Real.expproof · cited by 871
Cited by2
Results whose statement or proof uses this declaration.
- ProbabilityTheory.gaussianReal_map_const_mulproof · cited by 4
- ProbabilityTheory.gaussianPDFReal_mulproof · cited by 0