Theorems · Theorem · probability

ProbabilityTheory.gaussianReal_map_add_const

∀ {μ : ℝ} {v : NNReal} (y : ℝ),
  MeasureTheory.Measure.map (fun x => x + y) (ProbabilityTheory.gaussianReal μ v) =
    ProbabilityTheory.gaussianReal (μ + y) v

The map of a Gaussian distribution by addition of a constant is a Gaussian.

Defined in

Mathlib.Probability.Distributions.Gaussian.Real

Cited by

3 results in Mathlib

Foundations

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