On this page
Gaussian matrices from Gaussian rows
Imports 4 library modules and 16 external
- GaussianAnalysis.gaussian.measurable_matrix
- GaussianAnalysis.gaussian.gauss
- GaussianAnalysis.probability.lindeberg
- GaussianAnalysis.probability.conditioning
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability
A Gaussian matrix of size n x m is vec_mx a for a of law gauss (n * m), as in escape.v and cgmt.v. This file identifies two other descriptions of its law.
- gauss_tuple_mx: n independent rows of law gauss m, put in a matrix by tuple_mx, give the same law: for X measurable, tuple_prod (fun=> gauss m) n (tuple_mx @^-1` X) is gauss (n * m) [set a | X (vec_mx a)].
- gauss_trmx: the transpose of a Gaussian matrix of size n x m is a Gaussian matrix of size m x n.
Both follow from gauss_unique: the coordinates are permuted, and the laws agree on boxes by gauss_box and tuple_prod_box.
tuple_ | the n x m matrix whose rows are the vectors of t |
Main results
| Results | Statement |
|---|---|
Two descriptions of the law of an n x m matrix vec_mx a of independent standard normal entries (a of law gauss (n * m)): the matrix tuple_mx t of n independent rows of law gauss m has this law, tuple_prod (fun=> gauss m) n (tuple_mx @^-1` X) = gauss (n * m) [set a | X (vec_mx a)], and so has the transpose of an m x n such matrix, gauss (n * m) [set a | X (vec_mx a)^T] = gauss (m * n) [set b | X (vec_mx b)]. Both by gauss_unique on boxes. |
Declarations7 exported, 2 local
Context {R : realType}. Local Notation N := (@normal_prob R 0 1).
forall {R : realType} [n m : nat], n.-tuple 'rV_m -> 'M_(n, m)Definition tuple_mx n m (t : n.-tuple 'rV[R]_m) : 'M[R]_(n, m) := \matrix_(i, j) tnth t i 0 j.
The n x m matrix whose rows are the vectors of a tuple.
Used by 2 declarations in 1 file
- this file: measurable_tuple_mx, gauss_tuple_mx
forall {R : realType} [n m : nat], measurable_fun [set: n.-tuple _] (tuple_mx (m:=m))
Statement as written in the source
Lemma measurable_tuple_mx n m : measurable_fun setT (@tuple_mx n m).
Used by 1 declaration in 1 file
- this file: gauss_tuple_mx
forall {R : realType} [n m : nat], measurable_fun [set: 'rV_(n * m)] vec_mx
Statement as written in the source
Lemma measurable_vec_mx n m : measurable_fun setT (@vec_mx R n m).
Used by 2 declarations in 1 file
- this file: gauss_tuple_mx, gauss_trmx
forall {R : realType} [n m : nat], measurable_fun [set: 'M_(n, m)] mxvec
Statement as written in the source
Lemma measurable_mxvec n m : measurable_fun setT (@mxvec R n m).
Used by 2 declarations in 1 file
- this file: gauss_tuple_mx, gauss_trmx
Let unvec_ix n m (k : 'I_(n * m)) : 'I_n * 'I_m := enum_val (cast_ord (esym (mxvec_cast n m)) k).
The inverse of mxvec_index.
Used by 2 declarations in 1 file
- this file: unvec_ixK, gauss_trmx
Let unvec_ixK n m (i : 'I_n) (j : 'I_m) : unvec_ix (mxvec_index i j) = (i, j).
Used by 1 declaration in 1 file
- this file: gauss_trmx
forall {R : realType} [n m : nat] (F : 'I_(n * m) -> \bar R), (\prod_(k < n * m) F k)%E = (\prod_(i < n) \prod_(j < m) F (mxvec_index i j))%E
A product over the indices mxvec_index i j is a double product.
Statement as written in the source
Lemma prod_mxvec n m (F : 'I_(n * m) -> \bar R) : (\prod_(k < n * m) F k = \prod_(i < n) \prod_(j < m) F (mxvec_index i j))%E.
Used by 2 declarations in 1 file
- this file: gauss_tuple_mx, gauss_trmx
forall {R : realType} [n m : nat] [X : set 'M_(n, m)], (measure_matrix_display default_measure_display).-measurable X -> tuple_prod (fun=> gauss m) n (tuple_mx (m:=m) @^-1` X) = gauss (n * m) [set a | X (vec_mx a)]
n independent Gaussian rows form a Gaussian matrix.
Two descriptions of the law of an n x m matrix vec_mx a of independent standard normal entries (a of law gauss (n * m)): the matrix tuple_mx t of n independent rows of law gauss m has this law, tuple_prod (fun=> gauss m) n (tuple_mx @^-1` X) = gauss (n * m) [set a | X (vec_mx a)], and so has the transpose of an m x n such matrix, gauss (n * m) [set a | X (vec_mx a)^T] = gauss (m * n) [set b | X (vec_mx b)]. Both by gauss_unique on boxes.
Statement as written in the source
Theorem gauss_tuple_mx n m (X : set 'M[R]_(n, m)) : measurable X -> tuple_prod (fun=> gauss m) n (@tuple_mx n m @^-1` X) = gauss (n * m) [set a | X (vec_mx a)].
forall {R : realType} [n m : nat] [X : set 'M_(m, n)], (measure_matrix_display default_measure_display).-measurable X -> gauss (n * m) [set a | X (vec_mx a)^T] = gauss (m * n) [set b | X (vec_mx b)]
The transpose of a Gaussian matrix is a Gaussian matrix.
Stated in the README together with gauss_tuple_mx.