Theorems · Theorem · probability

ProbabilityTheory.gaussianReal_const_add

∀ {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasLaw X (ProbabilityTheory.gaussianReal μ v) P →
    ∀ (y : ℝ), ProbabilityTheory.HasLaw (fun ω => y + X ω) (ProbabilityTheory.gaussianReal (μ + y) v) P

If X is a real random variable with Gaussian law with mean μ and variance v, then y + X has Gaussian law with mean μ + y and variance v.

Defined in

Mathlib.Probability.Distributions.Gaussian.Real

Cited by

0 results in Mathlib

Foundations

Depth 290 from the axioms · uses propext, Classical.choice, Quot.sound