# 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 : ) => (( * 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 * μ) (c ^ 2, * v) x
theorem ProbabilityTheory.gaussianPDFReal_mul {μ : } {v : NNReal} {c : } (hc : c 0) (x : ) :
= |c⁻¹| * ProbabilityTheory.gaussianPDFReal (c⁻¹ * μ) ((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
• = if v = 0 then else MeasureTheory.volume.withDensity
Instances For
theorem ProbabilityTheory.gaussianReal_of_var_ne_zero (μ : ) {v : NNReal} (hv : v 0) :
= MeasureTheory.volume.withDensity
@[simp]
Equations
• =
theorem ProbabilityTheory.gaussianReal_apply (μ : ) {v : NNReal} (hv : v 0) (s : ) :
= ∫⁻ (x : ) in s,
theorem ProbabilityTheory.gaussianReal_apply_eq_integral (μ : ) {v : NNReal} (hv : v 0) (s : ) :
= ENNReal.ofReal (∫ (x : ) in s, )
theorem ProbabilityTheory.gaussianReal_absolutelyContinuous (μ : ) {v : NNReal} (hv : v 0) :
.AbsolutelyContinuous MeasureTheory.volume
theorem ProbabilityTheory.gaussianReal_absolutelyContinuous' (μ : ) {v : NNReal} (hv : v 0) :
MeasureTheory.volume.AbsolutelyContinuous
theorem ProbabilityTheory.rnDeriv_gaussianReal (μ : ) (v : NNReal) :
.rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume]
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 * μ) (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 * μ) (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 * μ) (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 * μ) (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.