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.

theorem ProbabilityTheory.gaussianPDFReal_def (μ : ℝ) (v : NNReal) : gaussianPDFReal μ v = fun (x : ℝ) => (√(2 * Real.pi * ↑v))⁻¹ * Real.exp (-(x - μ) ^ 2 / (2 * ↑v))

@[simp]

theorem ProbabilityTheory.gaussianPDFReal_zero_var (m : ℝ) : gaussianPDFReal m 0 = 0

theorem ProbabilityTheory.gaussianPDFReal_pos (μ : ℝ) (v : NNReal) (x : ℝ) (hv : v ≠ 0) : 0 < gaussianPDFReal μ v x

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

theorem ProbabilityTheory.gaussianPDFReal_nonneg (μ : ℝ) (v : NNReal) (x : ℝ) : 0 ≤ gaussianPDFReal μ v x

The gaussian pdf is nonnegative.

theorem ProbabilityTheory.measurable_gaussianPDFReal (μ : ℝ) (v : NNReal) : Measurable (gaussianPDFReal μ v)

The gaussian pdf is measurable.

theorem ProbabilityTheory.stronglyMeasurable_gaussianPDFReal (μ : ℝ) (v : NNReal) : MeasureTheory.StronglyMeasurable (gaussianPDFReal μ v)

The gaussian pdf is strongly measurable.

theorem ProbabilityTheory.integrable_gaussianPDFReal (μ : ℝ) (v : NNReal) : MeasureTheory.Integrable (gaussianPDFReal μ v) MeasureTheory.volume

theorem ProbabilityTheory.lintegral_gaussianPDFReal_eq_one (μ : ℝ) {v : NNReal} (h : v ≠ 0) : ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v 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 : ℝ), gaussianPDFReal μ v x = 1

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

theorem ProbabilityTheory.gaussianPDFReal_sub {μ : ℝ} {v : NNReal} (x y : ℝ) : gaussianPDFReal μ v (x - y) = gaussianPDFReal (μ + y) v x

theorem ProbabilityTheory.gaussianPDFReal_add {μ : ℝ} {v : NNReal} (x y : ℝ) : gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x

theorem ProbabilityTheory.gaussianPDFReal_inv_mul {μ : ℝ} {v : NNReal} {c : ℝ} (hc : c ≠ 0) (x : ℝ) : gaussianPDFReal μ v (c⁻¹ * x) = |c| * gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x

theorem ProbabilityTheory.gaussianPDFReal_mul {μ : ℝ} {v : NNReal} {c : ℝ} (hc : c ≠ 0) (x : ℝ) : gaussianPDFReal μ v (c * x) = |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨(c ^ 2)⁻¹, ⋯⟩ * v) x

noncomputable def ProbabilityTheory.gaussianPDF (μ : ℝ) (v : NNReal) (x : ℝ) : ENNReal

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

theorem ProbabilityTheory.gaussianPDF_def (μ : ℝ) (v : NNReal) : gaussianPDF μ v = fun (x : ℝ) => ENNReal.ofReal (gaussianPDFReal μ v x)

@[simp]

theorem ProbabilityTheory.gaussianPDF_zero_var (μ : ℝ) : gaussianPDF μ 0 = 0

@[simp]

theorem ProbabilityTheory.toReal_gaussianPDF {μ : ℝ} {v : NNReal} (x : ℝ) : (gaussianPDF μ v x).toReal = gaussianPDFReal μ v x

theorem ProbabilityTheory.gaussianPDF_pos (μ : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : 0 < gaussianPDF μ v x

theorem ProbabilityTheory.gaussianPDF_lt_top {μ : ℝ} {v : NNReal} {x : ℝ} : gaussianPDF μ v x < ⊤

theorem ProbabilityTheory.gaussianPDF_ne_top {μ : ℝ} {v : NNReal} {x : ℝ} : gaussianPDF μ v x ≠ ⊤

@[simp]

theorem ProbabilityTheory.support_gaussianPDF {μ : ℝ} {v : NNReal} (hv : v ≠ 0) : Function.support (gaussianPDF μ v) = Set.univ

theorem ProbabilityTheory.measurable_gaussianPDF (μ : ℝ) (v : NNReal) : Measurable (gaussianPDF μ v)

@[simp]

theorem ProbabilityTheory.lintegral_gaussianPDF_eq_one (μ : ℝ) {v : NNReal} (h : v ≠ 0) : ∫⁻ (x : ℝ), gaussianPDF μ v x = 1

noncomputable def ProbabilityTheory.gaussianReal (μ : ℝ) (v : NNReal) : MeasureTheory.Measure ℝ

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

theorem ProbabilityTheory.gaussianReal_of_var_ne_zero (μ : ℝ) {v : NNReal} (hv : v ≠ 0) : gaussianReal μ v = MeasureTheory.volume.withDensity (gaussianPDF μ v)

@[simp]

theorem ProbabilityTheory.gaussianReal_zero_var (μ : ℝ) : gaussianReal μ 0 = MeasureTheory.Measure.dirac μ

instance ProbabilityTheory.instIsProbabilityMeasureGaussianReal (μ : ℝ) (v : NNReal) : MeasureTheory.IsProbabilityMeasure (gaussianReal μ v)

theorem ProbabilityTheory.noAtoms_gaussianReal {μ : ℝ} {v : NNReal} (h : v ≠ 0) : MeasureTheory.NoAtoms (gaussianReal μ v)

theorem ProbabilityTheory.gaussianReal_apply (μ : ℝ) {v : NNReal} (hv : v ≠ 0) (s : Set ℝ) : (gaussianReal μ v) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x

theorem ProbabilityTheory.gaussianReal_apply_eq_integral (μ : ℝ) {v : NNReal} (hv : v ≠ 0) (s : Set ℝ) : (gaussianReal μ v) s = ENNReal.ofReal (∫ (x : ℝ) in s, gaussianPDFReal μ v x)

theorem ProbabilityTheory.gaussianReal_absolutelyContinuous (μ : ℝ) {v : NNReal} (hv : v ≠ 0) : (gaussianReal μ v).AbsolutelyContinuous MeasureTheory.volume

theorem ProbabilityTheory.gaussianReal_absolutelyContinuous' (μ : ℝ) {v : NNReal} (hv : v ≠ 0) : MeasureTheory.volume.AbsolutelyContinuous (gaussianReal μ v)

theorem ProbabilityTheory.rnDeriv_gaussianReal (μ : ℝ) (v : NNReal) : (gaussianReal μ v).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] gaussianPDF μ v

theorem ProbabilityTheory.integral_gaussianReal_eq_integral_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : ℝ} {v : NNReal} {f : ℝ → E} (hv : v ≠ 0) : ∫ (x : ℝ), f x ∂gaussianReal μ v = ∫ (x : ℝ), gaussianPDFReal μ v x • f x

theorem MeasurableEmbedding.gaussianReal_comap_apply {μ : ℝ} {v : NNReal} (hv : v ≠ 0) {f : ℝ → ℝ} (hf : MeasurableEmbedding f) {f' : ℝ → ℝ} (h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x) {s : Set ℝ} (hs : MeasurableSet s) : (MeasureTheory.Measure.comap f (ProbabilityTheory.gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * ProbabilityTheory.gaussianPDFReal μ v (f x))

theorem MeasurableEquiv.gaussianReal_map_symm_apply {μ : ℝ} {v : NNReal} (hv : v ≠ 0) (f : ℝ ≃ᵐ ℝ) {f' : ℝ → ℝ} (h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x) {s : Set ℝ} (hs : MeasurableSet s) : (MeasureTheory.Measure.map (⇑f.symm) (ProbabilityTheory.gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * ProbabilityTheory.gaussianPDFReal μ v (f x))

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

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

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

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) (gaussianReal μ v) = 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) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

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

theorem ProbabilityTheory.gaussianReal_map_neg {μ : ℝ} {v : NNReal} : MeasureTheory.Measure.map (fun (x : ℝ) => -x) (gaussianReal μ v) = gaussianReal (-μ) v

theorem ProbabilityTheory.gaussianReal_map_sub_const {μ : ℝ} {v : NNReal} (y : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => x - y) (gaussianReal μ v) = gaussianReal (μ - y) v

theorem ProbabilityTheory.gaussianReal_map_const_sub {μ : ℝ} {v : NNReal} (y : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => y - x) (gaussianReal μ v) = gaussianReal (y - μ) v

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

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} [MeasureTheory.MeasureSpace Ω] {X : Ω → ℝ} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = gaussianReal μ v) (y : ℝ) : MeasureTheory.Measure.map (fun (ω : Ω) => y + X ω) MeasureTheory.volume = gaussianReal (μ + y) v

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} [MeasureTheory.MeasureSpace Ω] {X : Ω → ℝ} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = gaussianReal μ v) (c : ℝ) : MeasureTheory.Measure.map (fun (ω : Ω) => c * X ω) MeasureTheory.volume = 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} [MeasureTheory.MeasureSpace Ω] {X : Ω → ℝ} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = gaussianReal μ v) (c : ℝ) : MeasureTheory.Measure.map (fun (ω : Ω) => X ω * c) MeasureTheory.volume = 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.

theorem ProbabilityTheory.complexMGF_id_gaussianReal {μ : ℝ} {v : NNReal} (z : ℂ) : complexMGF id (gaussianReal μ v) z = Complex.exp (z * ↑μ + ↑↑v * z ^ 2 / 2)

The complex moment generating function of a Gaussian distribution with mean μ and variance v is given by z ↦ exp (z * μ + v * z ^ 2 / 2).

theorem ProbabilityTheory.complexMGF_gaussianReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {p : MeasureTheory.Measure Ω} {μ : ℝ} {v : NNReal} {X : Ω → ℝ} (hX : MeasureTheory.Measure.map X p = gaussianReal μ v) (z : ℂ) : complexMGF X p z = Complex.exp (z * ↑μ + ↑↑v * z ^ 2 / 2)

The complex moment generating function of a random variable with Gaussian distribution with mean μ and variance v is given by z ↦ exp (z * μ + v * z ^ 2 / 2).

theorem ProbabilityTheory.charFun_gaussianReal {μ : ℝ} {v : NNReal} (t : ℝ) : MeasureTheory.charFun (gaussianReal μ v) t = Complex.exp (↑t * ↑μ * Complex.I - ↑↑v * ↑t ^ 2 / 2)

The characteristic function of a Gaussian distribution with mean μ and variance v is given by t ↦ exp (t * μ - v * t ^ 2 / 2).

theorem ProbabilityTheory.mgf_gaussianReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {p : MeasureTheory.Measure Ω} {μ : ℝ} {v : NNReal} {X : Ω → ℝ} (hX : MeasureTheory.Measure.map X p = gaussianReal μ v) (t : ℝ) : mgf X p t = Real.exp (μ * t + ↑v * t ^ 2 / 2)

The moment generating function of a random variable with Gaussian distribution with mean μ and variance v is given by t ↦ exp (μ * t + v * t ^ 2 / 2).

theorem ProbabilityTheory.mgf_fun_id_gaussianReal {μ : ℝ} {v : NNReal} : mgf (fun (x : ℝ) => x) (gaussianReal μ v) = fun (t : ℝ) => Real.exp (μ * t + ↑v * t ^ 2 / 2)

theorem ProbabilityTheory.mgf_id_gaussianReal {μ : ℝ} {v : NNReal} : mgf id (gaussianReal μ v) = fun (t : ℝ) => Real.exp (μ * t + ↑v * t ^ 2 / 2)

theorem ProbabilityTheory.cgf_gaussianReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {p : MeasureTheory.Measure Ω} {μ : ℝ} {v : NNReal} {X : Ω → ℝ} (hX : MeasureTheory.Measure.map X p = gaussianReal μ v) (t : ℝ) : cgf X p t = μ * t + ↑v * t ^ 2 / 2

The cumulant generating function of a random variable with Gaussian distribution with mean μ and variance v is given by t ↦ μ * t + v * t ^ 2 / 2.

theorem ProbabilityTheory.integrable_exp_mul_gaussianReal {μ : ℝ} {v : NNReal} (t : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (gaussianReal μ v)

@[simp]

theorem ProbabilityTheory.integrableExpSet_id_gaussianReal {μ : ℝ} {v : NNReal} : integrableExpSet id (gaussianReal μ v) = Set.univ

@[simp]

theorem ProbabilityTheory.integrableExpSet_fun_id_gaussianReal {μ : ℝ} {v : NNReal} : integrableExpSet (fun (x : ℝ) => x) (gaussianReal μ v) = Set.univ

@[simp]

theorem ProbabilityTheory.integral_id_gaussianReal {μ : ℝ} {v : NNReal} : ∫ (x : ℝ), x ∂gaussianReal μ v = μ

The mean of a real Gaussian distribution gaussianReal μ v is its mean parameter μ.

@[simp]

theorem ProbabilityTheory.variance_fun_id_gaussianReal {μ : ℝ} {v : NNReal} : variance (fun (x : ℝ) => x) (gaussianReal μ v) = ↑v

The variance of a real Gaussian distribution gaussianReal μ v is its variance parameter v.

@[simp]

theorem ProbabilityTheory.variance_id_gaussianReal {μ : ℝ} {v : NNReal} : variance id (gaussianReal μ v) = ↑v

The variance of a real Gaussian distribution gaussianReal μ v is its variance parameter v.

theorem ProbabilityTheory.memLp_id_gaussianReal {μ : ℝ} {v : NNReal} (p : NNReal) : MeasureTheory.MemLp id (↑p) (gaussianReal μ v)

All the moments of a real Gaussian distribution are finite. That is, the identity is in Lp for all finite p.

theorem ProbabilityTheory.memLp_id_gaussianReal' {μ : ℝ} {v : NNReal} (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp id p (gaussianReal μ v)

All the moments of a real Gaussian distribution are finite. That is, the identity is in Lp for all finite p.

theorem ProbabilityTheory.gaussianReal_map_linearMap {μ : ℝ} {v : NNReal} (L : ℝ →ₗ[ℝ] ℝ) : MeasureTheory.Measure.map (⇑L) (gaussianReal μ v) = gaussianReal (L μ) ((L 1 ^ 2).toNNReal * v)

theorem ProbabilityTheory.gaussianReal_map_continuousLinearMap {μ : ℝ} {v : NNReal} (L : ℝ →L[ℝ] ℝ) : MeasureTheory.Measure.map (⇑L) (gaussianReal μ v) = gaussianReal (L μ) ((L 1 ^ 2).toNNReal * v)

@[simp]

theorem ProbabilityTheory.integral_linearMap_gaussianReal {μ : ℝ} {v : NNReal} (L : ℝ →ₗ[ℝ] ℝ) : ∫ (x : ℝ), L x ∂gaussianReal μ v = L μ

@[simp]

theorem ProbabilityTheory.integral_continuousLinearMap_gaussianReal {μ : ℝ} {v : NNReal} (L : ℝ →L[ℝ] ℝ) : ∫ (x : ℝ), L x ∂gaussianReal μ v = L μ

@[simp]

theorem ProbabilityTheory.variance_linearMap_gaussianReal {μ : ℝ} {v : NNReal} (L : ℝ →ₗ[ℝ] ℝ) : variance (⇑L) (gaussianReal μ v) = ↑(L 1 ^ 2).toNNReal * ↑v

@[simp]

theorem ProbabilityTheory.variance_continuousLinearMap_gaussianReal {μ : ℝ} {v : NNReal} (L : ℝ →L[ℝ] ℝ) : variance (⇑L) (gaussianReal μ v) = ↑(L 1 ^ 2).toNNReal * ↑v

theorem ProbabilityTheory.gaussianReal_conv_gaussianReal {m₁ m₂ : ℝ} {v₁ v₂ : NNReal} : (gaussianReal m₁ v₁).conv (gaussianReal m₂ v₂) = gaussianReal (m₁ + m₂) (v₁ + v₂)

The convolution of two real Gaussian distributions with means m₁, m₂ and variances v₁, v₂ is a real Gaussian distribution with mean m₁ + m₂ and variance v₁ + v₂.

theorem ProbabilityTheory.gaussianReal_add_gaussianReal_of_indepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {m₁ m₂ : ℝ} {v₁ v₂ : NNReal} {X Y : Ω → ℝ} (hXY : IndepFun X Y P) (hX : MeasureTheory.Measure.map X P = gaussianReal m₁ v₁) (hY : MeasureTheory.Measure.map Y P = gaussianReal m₂ v₂) : MeasureTheory.Measure.map (X + Y) P = gaussianReal (m₁ + m₂) (v₁ + v₂)