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 variancev
(whenv ≠ 0
).gaussianPDF
:ℝ≥0∞
-valued pdf,gaussianPDF μ v x = ENNReal.ofReal (gaussianPDFReal μ v x)
.gaussianReal
: a Gaussian measure onℝ
, parametrized by its meanμ
and variancev
. Ifv = 0
, this isdirac μ
, otherwise it is defined as the measure with densitygaussianPDF μ v
with respect to the Lebesgue measure.
Main results #
gaussianReal_add_const
: ifX
is a random variable with Gaussian distribution with meanμ
and variancev
, thenX + y
is Gaussian with meanμ + y
and variancev
.gaussianReal_const_mul
: ifX
is a random variable with Gaussian distribution with meanμ
and variancev
, thenc * X
is Gaussian with meanc * μ
and variancec^2 * v
.
The gaussian pdf is nonnegative.
The gaussian pdf is measurable.
The gaussian pdf is strongly measurable.
The gaussian distribution pdf integrates to 1 when the variance is not zero.
The gaussian distribution pdf integrates to 1 when the variance is not zero.
The pdf of a Gaussian distribution on ℝ with mean μ
and variance v
.
Equations
Instances For
A Gaussian distribution on ℝ
with mean μ
and variance v
.
Equations
Instances For
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.
The map of a Gaussian distribution by multiplication by a constant is a Gaussian.
The map of a Gaussian distribution by multiplication by a constant is a Gaussian.
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
.
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
.
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
.
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
.