On this page

Moments of the standard Gaussian measures

GaussianAnalysis.gaussian.gauss_momentslibrary/gaussian/gauss_moments.v162 lines7 lemmas and theoremssource

Imports 4 library modules and 21 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.arithmetic_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.algebra.interval, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.derive, mathcomp.analysis.realfun, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability

Imported by 5

Required by 3 files of the paper proofs

The moments of the standard normal law follow from Stein's identity: E[X^(k+2)] = (k + 1) E[X^k] (normal_momentS), so the odd moments vanish and E[X^(2k)] = 1 * 3 * ... * (2k - 1) (normal_moment_odd, normal_moment_even). A vector x of law gauss n has mean 0 and covariance the identity (gauss_mean, gauss_cov), and x *m A has covariance A^T *m A (gauss_mulmx_cov).

Main results

Results	Statement
normal_momentSnormal_moment_oddnormal_moment_even	Moments of the standard normal law: `E[X^(k+2)] = (k + 1) E[X^k]`, so the odd moments vanish and `E[X^(2k)] = 1 * 3 * ... * (2k - 1)`.
gauss_meangauss_covgauss_mulmx_cov	A vector `x` of law `gauss n` has mean 0 and covariance the identity, and `x m A` has covariance `A^T m A`.

Declarations7 exported, 1 local

sectionnormal_moments

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).

let integrable_normal_exprnr section-local source, line 36

Let integrable_normal_exprnr k : N.-integrable [set: R] (fun x => (x ^+ k)%:E).

lemma normal_momentS main result source, line 43

forall {R : realType} (k : nat),
(\int[normal_prob 0 1]_x (x ^+ k.+2)%:E)%E =
((k.+1%:R)%:E * \int[normal_prob 0 1]_x (x ^+ k)%:E)%E

Main result, as the README states it

Moments of the standard normal law: E[X^(k+2)] = (k + 1) E[X^k], so the odd moments vanish and E[X^(2k)] = 1 * 3 * ... * (2k - 1).

Statement as written in the source

Lemma normal_momentS k :
  (\int[N]_x (x ^+ k.+2)%:E = k.+1%:R%:E * \int[N]_x (x ^+ k)%:E)%E.

Used by 2 declarations in 1 file

this file: normal_moment_odd, normal_moment_even

lemma normal_mean source, line 67

forall {R : realType}, (\int[normal_prob 0 1]_x x%:E)%E = 0

Statement as written in the source

Lemma normal_mean : (\int[N]_x x%:E = 0)%E.

Used by 3 declarations in 2 files

this file: normal_moment_odd, gauss_mean
GaussianAnalysis.probability.rademacher_lindeberg: Rintegral_normal_quadratic

lemma normal_moment_odd main result source, line 79

forall {R : realType} (k : nat), (\int[normal_prob 0 1]_x (x ^+ k.*2.+1)%:E)%E = 0

Main result

Stated in the README together with normal_momentS.

Statement as written in the source

Lemma normal_moment_odd k : (\int[N]_x (x ^+ k.*2.+1)%:E = 0)%E.

lemma normal_moment_even main result source, line 87

forall {R : realType} (k : nat),
(\int[normal_prob 0 1]_x (x ^+ k.*2)%:E)%E = (\prod_(i < k) i.*2.+1%:R)%:E

Main result

Stated in the README together with normal_momentS.

Statement as written in the source

Lemma normal_moment_even k :
  (\int[N]_x (x ^+ k.*2)%:E = (\prod_(i < k) i.*2.+1%:R)%:E)%E.

Used by 3 declarations in 2 files

GaussianAnalysis.probability.rademacher_lindeberg: Rintegral_normal_quadratic, Rintegral_normal_abs3
GaussianAnalysis.convex.gauss_feature: gauss_coord_moments

sectiongauss_moments

Context {R : realType}.

lemma gauss_mean main result source, line 102

forall {R : realType} [n : nat] (i : 'I_n), (\int[gauss n]_x (x 0 i)%:E)%E = 0

Main result, as the README states it

A vector x of law gauss n has mean 0 and covariance the identity, and x *m A has covariance A^T *m A.

Statement as written in the source

Lemma gauss_mean n (i : 'I_n) : (\int[gauss n]_x (x 0 i)%:E = 0 :> \bar R)%E.

Used by 1 declaration in 1 file

GaussianAnalysis.convex.gauss_feature: gauss_mxdot_moments

lemma gauss_cov main result source, line 111

forall {R : realType} [n : nat] (i j : 'I_n),
(\int[gauss n]_x (x 0 i * x 0 j)%:E)%E = ((i == j)%:R)%:E

Main result

Stated in the README together with gauss_mean.

Statement as written in the source

Lemma gauss_cov n (i j : 'I_n) :
  (\int[gauss n]_x (x 0 i * x 0 j)%:E = (i == j)%:R%:E :> \bar R)%E.

Used by 5 declarations in 4 files

this file: gauss_mulmx_cov
GaussianAnalysis.comparison.escape: gauss_frobenius_mean_le, gauss_sqr_mulmx
GaussianAnalysis.convex.gauss_feature: gauss_diag_moments
GaussianAnalysis.fourier.charfun_rV: integral_gauss_mxdot_self

lemma gauss_mulmx_cov main result source, line 134

forall {R : realType} [n k : nat] (A : 'M_(n, k)) (j l : 'I_k),
(\int[gauss n]_x ((x *m A) 0 j * (x *m A) 0 l)%:E)%E = ((A^T *m A) j l)%:E

Main result

Stated in the README together with gauss_mean.

Statement as written in the source

Lemma gauss_mulmx_cov n k (A : 'M[R]_(n, k)) (j l : 'I_k) :
  (\int[gauss n]_x ((x *m A) 0 j * (x *m A) 0 l)%:E = ((A^T *m A) j l)%:E)%E.

Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.