Documentation

TauCeti.Probability.Distributions.Gaussian.Transforms

Moment- and cumulant-generating functions of Gaussian linear functionals #

This file proves that every almost everywhere measurable continuous linear functional of a Gaussian measure has finite exponential moments of every real order and computes its moment-generating function. It then specializes the general result to inner products against a multivariate Gaussian vector, expressing the variance as the covariance-matrix quadratic form, and computes the corresponding cumulant-generating function.

The general results require no norm on the source space. Almost everywhere measurability of the functional suffices; the default proof handles continuous functionals when open sets are measurable, including sigma algebras larger than the Borel sigma algebra.

Main results #

References #

source
theorem ProbabilityTheory.IsGaussian.integrableExpSet_dual {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] (L : StrongDual ℝ E) (hL : AEMeasurable (⇑L) μ := by fun_prop) :
integrableExpSet (⇑L) μ = Set.univ

An almost everywhere measurable continuous linear functional of a Gaussian measure has finite exponential moments of every real order.

source
theorem ProbabilityTheory.IsGaussian.mgf_dual {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] (L : StrongDual ℝ E) (t : ℝ) (hL : AEMeasurable (⇑L) μ := by fun_prop) :
mgf (⇑L) μ t = Real.exp (t * ∫ (x : E), L x ∂μ + t ^ 2 / 2 * variance (⇑L) μ)

The moment-generating function of an almost everywhere measurable continuous linear functional of a Gaussian measure is determined by its mean and variance.

source
theorem ProbabilityTheory.IsGaussian.lintegral_ofReal_exp_mul_dual {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] (L : StrongDual ℝ E) (t : ℝ) (hL : AEMeasurable (⇑L) μ := by fun_prop) :
∫⁻ (y : E), ENNReal.ofReal (Real.exp (t * L y)) ∂μ = ENNReal.ofReal (Real.exp (t * ∫ (x : E), L x ∂μ + t ^ 2 / 2 * variance (⇑L) μ))

The exponential moment of an almost everywhere measurable continuous linear functional of a Gaussian measure as a nonnegative integral: ∫⁻ exp (t L) dμ = exp (t μ[L] + t² / 2 · Var[L; μ]).

source
theorem TauCeti.Probability.gaussian_exp_integral (a : ℝ) :
∫ (x : ℝ), Real.exp (a * x) ∂ProbabilityTheory.gaussianReal 0 1 = Real.exp (a ^ 2 / 2)

The exponential moment of the standard Gaussian.

source
theorem TauCeti.Probability.gaussian_x_exp_integral (a : ℝ) :
∫ (x : ℝ), x * Real.exp (a * x) ∂ProbabilityTheory.gaussianReal 0 1 = a * Real.exp (a ^ 2 / 2)

The first exponentially tilted moment of the standard Gaussian.

source
theorem TauCeti.Probability.gaussian_x_exp_integrable (a : ℝ) :
MeasureTheory.Integrable (fun (x : ℝ) => x * Real.exp (a * x)) (ProbabilityTheory.gaussianReal 0 1)

The first exponentially tilted moment of the standard Gaussian is integrable.

source
theorem TauCeti.Probability.integral_exp_nat_mul_sin_gaussianReal (n : ℕ) :
∫ (y : ℝ), Real.exp (↑n * y) * Real.sin (2 * Real.pi * y) ∂ProbabilityTheory.gaussianReal 0 1 = 0

The sine at frequency 2π is orthogonal under the standard Gaussian law to every exponential with a natural-number exponent.

source
theorem TauCeti.Probability.integral_cos_gaussianReal (t : ℝ) :
∫ (y : ℝ), Real.cos (t * y) ∂ProbabilityTheory.gaussianReal 0 1 = Real.exp (-t ^ 2 / 2)

The cosine transform of the standard Gaussian is exp (-t² / 2).

source
theorem TauCeti.Probability.integrableExpSet_inner_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m θ : EuclideanSpace ℝ ι) (S : Matrix ι ι ℝ) :
ProbabilityTheory.integrableExpSet (fun (x : EuclideanSpace ℝ ι) => inner ℝ θ x) (ProbabilityTheory.multivariateGaussian m S) = Set.univ

Every directional linear functional of a multivariate Gaussian has finite exponential moments of all real orders.

This remains true for a covariance matrix that is not positive semidefinite: Mathlib then totalizes the multivariate Gaussian to a Dirac measure at its mean.

source
@[simp]
theorem TauCeti.Probability.map_inner_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m q : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ} (hS : S.PosSemidef) :
MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ ι) => inner ℝ q x) (ProbabilityTheory.multivariateGaussian m S) = ProbabilityTheory.gaussianReal (inner ℝ q m) (inner ℝ q ((Matrix.toEuclideanLin S) q)).toNNReal

A real linear projection of a multivariate Gaussian has the corresponding directional mean and covariance quadratic form as its scalar Gaussian parameters.

source
theorem TauCeti.Probability.mgf_inner_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m θ : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (t : ℝ) :
ProbabilityTheory.mgf (fun (x : EuclideanSpace ℝ ι) => inner ℝ θ x) (ProbabilityTheory.multivariateGaussian m S) t = Real.exp (t * inner ℝ θ m + t ^ 2 / 2 * inner ℝ θ ((Matrix.toEuclideanLin S) θ))

The moment-generating function of the inner product against a multivariate Gaussian vector.

The exponent consists of the directional mean and one half of the covariance quadratic form, scaled respectively by t and t².

source
@[simp]
theorem TauCeti.Probability.cgf_inner_multivariateGaussian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m θ : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ} (hS : S.PosSemidef) (t : ℝ) :
ProbabilityTheory.cgf (fun (x : EuclideanSpace ℝ ι) => inner ℝ θ x) (ProbabilityTheory.multivariateGaussian m S) t = t * inner ℝ θ m + t ^ 2 / 2 * inner ℝ θ ((Matrix.toEuclideanLin S) θ)

The cumulant-generating function of an inner product against a multivariate Gaussian vector is the quadratic polynomial determined by its directional mean and variance.

The formula holds for every real order, including for singular positive-semidefinite covariance matrices.