On this page

The law of a linear image of a Gaussian vector

GaussianAnalysis.comparison.gauss_lawlibrary/comparison/gauss_law.v661 lines22 lemmas and theorems, 1 definitionsource

Imports 9 library modules and 28 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.matrix, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic, 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.sequences, mathcomp.analysis.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.numfun, 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 9 files of the paper proofs

For x of law gauss n and A an n x k matrix, x *m A is a centered Gaussian vector with covariance A^T *m A. Its law depends only on that covariance: if A^T *m A = B^T *m B, with B an m x k matrix, then gauss n [set x | X (x *m A)] = gauss m [set y | X (y *m B)] for every measurable set X of 'rV[R]_k (gauss_mulmx_law). When the columns of A are orthonormal, x *m A has law gauss k (gauss_orthogonal_law); in particular gauss n is invariant under every orthogonal matrix. The integral forms are ge0_integral_gauss_mulmx and integral_gauss_orthogonal.

The proof goes through test functions. Kahane's comparison inequality, applied in both directions, gives equal expectations to every test of class C^2 with polynomially bounded derivatives (gauss_law_smooth). A bounded Lipschitz function G is the uniform limit of its double Gaussian smoothings gauss_smooth t (gauss_smooth t G), which are of class C^2 because Gaussian integration by parts moves the derivative inside the second smoothing (gauss_smooth_partial_stein); hence the expectations of G agree too (gauss_law_lipschitz). Finally a finite measure on 'rV[R]_k is determined by the integrals of the Lipschitz functions with values in [0, 1] (measure_lipschitz_unique): the sets {Phi > 0}, for Phi nonnegative and Lipschitz, are closed under intersection, generate the Borel sets (measurable_lipschitz_pos), and their indicators are nondecreasing limits of min 1 (i Phi).

lipschitz_pos the sets [set x | 0 < Phi x], for Phi : 'rV[R]_k -> R nonnegative and Lipschitz for the Euclidean norm

Main results

Results	Statement	Used by `theories/`
gauss_mulmx_lawintegral_gauss_mulmx	The law of a centered Gaussian vector depends only on its covariance: for `x` of law `gauss n` and `y` of law `gauss m`, if `A^T m A = B^T m B`, then `P(x m A \in X) = P(y m B \in X)` for every measurable set `X` of `'rV[R]_k`, and `E[f (x m A)] = E[f (y m B)]` for every measurable `f`.	`Gaussian/Orthogonal/EqualCovariance`
gauss_orthogonal_lawintegral_gauss_orthogonalge0_integral_gauss_mulmx	If the columns of `A` are orthonormal, `x *m A` has law `gauss k`; in particular `gauss n` is invariant under every orthogonal matrix. Forms with integrals.	`Projected/BulkLaw`
gauss_law_smoothgauss_law_lipschitz	Gaussian vectors `x m A` and `y m B` with `A^T m A = B^T m B` give the same expectation to every test of class C^2 with polynomially bounded derivatives (Kahane's inequality in both directions), and to every bounded Lipschitz function.
measure_lipschitz_uniquemeasurable_lipschitz_pos	A finite measure on `'rV[R]_k` is determined by the integrals of the Lipschitz functions with values in `[0, 1]`; the sets `{Phi > 0}`, for `Phi` nonnegative and Lipschitz, generate the Borel sets.
gauss_smooth_partial_steingauss_smooth_partial_boundedgauss_smooth_partial_lipschitz	For `G` bounded and Lipschitz, the partial derivatives of `gauss_smooth eps G` are bounded and Lipschitz, and smoothing them again equals differentiating the double smoothing.

Declarations23 exported, 22 local

sectionaffine_derive

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

lemma is_derive_affine_comp source, line 61

forall {R : realType} {n : nat} [F : 'rV_n -> R] [x y : 'rV_n] 
  [c d : R] [j : 'I_n],
is_derive (x + c *: y) (delta_mx 0 j) F d ->
is_derive y (delta_mx 0 j)
  (fun y0 : 'rV[R]_n => F (x + c *: y0))
  (c * d)

The derivative of y |-> F (x + c y) along a coordinate.

Statement as written in the source

Lemma is_derive_affine_comp (F : 'rV[R]_n -> R) (x y : 'rV[R]_n) (c d : R) j :
  is_derive (x + c *: y) (delta_mx 0 j) F d ->
  is_derive y (delta_mx 0 j) (fun y => F (x + c *: y)) (c * d).

Used by 1 declaration in 1 file

this file: gauss_smooth_partial_stein

The partial derivatives of the Gaussian smoothing of a bounded Lipschitz function are bounded and Lipschitz.

sectionsmooth_partial

Context {R : realType} {n : nat}.
Variables (G : 'rV[R]_n -> R) (K L eps : R).
Hypothesis GK : forall x, `|G x| <= K.
Hypothesis GL : forall x y, `|G x - G y| <= L * frobenius (x - y).
Hypothesis eps0 : 0 < eps.

let K0 section-local source, line 91

Let K0 : 0 <= K := le_trans (normr_ge0 _) (GK 0).

let mG section-local source, line 92

Let mG : measurable_fun [set: 'rV[R]_n] G :=
  continuous_measurable_mx (lipschitz_frobenius_continuous GL).

Used by 1 declaration in 1 file

this file: mGc

let iF section-local source, line 94

Let iF := @integrable_gauss_frobenius R n.

Used by 2 declarations in 1 file

this file: gauss_smooth_partial_bounded, gauss_smooth_partial_lipschitz

let mGc section-local source, line 96

Let mGc x j : measurable_fun [set: 'rV[R]_n] (fun y => G (x + eps *: y) * y 0 j).

Used by 1 declaration in 1 file

this file: iGc

let iGc section-local source, line 103

Let iGc x j :
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o (fun y => G (x + eps *: y) * y 0 j)).

Used by 2 declarations in 1 file

this file: gauss_smooth_partial_bounded, gauss_smooth_partial_lipschitz

lemma gauss_smooth_partial_bounded main result source, line 112

forall {R : realType} {n : nat} [G : 'rV_n -> R] [K L eps : R],
(forall x : 'rV_n, `|G x| <= K) ->
(forall x y : 'rV_n, `|G x - G y| <= L * frobenius (x - y)) ->
0 < eps ->
forall (j : 'I_n) (x : 'rV_n),
`|gauss_smooth_partial eps G j x| <= eps^-1 * K * \int[gauss n]_y frobenius (y : 'rV_n)

Main result

Stated in the README together with gauss_smooth_partial_stein.

Statement as written in the source

Lemma gauss_smooth_partial_bounded j x :
  `|gauss_smooth_partial eps G j x| <=
  eps^-1 * K * \int[gauss n]_y frobenius (y : 'rV[R]_n).

Used by 2 declarations in 1 file

this file: FjK, D2H_poly

lemma gauss_smooth_partial_lipschitz main result source, line 128

forall {R : realType} {n : nat} [G : 'rV_n -> R] [K L eps : R],
(forall x : 'rV_n, `|G x| <= K) ->
(forall x y : 'rV_n, `|G x - G y| <= L * frobenius (x - y)) ->
0 < eps ->
forall (j : 'I_n) (x x' : 'rV_n),
`|gauss_smooth_partial eps G j x - gauss_smooth_partial eps G j x'| <=
eps^-1 * L * \int[gauss n]_y frobenius (y : 'rV_n) * frobenius (x - x')

Main result

Stated in the README together with gauss_smooth_partial_stein.

Statement as written in the source

Lemma gauss_smooth_partial_lipschitz j x x' :
  `|gauss_smooth_partial eps G j x - gauss_smooth_partial eps G j x'| <=
  eps^-1 * L * \int[gauss n]_y frobenius (y : 'rV[R]_n) * frobenius (x - x').

Used by 1 declaration in 1 file

this file: FjL

Gaussian vectors with the same covariance give the same expectation to a test of class C^2 whose derivatives grow at most polynomially: Kahane's comparison inequality holds in both directions.

sectiongauss_law_smooth

Context {R : realType} {k : nat}.
Variables (F : 'rV[R]_k -> R) (DF : 'I_k -> 'rV[R]_k -> R)
  (D2F : 'I_k -> 'I_k -> 'rV[R]_k -> R).
Hypothesis F_partial : forall j z, is_derive z (delta_mx 0 j) F (DF j z).
Hypothesis DF_partial : forall j l z, is_derive z (delta_mx 0 l) (DF j) (D2F j l z).
Hypothesis D2F_cont : forall j l, continuous (D2F j l).
Variables (C : R) (p : nat).
Hypothesis F_poly : forall z, `|F z| <= C * (1 + `|z| ^+ p).
Hypothesis DF_poly : forall j z, `|DF j z| <= C * (1 + `|z| ^+ p).
Hypothesis D2F_poly : forall j l z, `|D2F j l z| <= C * (1 + `|z| ^+ p).

theorem gauss_law_smooth main result source, line 175

forall {R : realType} {k : nat} [F : 'rV_k -> R] [DF : 'I_k -> 'rV_k -> R]
  [D2F : 'I_k -> 'I_k -> 'rV_k -> R],
(forall (j : 'I_k)
   (z : 'rV[R]_k),
 is_derive z (delta_mx 0 j) F (DF j z)) ->
(forall (j : 'I_k) (l : 'I_k)
   (z : 'rV[R]_k),
 is_derive z (delta_mx 0 l) (DF j) (D2F j l z)) ->
(forall j l : 'I_k, continuous (D2F j l)) ->
forall [C : R] [p : nat],
(forall z : 'rV_k, `|F z| <= C * (1 + `|z| ^+ p)) ->
(forall (j : 'I_k) (z : 'rV_k), `|DF j z| <= C * (1 + `|z| ^+ p)) ->
(forall (j l : 'I_k) (z : 'rV_k), `|D2F j l z| <= C * (1 + `|z| ^+ p)) ->
forall [n m : nat] [A : 'M_(n, k)] [B : 'M_(m, k)],
A^T *m A = B^T *m B ->
(\int[gauss n]_x (F (x *m A))%:E)%E = (\int[gauss m]_y (F (y *m B))%:E)%E

Main result, as the README states it

Gaussian vectors x *m A and y *m B with A^T *m A = B^T *m B give the same expectation to every test of class C^2 with polynomially bounded derivatives (Kahane's inequality in both directions), and to every bounded Lipschitz function.

Statement as written in the source

Theorem gauss_law_smooth n m (A : 'M[R]_(n, k)) (B : 'M[R]_(m, k)) :
  A^T *m A = B^T *m B ->
  (\int[gauss n]_x (F (x *m A))%:E = \int[gauss m]_y (F (y *m B))%:E)%E.

Used by 1 declaration in 1 file

this file: gauss_law_double_smooth

The double smoothing gauss_smooth delta (gauss_smooth eps G) of a bounded Lipschitz function G is of class C^2, with bounded derivatives.

sectiondouble_smooth

Context {R : realType} {k : nat}.
Variables (G : 'rV[R]_k -> R) (K L eps delta : R).
Hypothesis GK : forall x, `|G x| <= K.
Hypothesis GL : forall x y, `|G x - G y| <= L * frobenius (x - y).
Hypothesis eps0 : 0 < eps.
Hypothesis delta0 : 0 < delta.
Local Notation Ey := (\int[gauss k]_y frobenius (y : 'rV[R]_k)).
Local Notation F := (gauss_smooth eps G).
Local Notation Fj j := (gauss_smooth_partial eps G j).

let FK section-local source, line 207

Let FK x : `|F x| <= K := gauss_smooth_bounded eps GK GL x.

Used by 3 declarations in 1 file

this file: gauss_smooth_partial_stein, H_partial, H_poly

let FL section-local source, line 208

Let FL x y : `|F x - F y| <= L * frobenius (x - y) :=
  gauss_smooth_lipschitz eps GK GL x y.

Used by 3 declarations in 1 file

this file: gauss_smooth_partial_stein, H_partial, H_poly

let FjK section-local source, line 210

Let FjK j x : `|Fj j x| <= eps^-1 * K * Ey :=
  gauss_smooth_partial_bounded GK GL eps0 j x.

Used by 5 declarations in 1 file

this file: gauss_smooth_partial_stein, DH_partial, D2H_cont, DH_poly, D2H_poly

let FjL section-local source, line 212

Let FjL j x y : `|Fj j x - Fj j y| <= eps^-1 * L * Ey * frobenius (x - y) :=
  gauss_smooth_partial_lipschitz GK GL eps0 j x y.

Used by 5 declarations in 1 file

this file: gauss_smooth_partial_stein, DH_partial, D2H_cont, DH_poly, D2H_poly

let Fd section-local source, line 214

Let Fd x j : is_derive x (delta_mx 0 j) F (Fj j x) := gauss_smooth_derive GK GL eps0 x j.

Used by 1 declaration in 1 file

this file: gauss_smooth_partial_stein

let K0 section-local source, line 216

Let K0 : 0 <= K := le_trans (normr_ge0 _) (GK 0).

let Ey0 section-local source, line 217

Let Ey0 : 0 <= Ey.

let Kj0 section-local source, line 219

Let Kj0 : 0 <= eps^-1 * K * Ey.

lemma gauss_smooth_partial_stein main result source, line 223

forall {R : realType} {k : nat} [G : 'rV_k -> R] [K L eps delta : R],
(forall x : 'rV_k, `|G x| <= K) ->
(forall x y : 'rV_k, `|G x - G y| <= L * frobenius (x - y)) ->
0 < eps ->
0 < delta ->
forall (j : 'I_k) (x : 'rV_k),
gauss_smooth_partial delta (gauss_smooth eps G) j x =
gauss_smooth delta (gauss_smooth_partial eps G j) x

Gaussian integration by parts swaps the smoothing and the derivative.

Main result, as the README states it

For G bounded and Lipschitz, the partial derivatives of gauss_smooth eps G are bounded and Lipschitz, and smoothing them again equals differentiating the double smoothing.

Statement as written in the source

Lemma gauss_smooth_partial_stein j x :
  gauss_smooth_partial delta F j x = gauss_smooth delta (Fj j) x.

Used by 1 declaration in 1 file

this file: H_partial

Local Notation H := (gauss_smooth delta F).

let H_partial section-local source, line 270

Let H_partial j z : is_derive z (delta_mx 0 j) H (gauss_smooth delta (Fj j) z).

Used by 1 declaration in 1 file

this file: gauss_law_double_smooth

let DH_partial section-local source, line 275

Let DH_partial j l z : is_derive z (delta_mx 0 l) (gauss_smooth delta (Fj j))
  (gauss_smooth_partial delta (Fj j) l z).

Used by 1 declaration in 1 file

this file: gauss_law_double_smooth

let D2H_cont section-local source, line 279

Let D2H_cont j l : continuous (gauss_smooth_partial delta (Fj j) l).

Used by 1 declaration in 1 file

this file: gauss_law_double_smooth

let Kjj0 section-local source, line 282

Let Kjj0 : 0 <= delta^-1 * (eps^-1 * K * Ey) * Ey.

let C section-local source, line 285

Let C := K + eps^-1 * K * Ey + delta^-1 * (eps^-1 * K * Ey) * Ey.

Used by 4 declarations in 1 file

this file: Cb, H_poly, DH_poly, D2H_poly

let Cb section-local source, line 287

Let Cb c (z : 'rV[R]_k) : c <= C -> c <= C * (1 + `|z| ^+ 0).

Used by 3 declarations in 1 file

this file: H_poly, DH_poly, D2H_poly

let H_poly section-local source, line 293

Let H_poly z : `|H z| <= C * (1 + `|z| ^+ 0).

Used by 1 declaration in 1 file

this file: gauss_law_double_smooth

let DH_poly section-local source, line 299

Let DH_poly j z : `|gauss_smooth delta (Fj j) z| <= C * (1 + `|z| ^+ 0).

Used by 1 declaration in 1 file

this file: gauss_law_double_smooth

let D2H_poly section-local source, line 305

Let D2H_poly j l z :
  `|gauss_smooth_partial delta (Fj j) l z| <= C * (1 + `|z| ^+ 0).

Used by 1 declaration in 1 file

this file: gauss_law_double_smooth

lemma gauss_law_double_smooth source, line 314

forall {R : realType} {k : nat} [G : 'rV_k -> R] [K L eps delta : R],
(forall x : 'rV_k, `|G x| <= K) ->
(forall x y : 'rV_k, `|G x - G y| <= L * frobenius (x - y)) ->
0 < eps ->
0 < delta ->
forall [n m : nat] [A : 'M_(n, k)] [B : 'M_(m, k)],
A^T *m A = B^T *m B ->
\int[gauss n]_x gauss_smooth delta (gauss_smooth eps G) (x *m A) =
\int[gauss m]_y gauss_smooth delta (gauss_smooth eps G) (y *m B)

The double smoothing of G has the same expectation under two Gaussian vectors with the same covariance.

Statement as written in the source

Lemma gauss_law_double_smooth n m (A : 'M[R]_(n, k)) (B : 'M[R]_(m, k)) :
  A^T *m A = B^T *m B ->
  \int[gauss n]_x H (x *m A) = \int[gauss m]_y H (y *m B).

Used by 1 declaration in 1 file

this file: gauss_law_lipschitz

sectiongauss_law_lipschitz

Context {R : realType}.

lemma normr_Rintegral_gauss_le source, line 327

forall {R : realType} [n : nat] [f : 'rV_n -> R] [c : R],
measurable_fun [set: 'rV_n] f ->
(forall x : 'rV_n, `|f x| <= c) -> `|\int[gauss n]_x f x| <= c

Statement as written in the source

Lemma normr_Rintegral_gauss_le n (f : 'rV[R]_n -> R) (c : R) :
  measurable_fun [set: 'rV[R]_n] f -> (forall x, `|f x| <= c) ->
  `|\int[gauss n]_x f x| <= c.

Used by 1 declaration in 1 file

this file: gauss_law_lipschitz

lemma lipschitz_frobenius_mulmx source, line 341

forall {R : realType} [n k : nat] [f : 'rV_k -> R] [L : R] (A : 'M_(n, k)),
(forall x y : 'rV_k, `|f x - f y| <= L * frobenius (x - y)) ->
forall x y : 'rV_n, `|f (x *m A) - f (y *m A)| <= `|L| * frobenius A * frobenius (x - y)

Statement as written in the source

Lemma lipschitz_frobenius_mulmx n k (f : 'rV[R]_k -> R) (L : R) (A : 'M[R]_(n, k)) :
  (forall x y, `|f x - f y| <= L * frobenius (x - y)) ->
  forall x y : 'rV[R]_n,
    `|f (x *m A) - f (y *m A)| <= `|L| * frobenius A * frobenius (x - y).

theorem gauss_law_lipschitz main result source, line 353

forall {R : realType} [n m k : nat] [A : 'M_(n, k)] [B : 'M_(m, k)] 
  [G : 'rV_k -> R] [K L : R],
(forall x : 'rV_k, `|G x| <= K) ->
(forall x y : 'rV_k, `|G x - G y| <= L * frobenius (x - y)) ->
A^T *m A = B^T *m B -> \int[gauss n]_x G (x *m A) = \int[gauss m]_y G (y *m B)

Gaussian vectors with the same covariance give the same expectation to every bounded Lipschitz function.

Main result

Stated in the README together with gauss_law_smooth.

Statement as written in the source

Theorem gauss_law_lipschitz n m k (A : 'M[R]_(n, k)) (B : 'M[R]_(m, k))
    (G : 'rV[R]_k -> R) (K L : R) :
  (forall x, `|G x| <= K) -> (forall x y, `|G x - G y| <= L * frobenius (x - y)) ->
  A^T *m A = B^T *m B ->
  \int[gauss n]_x G (x *m A) = \int[gauss m]_y G (y *m B).

Used by 1 declaration in 1 file

this file: gauss_mulmx_law

A finite measure on row vectors is determined by the integrals of the Lipschitz functions with values in [0, 1]. The sets {Phi > 0}, for Phi nonnegative and Lipschitz, are closed under intersection and generate the Borel sets; the indicator of {Phi > 0} is the nondecreasing limit of min 1 (i Phi).

sectionlipschitz_unique

Context {R : realType} {k : nat}.

definition lipschitz_pos source, line 420

Type

forall {R : realType} {k : nat}, set (set 'rV_k)

Definition

Definition lipschitz_pos : set (set 'rV[R]_k) :=
  [set [set x | 0 < Phi x] | Phi in [set Phi : 'rV[R]_k -> R |
    (forall x, 0 <= Phi x) /\
    exists L, forall x y, `|Phi x - Phi y| <= L * frobenius (x - y)]].

Used by 5 declarations in 1 file

this file: setI_closed_lipschitz_pos, lipschitz_pos_setT, measurable_lipschitz_pos, lipschitz_pos_agree, measure_lipschitz_unique

lemma minr_dist source, line 425

forall {R : realType} (a b c d : R), `|minr a b - minr c d| <= `|a - c| + `|b - d|

Statement as written in the source

Lemma minr_dist (a b c d : R) :
  `|Num.min a b - Num.min c d| <= `|a - c| + `|b - d|.

Used by 2 declarations in 1 file

this file: setI_closed_lipschitz_pos, lipschitz_pos_agree

lemma maxr_dist source, line 437

forall {R : realType} (a b c d : R), `|maxr a b - maxr c d| <= `|a - c| + `|b - d|

Statement as written in the source

Lemma maxr_dist (a b c d : R) :
  `|Num.max a b - Num.max c d| <= `|a - c| + `|b - d|.

Used by 1 declaration in 1 file

this file: measurable_lipschitz_pos

lemma measurable_lipschitz_gt0 source, line 449

forall {R : realType} {k : nat} [Phi : 'rV_k -> R] [L : R],
(forall x y : 'rV_k, `|Phi x - Phi y| <= L * frobenius (x - y)) ->
(measure_matrix_display default_measure_display).-measurable [set x | 0 < Phi x]

Statement as written in the source

Lemma measurable_lipschitz_gt0 (Phi : 'rV[R]_k -> R) (L : R) :
  (forall x y, `|Phi x - Phi y| <= L * frobenius (x - y)) ->
  measurable [set x | 0 < Phi x].

Used by 2 declarations in 1 file

this file: measurable_lipschitz_pos, lipschitz_pos_agree

lemma setI_closed_lipschitz_pos source, line 458

forall {R : realType} {k : nat}, setI_closed lipschitz_pos

Statement as written in the source

Lemma setI_closed_lipschitz_pos : setI_closed lipschitz_pos.

Used by 1 declaration in 1 file

this file: measure_lipschitz_unique

lemma lipschitz_pos_setT source, line 470

forall {R : realType} {k : nat}, lipschitz_pos [set: 'rV_k]

Statement as written in the source

Lemma lipschitz_pos_setT : lipschitz_pos [set: 'rV[R]_k].

Used by 1 declaration in 1 file

this file: measure_lipschitz_unique

lemma measurable_lipschitz_pos main result source, line 477

forall {R : realType} {k : nat},
(measure_matrix_display default_measure_display).-measurable = <<s lipschitz_pos >>

Main result

Stated in the README together with measure_lipschitz_unique.

Statement as written in the source

Lemma measurable_lipschitz_pos : measurable = <<s lipschitz_pos >>.

Used by 1 declaration in 1 file

this file: measure_lipschitz_unique

lemma lipschitz_pos_agree source, line 496

forall {R : realType} {k : nat} [mu1 mu2 : measure 'rV_k R],
(forall (Phi : 'rV_k -> R) (L : R),
 (forall x : 'rV_k, 0 <= Phi x <= 1) ->
 (forall x y : 'rV_k, `|Phi x - Phi y| <= L * frobenius (x - y)) ->
 (\int[mu1]_x (Phi x)%:E)%E = (\int[mu2]_x (Phi x)%:E)%E) ->
forall [A : set 'rV_k], lipschitz_pos A -> mu1 A = mu2 A

Statement as written in the source

Lemma lipschitz_pos_agree (mu1 mu2 : {measure set 'rV[R]_k -> \bar R}) :
  (forall (Phi : 'rV[R]_k -> R) (L : R), (forall x, 0 <= Phi x <= 1) ->
     (forall x y, `|Phi x - Phi y| <= L * frobenius (x - y)) ->
     (\int[mu1]_x (Phi x)%:E = \int[mu2]_x (Phi x)%:E)%E) ->
  forall A, lipschitz_pos A -> mu1 A = mu2 A.

Used by 1 declaration in 1 file

this file: measure_lipschitz_unique

theorem measure_lipschitz_unique main result source, line 546

forall {R : realType} {k : nat} [mu1 mu2 : measure 'rV_k R],
(mu1 [set: 'rV_k] < +oo)%E ->
(forall (Phi : 'rV_k -> R) (L : R),
 (forall x : 'rV_k, 0 <= Phi x <= 1) ->
 (forall x y : 'rV_k, `|Phi x - Phi y| <= L * frobenius (x - y)) ->
 (\int[mu1]_x (Phi x)%:E)%E = (\int[mu2]_x (Phi x)%:E)%E) ->
forall [X : set 'rV_k],
(measure_matrix_display default_measure_display).-measurable X -> mu1 X = mu2 X

Main result, as the README states it

A finite measure on 'rV[R]_k is determined by the integrals of the Lipschitz functions with values in [0, 1]; the sets {Phi > 0}, for Phi nonnegative and Lipschitz, generate the Borel sets.

Statement as written in the source

Theorem measure_lipschitz_unique (mu1 mu2 : {measure set 'rV[R]_k -> \bar R}) :
  (mu1 [set: 'rV[R]_k] < +oo)%E ->
  (forall (Phi : 'rV[R]_k -> R) (L : R), (forall x, 0 <= Phi x <= 1) ->
     (forall x y, `|Phi x - Phi y| <= L * frobenius (x - y)) ->
     (\int[mu1]_x (Phi x)%:E = \int[mu2]_x (Phi x)%:E)%E) ->
  forall X, measurable X -> mu1 X = mu2 X.

Used by 2 declarations in 2 files

this file: gauss_mulmx_law
GaussianAnalysis.fourier.inversion: cf_rV_inversion

The law of x *m A, for x of law gauss n, depends only on A^T *m A: two centered Gaussian vectors with the same covariance have the same law.

sectiongauss_mulmx_law

Context {R : realType}.

theorem gauss_mulmx_law main result source, line 569

forall {R : realType} [n m k : nat] [A : 'M_(n, k)] [B : 'M_(m, k)]
  [X : set 'rV_k],
A^T *m A = B^T *m B ->
(measure_matrix_display default_measure_display).-measurable X ->
gauss n [set x | X (x *m A)] = gauss m [set y | X (y *m B)]

Main result, as the README states it

The law of a centered Gaussian vector depends only on its covariance: for x of law gauss n and y of law gauss m, if A^T *m A = B^T *m B, then P(x *m A \in X) = P(y *m B \in X) for every measurable set X of 'rV[R]_k, and E[f (x *m A)] = E[f (y *m B)] for every measurable f.

Used in theories/ by: Gaussian/Orthogonal/EqualCovariance

Statement as written in the source

Theorem gauss_mulmx_law n m k (A : 'M[R]_(n, k)) (B : 'M[R]_(m, k)) X :
  A^T *m A = B^T *m B -> measurable X ->
  gauss n [set x | X (x *m A)] = gauss m [set y | X (y *m B)].

Used by 3 declarations in 2 files

GaussianAnalysis.random_matrix.goe_entries: goe_mx_row_tail
this file: gauss_orthogonal_law, ge0_integral_gauss_mulmx

corollary gauss_orthogonal_law main result source, line 607

forall {R : realType} [n k : nat] [A : 'M_(n, k)]
  [X : set 'rV_k],
A^T *m A = 1%:M ->
(measure_matrix_display default_measure_display).-measurable X ->
gauss n [set x | X (x *m A)] = gauss k X

If the columns of A are orthonormal, x *m A has law gauss k: in particular gauss n is invariant under every orthogonal matrix.

Main result, as the README states it

If the columns of A are orthonormal, x *m A has law gauss k; in particular gauss n is invariant under every orthogonal matrix. Forms with integrals.

Used in theories/ by: Projected/BulkLaw

Statement as written in the source

Corollary gauss_orthogonal_law n k (A : 'M[R]_(n, k)) X :
  A^T *m A = 1%:M -> measurable X -> gauss n [set x | X (x *m A)] = gauss k X.

Used by 1 declaration in 1 file

this file: integral_gauss_orthogonal

corollary ge0_integral_gauss_mulmx main result source, line 616

forall {R : realType} [n m k : nat] [A : 'M_(n, k)] [B : 'M_(m, k)] [f : 'rV_k -> \bar R],
A^T *m A = B^T *m B ->
measurable_fun [set: 'rV_k] f ->
(forall y : 'rV_k, (0%R <= f y)%E) ->
(\int[gauss n]_x f (x *m A))%E = (\int[gauss m]_y f (y *m B))%E

Main result

Stated in the README together with gauss_orthogonal_law.

Statement as written in the source

Corollary ge0_integral_gauss_mulmx n m k (A : 'M[R]_(n, k)) (B : 'M[R]_(m, k))
    (f : 'rV[R]_k -> \bar R) :
  A^T *m A = B^T *m B -> measurable_fun [set: 'rV[R]_k] f -> (forall y, 0 <= f y)%E ->
  (\int[gauss n]_x f (x *m A) = \int[gauss m]_y f (y *m B))%E.

Used by 2 declarations in 2 files

GaussianAnalysis.probability.hanson_wright: gauss_chaos_mgf
this file: integral_gauss_mulmx

corollary integral_gauss_mulmx main result source, line 633

forall {R : realType} [n m k : nat] [A : 'M_(n, k)] [B : 'M_(m, k)] [f : 'rV_k -> \bar R],
A^T *m A = B^T *m B ->
measurable_fun [set: 'rV_k] f ->
(\int[gauss n]_x f (x *m A))%E = (\int[gauss m]_y f (y *m B))%E

Main result

Stated in the README together with gauss_mulmx_law.

Statement as written in the source

Corollary integral_gauss_mulmx n m k (A : 'M[R]_(n, k)) (B : 'M[R]_(m, k))
    (f : 'rV[R]_k -> \bar R) :
  A^T *m A = B^T *m B -> measurable_fun [set: 'rV[R]_k] f ->
  (\int[gauss n]_x f (x *m A) = \int[gauss m]_y f (y *m B))%E.

Used by 1 declaration in 1 file

GaussianAnalysis.random_matrix.goe_rotation: goe_conj_integral

corollary integral_gauss_orthogonal main result source, line 652

forall {R : realType} [n k : nat] [A : 'M_(n, k)] [f : 'rV_k -> \bar R],
A^T *m A = 1%:M ->
(gauss k).-integrable [set: 'rV_k] f ->
(\int[gauss n]_x f (x *m A))%E = (\int[gauss k]_y f y)%E

Main result

Stated in the README together with gauss_orthogonal_law.

Statement as written in the source

Corollary integral_gauss_orthogonal n k (A : 'M[R]_(n, k)) (f : 'rV[R]_k -> \bar R) :
  A^T *m A = 1%:M -> (gauss k).-integrable [set: 'rV[R]_k] f ->
  (\int[gauss n]_x f (x *m A) = \int[gauss k]_y f y)%E.

Used by 2 declarations in 2 files

GaussianAnalysis.comparison.brascamp_lieb: gauss_ibp_unit
GaussianAnalysis.convex.gauss_feature: gauss_quad_moments

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.