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

• ProbabilityTheory.gaussianPDFReal μ v x = (√(2 * Real.pi * ↑v))⁻¹ * Real.exp (-(x - μ) ^ 2 / (2 * ↑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.

Equations

• ProbabilityTheory.gaussianPDF μ v x = ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal μ v x)

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

@[simp]

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

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

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.

Equations

• ProbabilityTheory.gaussianReal μ v = if v = 0 then MeasureTheory.Measure.dirac μ else MeasureTheory.volume.withDensity (ProbabilityTheory.gaussianPDF μ 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.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 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_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.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)

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