On this page

Linear forms of a standard Gaussian vector

GaussianAnalysis.comparison.gauss_linearlibrary/comparison/gauss_linear.v209 lines12 lemmas and theorems, 1 definitionsource

Imports 6 library modules and 29 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.finite_group.fingroup, mathcomp.finite_group.perm, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.interval, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.classical.cardinality, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.analysis.numfun, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.probability_theory.normal_distribution

Imported by 6

Required by 4 files of the paper proofs

For x of law gauss n and a nonzero row vector a, the inner product mxdot x a has law normal_prob 0 (frobenius a), the normal law with variance |a|^2 (gauss_mxdot). Integrals of functions of mxdot x a are integrals against that law (ge0_integral_gauss_mxdot, integral_gauss_mxdot). The moment generating function of mxdot x a is expR (t^2 |a|^2 / 2) for every a (integral_gauss_expR_mxdot), and its tails are those of the normal law (gauss_mxdot_upper_tail, gauss_mxdot_abs_tail).

row_tail a the row of the coordinates 1, ..., n of a : 'rV[R]_n.+1

Main results

Results	Statement	Used by `theories/`
gauss_mxdotge0_integral_gauss_mxdotintegral_gauss_mxdot	For `x` of law `gauss n` and `a != 0`, the linear form `mxdot x a` has law `normal_prob 0 (frobenius a)`, the normal law with variance `\|a\|^2`.
integral_gauss_expR_mxdotgauss_mxdot_upper_tailgauss_mxdot_abs_tail	`E[expR (t <x, a>)] = expR (t^2 \|a\|^2 / 2)`, and `P(\|<x, a>\| >= u) <= 2 expR (- u^2 / (2 \|a\|^2))`.	`Gaussian/Tail/UnitLinear`

Declarations13 exported

sectionnormal_prob_normr

Context {R : realType}.

lemma normal_pdf_normr source, line 43

forall {R : realType} (m s x : R), normal_pdf m `|s| x = normal_pdf m s x

Statement as written in the source

Lemma normal_pdf_normr (m s x : R) : normal_pdf m `|s| x = normal_pdf m s x.

Used by 1 declaration in 1 file

this file: normal_prob_normr

lemma normal_prob_normr source, line 49

forall {R : realType} (m s : R)
  (A : set
         (g_sigma_algebraType
            (R.-ocitv).-measurable)),
normal_prob m `|s| A = normal_prob m s A

Statement as written in the source

Lemma normal_prob_normr (m s : R) A : normal_prob m `|s| A = normal_prob m s A.

Used by 1 declaration in 1 file

this file: gauss_mxdot

sectionrow_tail

Context {R : realType} (n : nat).

definition row_tail source, line 58

Type

forall {R : realType} [n : nat], 'rV_n.+1 -> 'rV_n

Definition

Definition row_tail (a : 'rV[R]_n.+1) : 'rV[R]_n := \row_j a 0 (lift ord0 j).

The coordinates 1, ..., n of a row vector of size n.+1.

Used by 5 declarations in 2 files

this file: mxdot_rV_cons, mxdot_row_tail, gauss_mxdot
GaussianAnalysis.comparison.gauss_shift: rV_cons_row_tail, ge0_integral_gauss_shift

lemma mxdot_rV_cons source, line 60

forall {R : realType} [n : nat] (a : 'rV_n.+1) (t : measurableTypeR R) (v : 'rV_n),
mxdot (rV_cons (t, v)) a = t * a 0 ord0 + mxdot v (row_tail a)

Statement as written in the source

Lemma mxdot_rV_cons (a : 'rV[R]_n.+1) t (v : 'rV[R]_n) :
  mxdot (rV_cons (t, v)) a = t * a 0 ord0 + mxdot v (row_tail a).

Used by 2 declarations in 2 files

this file: gauss_mxdot
GaussianAnalysis.comparison.gauss_shift: ge0_integral_gauss_shift

lemma mxdot_row_tail source, line 67

forall {R : realType} [n : nat] (a : 'rV_n.+1),
mxdot a a = a 0 ord0 ^+ 2 + mxdot (row_tail a) (row_tail a)

Statement as written in the source

Lemma mxdot_row_tail (a : 'rV[R]_n.+1) :
  mxdot a a = a 0 ord0 ^+ 2 + mxdot (row_tail a) (row_tail a).

Used by 2 declarations in 2 files

this file: gauss_mxdot
GaussianAnalysis.comparison.gauss_shift: ge0_integral_gauss_shift

sectiongauss_mxdot

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

lemma measurable_mxdot source, line 80

forall {R : realType} [n : nat] (a : 'rV_n),
measurable_fun [set: 'rV_n] ((mxdot (n:=n))^~ a)

Statement as written in the source

Lemma measurable_mxdot n (a : 'rV[R]_n) :
  measurable_fun [set: 'rV[R]_n] (fun x => mxdot x a).

Used by 24 declarations in 6 files

this file: ge0_integral_gauss_mxdot, integrable_gauss_mxdot, integral_gauss_mxdot
GaussianAnalysis.comparison.gauss_shift: measurable_mxdotl
GaussianAnalysis.comparison.brascamp_lieb: gauss_ibp_unit, measurable_G, mline, dLambda_le0, Lambda_lip
GaussianAnalysis.comparison.brascamp_lieb_lebesgue: gauss_brascamp_lieb_ge0, gauss_brascamp_lieb, brascamp_lieb
GaussianAnalysis.fourier.charfun_rV: cf_rV_law, cf_rV_norm_le1, cf_rV_re_le1, cf_rV_im_le1, continuous_cf_rV_re, continuous_cf_rV_im, cf_rV_image, cf_rV_add, cf_rV_regularization, cf_rV_regularization_le
GaussianAnalysis.fourier.inversion: measurable_cf_rV_kernel, integral_cf_rV_kernel_gauss

theorem gauss_mxdot main result source, line 87

forall {R : realType} [n : nat] [a : 'rV_n] [A : set R],
a != 0 -> 'measurable A -> gauss n [set x | A (mxdot x a)] = normal_prob 0 (frobenius a) A

Main result, as the README states it

For x of law gauss n and a != 0, the linear form mxdot x a has law normal_prob 0 (frobenius a), the normal law with variance |a|^2.

Statement as written in the source

Theorem gauss_mxdot n (a : 'rV[R]_n) (A : set R) : a != 0 -> measurable A ->
  gauss n [set x | A (mxdot x a)] = normal_prob 0 (frobenius a) A.

Used by 5 declarations in 2 files

this file: ge0_integral_gauss_mxdot, integral_gauss_mxdot, gauss_mxdot_upper_tail, gauss_mxdot_abs_tail
GaussianAnalysis.fourier.charfun_rV: cf_rV_gauss

lemma ge0_integral_gauss_mxdot main result source, line 130

forall {R : realType} [n : nat] [a : 'rV_n] [f : R -> \bar R],
a != 0 ->
measurable_fun [set: R] f ->
(forall y : R, (0%R <= f y)%E) ->
(\int[gauss n]_x f (mxdot x a))%E = (\int[normal_prob 0 (frobenius a)]_y f y)%E

Main result

Stated in the README together with gauss_mxdot.

Statement as written in the source

Lemma ge0_integral_gauss_mxdot n (a : 'rV[R]_n) (f : R -> \bar R) : a != 0 ->
    measurable_fun [set: R] f -> (forall y, (0 <= f y)%E) ->
  (\int[gauss n]_x f (mxdot x a) = \int[normal_prob 0 (frobenius a)]_y f y)%E.

Used by 3 declarations in 2 files

this file: integrable_gauss_mxdot, integral_gauss_expR_mxdot
GaussianAnalysis.comparison.brascamp_lieb: Lambda_lip

lemma integrable_gauss_mxdot source, line 142

forall {R : realType} [n : nat] [a : 'rV_n] [f : R -> \bar R],
a != 0 ->
measurable_fun [set: R] f ->
(gauss n).-integrable [set: 'rV_n] (fun x : 'rV_n => f (mxdot x a)) <->
(normal_prob 0 (frobenius a)).-integrable [set: R] f

Statement as written in the source

Lemma integrable_gauss_mxdot n (a : 'rV[R]_n) (f : R -> \bar R) : a != 0 ->
    measurable_fun [set: R] f ->
  (gauss n).-integrable [set: 'rV[R]_n] (fun x => f (mxdot x a)) <->
  (normal_prob 0 (frobenius a)).-integrable [set: R] f.

Used by 1 declaration in 1 file

this file: integral_gauss_mxdot

lemma integral_gauss_mxdot main result source, line 157

forall {R : realType} [n : nat] [a : 'rV_n] [f : R -> \bar R],
a != 0 ->
(normal_prob 0 (frobenius a)).-integrable [set: R] f ->
(\int[gauss n]_x f (mxdot x a))%E = (\int[normal_prob 0 (frobenius a)]_y f y)%E

Main result

Stated in the README together with gauss_mxdot.

Statement as written in the source

Lemma integral_gauss_mxdot n (a : 'rV[R]_n) (f : R -> \bar R) : a != 0 ->
    (normal_prob 0 (frobenius a)).-integrable [set: R] f ->
  (\int[gauss n]_x f (mxdot x a) = \int[normal_prob 0 (frobenius a)]_y f y)%E.

theorem integral_gauss_expR_mxdot main result source, line 171

forall {R : realType} [n : nat] (a : 'rV_n) (t : R),
(\int[gauss n]_x (expR (t * mxdot x a))%:E)%E = (expR (t ^+ 2 * frobenius a ^+ 2 / 2))%:E

Main result, as the README states it

E[expR (t <x, a>)] = expR (t^2 |a|^2 / 2), and P(|<x, a>| >= u) <= 2 expR (- u^2 / (2 |a|^2)).

Used in theories/ by: Gaussian/Tail/UnitLinear

Statement as written in the source

Theorem integral_gauss_expR_mxdot n (a : 'rV[R]_n) t :
  (\int[gauss n]_x (expR (t * mxdot x a))%:E =
   (expR (t ^+ 2 * frobenius a ^+ 2 / 2))%:E)%E.

theorem gauss_mxdot_upper_tail main result source, line 184

forall {R : realType} [n : nat] [a : 'rV_n] [u : R],
a != 0 ->
0 <= u ->
(gauss n [set x | (u <= mxdot x a)%R] <= (expR (- u ^+ 2 / (2 * frobenius a ^+ 2)))%:E)%E

Main result

Stated in the README together with integral_gauss_expR_mxdot.

Statement as written in the source

Theorem gauss_mxdot_upper_tail n (a : 'rV[R]_n) (u : R) : a != 0 -> 0 <= u ->
  (gauss n [set x | u <= mxdot x a]%R <=
   (expR (- u ^+ 2 / (2 * frobenius a ^+ 2)))%:E)%E.

theorem gauss_mxdot_abs_tail main result source, line 194

forall {R : realType} [n : nat] [a : 'rV_n] [u : R],
a != 0 ->
0 <= u ->
(gauss n [set x | (u <= `|mxdot x a|)%R] <=
 (2 * expR (- u ^+ 2 / (2 * frobenius a ^+ 2)))%:E)%E

Main result

Stated in the README together with integral_gauss_expR_mxdot.

Statement as written in the source

Theorem gauss_mxdot_abs_tail n (a : 'rV[R]_n) (u : R) : a != 0 -> 0 <= u ->
  (gauss n [set x | u <= `|mxdot x a|]%R <=
   (2 * expR (- u ^+ 2 / (2 * frobenius a ^+ 2)))%:E)%E.

Used by 2 declarations in 1 file

GaussianAnalysis.random_matrix.goe_entries: goe_mx_diag_tail, goe_mx_offdiag_tail

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.