gaussian/

This directory builds Gaussian analysis on row vectors. It defines a measurable structure on matrices, the standard Gaussian measure gauss n and Lebesgue measure lebesgue_rV n on 'rV[R]_n, and proves the calculus the rest of the library relies on: Fubini, marginals, moments, Gaussian integration by parts and interpolation.

It starts from MathComp-Analysis's normal law normal_prob m s and its product measures. A matrix carries the sigma-algebra generated by its entries, and gauss n and lebesgue_rV n are built one coordinate at a time. Vectors are rows and matrices act on the right: if x has law gauss n, then x *m A has covariance A^T *m A.

Conventions: |x| is MathComp's norm, the largest absolute value of an entry; frobenius (matrix/euclidean.v) is the Euclidean norm. Polynomial growth means |F x| <= C (1 + |x|^k) everywhere. The partial derivative d_i F is the derivative along delta_mx 0 i.

Reading order

1. measurable_matrix.v: the sigma-algebra of matrices, uniqueness of measures from boxes, and the max-entry norm.
2. normal_integral.v: integrals against normal_prob m s through its density, and integrability of polynomially growing functions against normal_prob 0 1.
3. parameter_integral.v: continuity of an integral depending on a parameter in a pseudometric space.
4. gauss.v: the measure gauss n, boxes, Fubini, permutations, blocks and coordinates.
5. gauss_ibp.v: Stein's identity and Gaussian integration by parts of orders one and two.
6. gauss_moments.v: moments of the normal law, and covariances under gauss n.
7. partial_derivative.v: continuous partial derivatives imply differentiability.
8. gauss_interpolation.v: Gaussian interpolation along a path of matrices, and Kahane's comparison inequality.
9. lebesgue_rV.v: Lebesgue measure on 'rV[R]_n, its invariances, the density of gauss n and the volume of balls.

Core definitions

• mxbox (measurable_matrix.v): the matrices M with M i j in A i j for all i, j. The boxes with measurable sides, mxboxes, generate the sigma-algebra.
• rV_cons (gauss.v): the vector of size n.+1 with first coordinate p.1, followed by the coordinates of p.2.
• gauss (gauss.v): the standard Gaussian probability on 'rV[R]_n, by recursion on n: gauss n.+1 is the image of normal_prob 0 1 \x gauss n under rV_cons (gaussS).
• lebesgue_rV (lebesgue_rV.v): Lebesgue measure on 'rV[R]_n, a sigma-finite measure built as gauss is (lebesgue_rV_rec).
• gauss_pdf (lebesgue_rV.v): (2 pi)^(-n/2) exp (- mxdot x x / 2), the density of gauss n against lebesgue_rV n.

Main results

Matrices.

• measurable_fun_mxP: a map into matrices is measurable if and only if each entry is. continuous_measurable_mx: a continuous real function of a matrix is measurable.
• measure_rowbox_unique, measure_mxbox_unique: two measures on row vectors, or on matrices, that agree on the boxes with measurable sides, the first of finite mass, agree on all measurable sets.

The normal law and gauss n.

• integral_normal_prob: the integral of an integrable f against normal_prob m s is the Lebesgue integral of f normal_pdf m s. integrable_gauss_poly: measurable functions of polynomial growth are integrable against gauss n.
• gauss_box, gauss_unique: the box with measurable sides A i has measure \prod_i normal_prob 0 1 (A i), and this characterizes gauss n. integral_gauss_cons is Fubini for the first coordinate.
• gauss_row_mx, gauss_lsubmx, gauss_col_perm, gauss_coord: gauss (n + m) is the image of gauss n \x gauss m under row_mx and its first block has law gauss n; gauss n is invariant under permutations of the coordinates, and each coordinate has law normal_prob 0 1.
• gauss_cov, gauss_mulmx_cov, normal_moment_even: E[x_i x_j] is 1 if i = j and 0 otherwise, E[(x A)_j (x A)_l] = (A^T A)_(j, l), and E[X^(2k)] = 1 * 3 * ... * (2k - 1) for X of law normal_prob 0 1.

Integration by parts.

• normal_ibp: E[X f(X)] = E[f'(X)] for X of law normal_prob 0 1, when f has the derivative f' everywhere, f' is continuous, and f and f' have polynomial growth.
• gauss_ibp: E[x_i F(x)] = E[dF(x)] under gauss n, when dF is the derivative of F along delta_mx 0 i everywhere, and F and dF are continuous and of polynomial growth. gauss_ibp_line only needs F and dF measurable and dF continuous along the lines parallel to the i-th axis.
• gauss_ibp2: E[(x_i^2 - 1) F(x)] = E[d2F(x)] for F measurable with derivatives dF and d2F along delta_mx 0 i, d2F continuous, all three of polynomial growth; dF need not be continuous.

Interpolation. Here x has law gauss n, F : 'rV[R]_k -> R and its partial derivatives d_j F are differentiable, the d_l d_j F are continuous, and all are bounded by one C (1 + |z|^p).

• gauss_interpolation: if M has the derivative M' on an open interval, with |M s| <= K and |M' s| <= K there, then on that interval the derivative of t |-> E[F(x *m M t)] is \sum_(j, l) ((M' t)^T *m M t)_(j, l) E[d_l d_j F(x *m M t)].
• gauss_comparison: Kahane's inequality. If \sum_(j, l) (A^T A - B^T B)_(j, l) d_l d_j F z <= 0 for every z, then E[F(x *m A)] <= E[F(y *m B)] for y of law gauss m.

Lebesgue measure.

• lebesgue_rV_box, lebesgue_rV_unique: a box with measurable sides A i has measure \prod_i lebesgue_measure (A i), and this characterizes lebesgue_rV n.
• lebesgue_rV_shift, lebesgue_rV_col_perm, lebesgue_rV_scale: invariance under translations and permutations, and the factor |a|^-n for preimages under x |-> a x, a nonzero.
• integral_gauss_pdf: E[f(x)] = \int f(x) gauss_pdf x dx against lebesgue_rV n, for f integrable against gauss n.
• lebesgue_rV_ball_le: for r > 0, the closed ball [set x | frobenius (x - z) <= r] has measure at most (sqrt (2 pi e / n) r)^n.

How the proofs go

• gauss_unique follows from measure_rowbox_unique and gauss_box: the boxes generate the sigma-algebra and are closed under intersection.
• normal_ibp integrates (f phi)' over [-(n+1), n+1], phi the normal density; the boundary terms tend to 0. gauss_ibp_line moves coordinate i first by a transposition and applies normal_ibp to it inside Fubini; gauss_ibp2 applies gauss_ibp_line to dF and to x_i F.
• gauss_comparison applies gauss_interpolation to the path col_mx (cos t *: A) (sin t *: B) on [0, pi / 2], whose ends give x *m A and y *m B, x and y the two blocks of a vector of law gauss (n + m).

Connections

• Requires MathComp and MathComp-Analysis. Only lebesgue_rV.v requires other directories: matrix/euclidean.v and comparison/normal_linear.v.
• Every other library directory requires it. comparison/ builds its comparison inequalities on gauss_interpolation.v; fourier/, random_matrix/, probability/, matrix/ and convex/ require gauss.v or measurable_matrix.v. In applications/, the matrix series, GOE edge, SK gap and perceptron targets require gauss.v. theories/ and extension/ use it too.