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

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

@[simp]

theorem ProbabilityTheory.gaussianPdfReal_zero_var (m : ℝ) : ProbabilityTheory.gaussianPdfReal m 0 = 0

theorem ProbabilityTheory.gaussianPdfReal_pos (μ : ℝ) (v : NNReal) (x : ℝ) (hv : v ≠ 0) : 0 < ProbabilityTheory.gaussianPdfReal μ v x

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

theorem ProbabilityTheory.gaussianPdfReal_nonneg (μ : ℝ) (v : NNReal) (x : ℝ) : 0 ≤ ProbabilityTheory.gaussianPdfReal μ v x

The gaussian pdf is nonnegative.

theorem ProbabilityTheory.measurable_gaussianPdfReal (μ : ℝ) (v : NNReal) : Measurable (ProbabilityTheory.gaussianPdfReal μ v)

The gaussian pdf is measurable.

theorem ProbabilityTheory.stronglyMeasurable_gaussianPdfReal (μ : ℝ) (v : NNReal) : MeasureTheory.StronglyMeasurable (ProbabilityTheory.gaussianPdfReal μ v)

The gaussian pdf is strongly measurable.

theorem ProbabilityTheory.integrable_gaussianPdfReal (μ : ℝ) (v : NNReal) : MeasureTheory.Integrable (ProbabilityTheory.gaussianPdfReal μ v)

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

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

theorem ProbabilityTheory.gaussianPdfReal_inv_mul {μ : ℝ} {v : NNReal} {c : ℝ} (hc : c ≠ 0) (x : ℝ) : ProbabilityTheory.gaussianPdfReal μ v (c⁻¹ * 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 : ℝ) : ProbabilityTheory.gaussianPdfReal μ v (c * x) = |c⁻¹| * ProbabilityTheory.gaussianPdfReal (c⁻¹ * μ) ({ val := (c ^ 2)⁻¹, property := (_ : 0 ≤ (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) : ProbabilityTheory.gaussianPdf μ v = fun (x : ℝ) => ENNReal.ofReal (ProbabilityTheory.gaussianPdfReal μ v x)

@[simp]

theorem ProbabilityTheory.gaussianPdf_zero_var (μ : ℝ) : ProbabilityTheory.gaussianPdf μ 0 = 0

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

theorem ProbabilityTheory.measurable_gaussianPdf (μ : ℝ) (v : NNReal) : Measurable (ProbabilityTheory.gaussianPdf μ v)

@[simp]

theorem ProbabilityTheory.lintegral_gaussianPdf_eq_one (μ : ℝ) {v : NNReal} (h : v ≠ 0) : ∫⁻ (x : ℝ), ProbabilityTheory.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.Measure.withDensity MeasureTheory.volume (ProbabilityTheory.gaussianPdf μ v)

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

@[simp]

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

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

Equations

• (_ : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.gaussianReal μ v)) = (_ : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.gaussianReal μ v))

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

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

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

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

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