# Documentation

Mathlib.Probability.Distributions.Gaussian

# Gaussian distributions over ℝ #

We define a Gaussian measure over the reals.

## Main definitions #

• gaussianPdfReal: the function μ v x ↦ (1 / (sqrt (2 * pi * v))) * exp (- (x - μ)^2 / (2 * v)), which is the probability density function of a Gaussian distribution with mean μ and variance v (when v ≠ 0).
• gaussianPdf: ℝ≥0∞-valued pdf, gaussianPdf μ v x = ENNReal.ofReal (gaussianPdfReal μ v x).
• gaussianReal: a Gaussian measure on ℝ, parametrized by its mean μ and variance v. If v = 0, this is dirac μ, otherwise it is defined as the measure with density gaussianPdf μ v with respect to the Lebesgue measure.

## Main results #

• gaussianReal_add_const: if X is a random variable with Gaussian distribution with mean μ and variance v, then X + y is Gaussian with mean μ + y and variance v.
• gaussianReal_const_mul: if X is a random variable with Gaussian distribution with mean μ and variance v, then c * X is Gaussian with mean c * μ and variance c^2 * v.
noncomputable def ProbabilityTheory.gaussianPdfReal (μ : ) (v : NNReal) (x : ) :

Probability density function of the gaussian distribution with mean μ and variance v.

Equations
Instances For
theorem ProbabilityTheory.gaussianPdfReal_def (μ : ) (v : NNReal) :
= fun (x : ) => (Real.sqrt ( * v))⁻¹ * Real.exp (-(x - μ) ^ 2 / (2 * v))
theorem ProbabilityTheory.gaussianPdfReal_pos (μ : ) (v : NNReal) (x : ) (hv : v 0) :

The gaussian pdf is positive when the variance is not zero.

The gaussian pdf is nonnegative.

The gaussian pdf is measurable.

The gaussian pdf is strongly measurable.

theorem ProbabilityTheory.lintegral_gaussianPdfReal_eq_one (μ : ) {v : NNReal} (h : v 0) :
∫⁻ (x : ), = 1

The gaussian distribution pdf integrates to 1 when the variance is not zero.

theorem ProbabilityTheory.integral_gaussianPdfReal_eq_one (μ : ) {v : NNReal} (hv : v 0) :
∫ (x : ), = 1

The gaussian distribution pdf integrates to 1 when the variance is not zero.

theorem ProbabilityTheory.gaussianPdfReal_sub {μ : } {v : NNReal} (x : ) (y : ) :
=
theorem ProbabilityTheory.gaussianPdfReal_add {μ : } {v : NNReal} (x : ) (y : ) :
=
theorem ProbabilityTheory.gaussianPdfReal_inv_mul {μ : } {v : NNReal} {c : } (hc : c 0) (x : ) :
= |c| * ProbabilityTheory.gaussianPdfReal (c * μ) ({ val := c ^ 2, property := (_ : 0 c ^ 2) } * v) x
theorem ProbabilityTheory.gaussianPdfReal_mul {μ : } {v : NNReal} {c : } (hc : c 0) (x : ) :
= |c⁻¹| * ProbabilityTheory.gaussianPdfReal (c⁻¹ * μ) ({ val := (c ^ 2)⁻¹, property := (_ : 0 (c ^ 2)⁻¹) } * v) x
noncomputable def ProbabilityTheory.gaussianPdf (μ : ) (v : NNReal) (x : ) :

The pdf of a Gaussian distribution on ℝ with mean μ and variance v.

Equations
Instances For
theorem ProbabilityTheory.gaussianPdf_def (μ : ) (v : NNReal) :
= fun (x : ) =>
theorem ProbabilityTheory.gaussianPdf_pos (μ : ) {v : NNReal} (hv : v 0) (x : ) :
@[simp]
theorem ProbabilityTheory.lintegral_gaussianPdf_eq_one (μ : ) {v : NNReal} (h : v 0) :
∫⁻ (x : ), = 1
noncomputable def ProbabilityTheory.gaussianReal (μ : ) (v : NNReal) :

A Gaussian distribution on ℝ with mean μ and variance v.

Equations
Instances For
@[simp]
Equations
theorem ProbabilityTheory.gaussianReal_apply (μ : ) {v : NNReal} (hv : v 0) (s : ) :
s = ∫⁻ (x : ) in s,
theorem ProbabilityTheory.gaussianReal_apply_eq_integral (μ : ) {v : NNReal} (hv : v 0) (s : ) :
s = ENNReal.ofReal (∫ (x : ) in s, )
theorem MeasurableEmbedding.gaussianReal_comap_apply {μ : } {v : NNReal} (hv : v 0) {f : } (hf : ) {f' : } (h_deriv : ∀ (x : ), HasDerivAt f (f' x) x) {s : } (hs : ) :
= ENNReal.ofReal (∫ (x : ) in s, |f' x| * )
theorem MeasurableEquiv.gaussianReal_map_symm_apply {μ : } {v : NNReal} (hv : v 0) (f : ) {f' : } (h_deriv : ∀ (x : ), HasDerivAt (f) (f' x) x) {s : } (hs : ) :
(MeasureTheory.Measure.map (f.symm) ) s = ENNReal.ofReal (∫ (x : ) in s, |f' x| * )

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

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

theorem ProbabilityTheory.gaussianReal_map_const_mul {μ : } {v : NNReal} (c : ) :
MeasureTheory.Measure.map (fun (x : ) => c * x) = ProbabilityTheory.gaussianReal (c * μ) ({ val := c ^ 2, property := (_ : 0 c ^ 2) } * v)

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

theorem ProbabilityTheory.gaussianReal_map_mul_const {μ : } {v : NNReal} (c : ) :
MeasureTheory.Measure.map (fun (x : ) => x * c) = ProbabilityTheory.gaussianReal (c * μ) ({ val := c ^ 2, property := (_ : 0 c ^ 2) } * v)

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

theorem ProbabilityTheory.gaussianReal_add_const {μ : } {v : NNReal} {Ω : Type} {X : Ω} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = ) (y : ) :
MeasureTheory.Measure.map (fun (ω : Ω) => X ω + y) MeasureTheory.volume =

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

theorem ProbabilityTheory.gaussianReal_const_add {μ : } {v : NNReal} {Ω : Type} {X : Ω} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = ) (y : ) :
MeasureTheory.Measure.map (fun (ω : Ω) => y + X ω) MeasureTheory.volume =

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.

theorem ProbabilityTheory.gaussianReal_const_mul {μ : } {v : NNReal} {Ω : Type} {X : Ω} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = ) (c : ) :
MeasureTheory.Measure.map (fun (ω : Ω) => c * X ω) MeasureTheory.volume = ProbabilityTheory.gaussianReal (c * μ) ({ val := c ^ 2, property := (_ : 0 c ^ 2) } * v)

If X is a real random variable with Gaussian law with mean μ and variance v, then c * X has Gaussian law with mean c * μ and variance c^2 * v.

theorem ProbabilityTheory.gaussianReal_mul_const {μ : } {v : NNReal} {Ω : Type} {X : Ω} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = ) (c : ) :
MeasureTheory.Measure.map (fun (ω : Ω) => X ω * c) MeasureTheory.volume = ProbabilityTheory.gaussianReal (c * μ) ({ val := c ^ 2, property := (_ : 0 c ^ 2) } * v)

If X is a real random variable with Gaussian law with mean μ and variance v, then X * c has Gaussian law with mean c * μ and variance c^2 * v.