ProbabilityTheory.gaussianReal_map_const_add
theorem ProbabilityTheory.gaussianReal_map_const_add :
∀ {μ : ℝ} {v : NNReal} (y : ℝ),
MeasureTheory.Measure.map (fun x => y + x) (ProbabilityTheory.gaussianReal μ v) =
ProbabilityTheory.gaussianReal (μ + y) v
This theorem states that the transformation of a Gaussian distribution by adding a constant is also a Gaussian distribution. Specifically, if you have a Gaussian distribution with mean `μ` and variance `v`, and you map this distribution by adding a constant `y` to each point in the distribution, the result is a new Gaussian distribution with mean `μ + y` and the same variance `v`. This holds true for any real numbers `μ` and `y` and any non-negative real number `v`.
More concisely: If `X` is a Gaussian distribution with mean `μ` and variance `v`, then the distribution of `X + y` is also Gaussian with mean `μ + y` and variance `v`.
|
ProbabilityTheory.gaussianReal_const_mul
theorem ProbabilityTheory.gaussianReal_const_mul :
∀ {μ : ℝ} {v : NNReal} {Ω : Type} [inst : MeasureTheory.MeasureSpace Ω] {X : Ω → ℝ},
MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v →
∀ (c : ℝ),
MeasureTheory.Measure.map (fun ω => c * X ω) MeasureTheory.volume =
ProbabilityTheory.gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
The theorem `ProbabilityTheory.gaussianReal_const_mul` states that if we have a real random variable `X` which follows a Gaussian distribution with mean `μ` and variance `v`, then if we multiply `X` by a constant `c`, the resulting random variable `c * X` also follows a Gaussian distribution, but with mean `c * μ` and variance `c^2 * v`. This implies that scaling a Gaussian random variable by a constant factor essentially scales its mean and variance by the same and the square of the factor respectively.
More concisely: If `X` is a real random variable following a Gaussian distribution with mean `μ` and variance `v`, then the random variable `c * X` follows a Gaussian distribution with mean `c * μ` and variance `c^2 * v`.
|
ProbabilityTheory.gaussianPDFReal_pos
theorem ProbabilityTheory.gaussianPDFReal_pos :
∀ (μ : ℝ) (v : NNReal) (x : ℝ), v ≠ 0 → 0 < ProbabilityTheory.gaussianPDFReal μ v x
The theorem states that the probability density function (PDF) of a Gaussian distribution is always positive when the variance is not zero. In other words, for any real number `μ`, non-negative real number `v`, and real number `x`, if `v` is not equal to zero, then the value of the Gaussian PDF, computed with mean `μ`, variance `v`, and for the input `x`, is strictly greater than zero.
More concisely: For any real numbers `μ` and `x`, and non-negative real number `v`, the Gaussian PDF with mean `μ`, variance `v` is strictly positive: `∀ μ ∈ ℝ, ∀ v ≥ 0, ∀ x ∈ ℝ, (normalDensity μ v x) > 0`.
|
ProbabilityTheory.gaussianReal_const_add
theorem ProbabilityTheory.gaussianReal_const_add :
∀ {μ : ℝ} {v : NNReal} {Ω : Type} [inst : MeasureTheory.MeasureSpace Ω] {X : Ω → ℝ},
MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v →
∀ (y : ℝ),
MeasureTheory.Measure.map (fun ω => y + X ω) MeasureTheory.volume =
ProbabilityTheory.gaussianReal (μ + y) v
This theorem states that if `X` is a real-valued random variable following a Gaussian distribution with mean `μ` and variance `v`, then the random variable `y + X` (which means adding a constant `y` to each possible outcome of `X`) also follows a Gaussian distribution, but with a mean of `μ + y` and the same variance `v`. In other words, adding a constant to a Gaussian random variable simply shifts the distribution without changing its shape or spread.
More concisely: If `X` is a real-valued random variable following a Gaussian distribution with mean `μ` and variance `v`, then adding a constant `y` to each outcome results in a new Gaussian distribution with mean `μ + y` and the same variance `v`.
|
ProbabilityTheory.gaussianReal_mul_const
theorem ProbabilityTheory.gaussianReal_mul_const :
∀ {μ : ℝ} {v : NNReal} {Ω : Type} [inst : MeasureTheory.MeasureSpace Ω] {X : Ω → ℝ},
MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v →
∀ (c : ℝ),
MeasureTheory.Measure.map (fun ω => X ω * c) MeasureTheory.volume =
ProbabilityTheory.gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
This theorem states that if `X` is a real-valued random variable that follows a Gaussian distribution with mean `μ` and variance `v`, then the random variable `X * c`, formed by multiplying `X` by a real constant `c`, also follows a Gaussian distribution, but with mean `c * μ` and variance `c^2 * v`. Here, `c` is any real number, `μ` is the original mean of the Gaussian distribution that `X` follows, and `v` is a nonnegative real number representing the original variance of the Gaussian distribution. The theorem essentially describes how scaling a Gaussian random variable affects its distribution.
More concisely: If `X` is a real-valued random variable following a Gaussian distribution with mean `μ` and variance `v`, then the random variable `X * c` has mean `c * μ` and variance `c^2 * v`.
|
ProbabilityTheory.gaussianReal_map_const_mul
theorem ProbabilityTheory.gaussianReal_map_const_mul :
∀ {μ : ℝ} {v : NNReal} (c : ℝ),
MeasureTheory.Measure.map (fun x => c * x) (ProbabilityTheory.gaussianReal μ v) =
ProbabilityTheory.gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
This theorem states that the map of a Gaussian distribution by multiplication by a constant results in a Gaussian distribution. Specifically, if we have a Gaussian distribution with mean `μ` and variance `v`, and we map this distribution by multiplying by a constant `c`, the result is a new Gaussian distribution. The mean of this new distribution is the original mean multiplied by `c`, and the variance is the original variance multiplied by `c` squared (where `c` squared is guaranteed to be a nonnegative real number). This theorem thus characterizes a property of Gaussian distributions under scaling transformations.
More concisely: If `X` is a Gaussian distribution with mean `μ` and variance `v`, then the distribution of `c * X` is a Gaussian with mean `μ * c` and variance `v * c^2`, where `c` is a nonnegative real number.
|
ProbabilityTheory.gaussianReal_zero_var
theorem ProbabilityTheory.gaussianReal_zero_var :
∀ (μ : ℝ), ProbabilityTheory.gaussianReal μ 0 = MeasureTheory.Measure.dirac μ
The theorem `ProbabilityTheory.gaussianReal_zero_var` states that for all real numbers `μ`, the Gaussian distribution with mean `μ` and variance `0` is equivalent to the dirac measure at `μ`. In other words, a Gaussian distribution with zero variance behaves like a point mass located at the mean. This is consistent with the principle that a zero-variance Gaussian distribution is a distribution where every point except the mean has almost zero probability.
More concisely: For all real numbers `μ`, the Gaussian distribution with mean `μ` and variance `0` is equal to the Dirac measure at `μ`.
|
ProbabilityTheory.lintegral_gaussianPDFReal_eq_one
theorem ProbabilityTheory.lintegral_gaussianPDFReal_eq_one :
∀ (μ : ℝ) {v : NNReal}, v ≠ 0 → ∫⁻ (x : ℝ), ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal μ v x) = 1
This theorem states that for any real number `μ` and any non-zero nonnegative real number `v`, the integral from negative infinity to positive infinity (i.e., the total area under the curve) of the probability density function (PDF) of the Gaussian distribution with mean `μ` and variance `v`, is equal to 1. This property is one of the key characteristics of a probability density function. In mathematical terms, this theorem asserts that for a Gaussian distribution $N(\mu, v)$, we have $\int_{-\infty}^{\infty} f(x) \, dx = 1,$ where $f(x)$ is the Gaussian PDF given by the formula $f(x) = \frac{1}{\sqrt{2\pi v}} e^{-(x - \mu)^2 / 2v}$.
More concisely: The integral of the Gaussian PDF with mean `μ` and variance `v` from `−∞` to `∞` equals `1`.
|
ProbabilityTheory.gaussianPDFReal_nonneg
theorem ProbabilityTheory.gaussianPDFReal_nonneg :
∀ (μ : ℝ) (v : NNReal) (x : ℝ), 0 ≤ ProbabilityTheory.gaussianPDFReal μ v x
This theorem states that the probability density function of the Gaussian distribution is always nonnegative. In other words, for any real number `μ` (the mean of the distribution), any nonnegative real number `v` (the variance of the distribution), and any real number `x`, the value of the Gaussian probability density function at `x` is greater than or equal to zero. This is consistent with the definition of a probability density function, as it should be nonnegative for all possible events (or values of `x`).
More concisely: The Gaussian probability density function, defined by `x => 1 / (sqrt(2 *. pi) *. v) *. exp (-. ((x - μ) ^ 2) / (2 *. v ^ 2)),` where `μ` is the mean and `v` is the variance, is nonnegative for all real numbers `x`, `μ`, and `v` (`v` nonnegative).
|
ProbabilityTheory.measurable_gaussianPDFReal
theorem ProbabilityTheory.measurable_gaussianPDFReal :
∀ (μ : ℝ) (v : NNReal), Measurable (ProbabilityTheory.gaussianPDFReal μ v)
The theorem `ProbabilityTheory.measurable_gaussianPDFReal` states that for any real number `μ` and any nonnegative real number `v`, the probability density function of the Gaussian distribution, defined with mean `μ` and variance `v`, is measurable. Here, a function is said to be measurable if the preimage of any measurable set is also a measurable set.
More concisely: The Gaussian distribution function with real mean μ and nonnegative variance v is a measurable function.
|
ProbabilityTheory.gaussianReal_add_const
theorem ProbabilityTheory.gaussianReal_add_const :
∀ {μ : ℝ} {v : NNReal} {Ω : Type} [inst : MeasureTheory.MeasureSpace Ω] {X : Ω → ℝ},
MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v →
∀ (y : ℝ),
MeasureTheory.Measure.map (fun ω => X ω + y) MeasureTheory.volume =
ProbabilityTheory.gaussianReal (μ + y) v
This theorem is about Gaussian distributions in probability theory. It states that given a real random variable `X` that follows a Gaussian distribution with mean `μ` and variance `v`, then the distribution of the random variable `X + y` is also a Gaussian distribution, but with a mean shifted by `y`, namely `μ + y`, and the same variance `v`. In other words, adding a constant `y` to a random variable doesn't change its variance but increases its mean by the same constant. This holds for any real number `y`.
More concisely: If `X` is a real random variable following a Gaussian distribution with mean `μ` and variance `v`, then the distribution of `X + y` is also Gaussian with mean `μ + y` and variance `v`.
|
ProbabilityTheory.integrable_gaussianPDFReal
theorem ProbabilityTheory.integrable_gaussianPDFReal :
∀ (μ : ℝ) (v : NNReal), MeasureTheory.Integrable (ProbabilityTheory.gaussianPDFReal μ v) MeasureTheory.volume := by
sorry
This theorem states that for any real number `μ` and any nonnegative real number `v`, the probability density function of the Gaussian distribution with mean `μ` and variance `v` is integrable with respect to the Lebesgue measure. In other words, the function is measurable and its Lebesgue integral over the whole real line is finite. This is a fundamental property of the Gaussian distribution, which ensures that its total probability mass equals 1 and that it is well-defined as a probability distribution.
More concisely: The Gaussian distribution with mean `μ` and variance `v` has an integrable probability density function with respect to the Lebesgue measure.
|
ProbabilityTheory.integral_gaussianPDFReal_eq_one
theorem ProbabilityTheory.integral_gaussianPDFReal_eq_one :
∀ (μ : ℝ) {v : NNReal}, v ≠ 0 → ∫ (x : ℝ), ProbabilityTheory.gaussianPDFReal μ v x = 1
The theorem `integral_gaussianPDFReal_eq_one` states that for any real number `μ` and any non-zero nonnegative real number `v`, the integral of the Gaussian probability density function (with mean `μ` and variance `v`) over all real numbers equals 1. In other words, when the variance of the Gaussian distribution is not zero, the total probability of all possible outcomes (when integrated over all real numbers) is 1. This is a standard property of probability density functions, which reflects that any possible outcome must occur with some probability, and the total probability across all outcomes must be 1.
More concisely: The integral of a Gaussian probability density function with mean μ and non-zero variance v over all real numbers equals 1.
|
ProbabilityTheory.stronglyMeasurable_gaussianPDFReal
theorem ProbabilityTheory.stronglyMeasurable_gaussianPDFReal :
∀ (μ : ℝ) (v : NNReal), MeasureTheory.StronglyMeasurable (ProbabilityTheory.gaussianPDFReal μ v)
The theorem `ProbabilityTheory.stronglyMeasurable_gaussianPDFReal` states that for all real numbers `μ` and for all nonnegative real numbers `v`, the probability density function of the Gaussian distribution with mean `μ` and variance `v` is strongly measurable. In other words, the Gaussian distribution's probability density function can be expressed as the limit of a sequence of simple functions. This is a fundamental property in measure theory and probability theory.
More concisely: The Gaussian distribution's probability density function with real mean μ and nonnegative variance v is a strongly measurable function.
|
ProbabilityTheory.gaussianReal_map_mul_const
theorem ProbabilityTheory.gaussianReal_map_mul_const :
∀ {μ : ℝ} {v : NNReal} (c : ℝ),
MeasureTheory.Measure.map (fun x => x * c) (ProbabilityTheory.gaussianReal μ v) =
ProbabilityTheory.gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
This theorem states that if you have a Gaussian distribution on the real numbers with mean `μ` and variance `v`, and if you apply a map to this distribution that multiplies every number by a constant `c`, you end up with a new Gaussian distribution. The mean of the new distribution will be the original mean multiplied by `c`, and the variance will be the original variance multiplied by the square of `c`. This theorem thus describes how Gaussian distributions change under scalar multiplication.
More concisely: If `X` is a Gaussian distributed random variable with mean `μ` and variance `v`, then the random variable `c * X` is also Gaussian distributed with mean `μ * c` and variance `v * c^2`.
|
ProbabilityTheory.gaussianReal_of_var_ne_zero
theorem ProbabilityTheory.gaussianReal_of_var_ne_zero :
∀ (μ : ℝ) {v : NNReal},
v ≠ 0 →
ProbabilityTheory.gaussianReal μ v = MeasureTheory.volume.withDensity (ProbabilityTheory.gaussianPDF μ v)
This theorem asserts that for any real number `μ` and any nonnegative real number `v` different from zero, the Gaussian distribution on real numbers with mean `μ` and variance `v` is equal to the measure that is obtained by applying the `withDensity` operation on the probability density function (pdf) of the Gaussian distribution with mean `μ` and variance `v`. In simpler terms, it shows that when the variance `v` is not zero, the Gaussian distribution is defined by the density function associated with that Gaussian distribution.
More concisely: For any real number `μ` and nonzero real number `v`, the Gaussian distribution with mean `μ` and variance `v` is equal to the measure obtained by applying `withDensity` to its probability density function.
|
ProbabilityTheory.gaussianReal_map_add_const
theorem ProbabilityTheory.gaussianReal_map_add_const :
∀ {μ : ℝ} {v : NNReal} (y : ℝ),
MeasureTheory.Measure.map (fun x => x + y) (ProbabilityTheory.gaussianReal μ v) =
ProbabilityTheory.gaussianReal (μ + y) v
This theorem states that mapping a Gaussian distribution by the addition of a constant results in another Gaussian distribution. Specifically, for any real numbers `μ` and `y`, and any nonnegative real number `v`, if we apply the operation `x => x + y` to a Gaussian distribution with mean `μ` and variance `v`, the resulting distribution is a Gaussian distribution with mean `μ + y` and the same variance `v`. This expresses in formal terms the property that adding a constant to all values in a Gaussian distribution simply shifts the mean of the distribution by that constant, without changing its shape or spread.
More concisely: The sum of a Gaussian distribution with mean `μ` and variance `v` and a constant `y` results in another Gaussian distribution with mean `μ + y` and the same variance `v`.
|