On this page

GaussianAnalysisgaussiangauss_interpolation

Gaussian interpolation and Kahane's comparison inequality

GaussianAnalysis.gaussian.gauss_interpolationlibrary/gaussian/gauss_interpolation.v545 lines12 lemmas and theoremssource

Imports 4 library modules and 20 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.trigo, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral

Imported by 10

Let x have law gauss n, and let M t : 'M_(n, k) depend differentiably on a real parameter t. Then x *m M t is a centered Gaussian vector with covariance (M t)^T *m M t. For F : 'rV_k -> R of class C^2 whose derivatives of order at most 2 grow at most polynomially, gauss_interpolation gives the derivative of t |-> E[F (x *m M t)]:

\sum_(j, l) ((M' t)^T *m M t) j l * E[d_l d_j F (x *m M t)],

with M' the derivative of M and d_j F = 'D_(delta_mx 0 j) F the partial derivative along the j-th vector of the canonical basis. When the Hessian of F is symmetric, this is half the pairing of the derivative of the covariance with the expected Hessian.

gauss_comparison is Kahane's comparison inequality: if

\sum_(j, l) (A^T *m A - B^T *m 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 x of law gauss n and y of law gauss m. The inequalities of Slepian, Sudakov-Fernique and Gordon follow from it for suitable F. The proof applies gauss_interpolation to the path col_mx (cos t *: A) (sin t *: B), t in [0, pi / 2], whose ends give x *m A and y *m B for the two blocks of a vector of law gauss (n + m).

gauss_comparison_partial is the same inequality for F given by its partial derivatives of order 1 and 2 at every point, those of order 2 continuous: F is then of class C^2 (differentiable_partials of partial_derivative.v).

The first sections hold general facts used by the proofs: the chain rule along a curve, the derivative of a matrix product along a path, and integrals of finite sums.

Main results

Results	Statement
gauss_ibp_mulmx	Integration by parts through a linear map: `E[x_i d_j F (x m M)] = \sum_l M_(i, l) E[d_l d_j F (x m M)]`.
gauss_interpolation	Gaussian interpolation: let `x` have law `gauss n`, let the path of matrices `M t` be differentiable on an open interval with derivative `M' t`, with `\|M t\| <= K` and `\|M' t\| <= K` on the interval, and let `F` be of class C^2 with `F` and its partial derivatives of order 1 and 2 all bounded by one `C (1 + \|z\|^p)`. Then at every `t` of the interval the derivative of `t \|-> E[F (x m M t)]` is `\sum_(j, l) ((M' t)^T M t)_(j, l) E[d_l d_j F (x m M t)]`.
gauss_comparison	Kahane's comparison inequality, for `F` of class C^2 with the same growth hypothesis: if `\sum_(j, l) (A^T A - B^T B)_(j, l) d_l d_j F <= 0` everywhere, then `E[F (x m A)] <= E[F (y m B)]` for `x` of law `gauss n` and `y` of law `gauss m`.
gauss_comparison_partial	The same comparison for `F` given by its partial derivatives of order 1 and 2, those of order 2 continuous.

Declarations12 exported, 10 local

sectiondifferential_rV

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

lemma diff_rV_sum source, line 58

forall {R : realType} {k : nat} {W : normedModType R} [F : 'rV_k -> W] 
  [z : 'rV_k] (v : 'rV_k),
differentiable F z -> 'd F z v = \sum_(j < k) v 0 j *: 'D_(delta_mx 0 j) F z

Statement as written in the source

Lemma diff_rV_sum (F : 'rV[R]_k -> W) (z v : 'rV[R]_k) : differentiable F z ->
  'd F z v = \sum_(j < k) v 0 j *: 'D_(delta_mx 0 j) F z.

Used by 2 declarations in 1 file

this file: is_derive_rV_comp, gauss_ibp_mulmx

lemma is_derive_rV_comp source, line 65

forall {R : realType} {k : nat} {W : normedModType R} [F : 'rV_k -> W] 
  [g : R -> 'rV_k] [t : R] [dg : 'rV_k],
differentiable F (g t) ->
is_derive t 1 g dg ->
is_derive t 1 (F \o g) (\sum_(j < k) dg 0 j *: 'D_(delta_mx 0 j) F (g t))

Statement as written in the source

Lemma is_derive_rV_comp (F : 'rV[R]_k -> W) (g : R -> 'rV[R]_k) t
    (dg : 'rV[R]_k) :
  differentiable F (g t) -> is_derive t 1 g dg ->
  is_derive t 1 (F \o g) (\sum_(j < k) dg 0 j *: 'D_(delta_mx 0 j) F (g t)).

Used by 2 declarations in 2 files

this file: gauss_interpolation
GaussianAnalysis.comparison.gauss_concentration: herbst_is_derive_Fz

sectionmulmx_derive

Context {R : realType}.

lemma is_derive_mulmxl source, line 83

forall {R : realType} [m n p : nat] (A : 'M_(m, n)) [M : R -> 'M_(n, p)] 
  [t : R] [dM : 'M[R]_(n, p)],
is_derive t 1 M dM ->
is_derive t 1 (fun s : R => A *m M s)
  (A *m dM)

Statement as written in the source

Lemma is_derive_mulmxl m n p (A : 'M[R]_(m, n)) (M : R -> 'M[R]_(n, p))
    (t : R) dM :
  is_derive t 1 M dM -> is_derive t 1 (fun s => A *m M s) (A *m dM).

Used by 1 declaration in 1 file

this file: gauss_interpolation

lemma mulmx_col_mx source, line 98

forall {R : realType} [m n1 n2 p : nat] (x : 'M_(m, n1 + n2)) (P : 'M_(n1, p))
  (Q : 'M_(n2, p)),
x *m col_mx P Q = lsubmx x *m P + rsubmx x *m Q

Statement as written in the source

Lemma mulmx_col_mx m n1 n2 p (x : 'M[R]_(m, n1 + n2)) (P : 'M[R]_(n1, p))
    (Q : 'M[R]_(n2, p)) :
  x *m col_mx P Q = lsubmx x *m P + rsubmx x *m Q.

Used by 1 declaration in 1 file

this file: gauss_comparison

sectionis_derive_scalel

Context {R : realType} {V : normedModType R}.

lemma is_derive_scalel source, line 108

forall {R : realType} {V : normedModType R} [a : R -> R] (P : V) [t da : R],
is_derive t 1 a da ->
is_derive t 1 (fun s : R => a s *: P)
  (da *: P)

Statement as written in the source

Lemma is_derive_scalel (a : R -> R) (P : V) (t da : R) :
  is_derive t 1 a da -> is_derive t 1 (fun s => a s *: P) (da *: P).

Used by 2 declarations in 2 files

this file: gauss_comparison
GaussianAnalysis.comparison.gauss_concentration: herbst_is_derive_z

sectionRintegral_sum

Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T -> \bar R}.

lemma Rintegral_sum source, line 124

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : measure T R] [I : Type] (s : seq I) [D : set T] [f : I -> T -> R],
d.-measurable D ->
(forall i : I, mu.-integrable D (EFin \o f i)) ->
\int[mu]_(x in D) \sum_(i <- s) f i x = \sum_(i <- s) \int[mu]_(x in D) f i x

Statement as written in the source

Lemma Rintegral_sum (I : Type) (s : seq I) (D : set T) (f : I -> T -> R) :
  measurable D -> (forall i, mu.-integrable D (EFin \o f i)) ->
  \int[mu]_(x in D) \sum_(i <- s) f i x = \sum_(i <- s) \int[mu]_(x in D) f i x.

Used by 12 declarations in 7 files

this file: gauss_ibp_mulmx, gauss_ibp_gradient, gauss_comparison
GaussianAnalysis.random_matrix.goe: Rintegral_polyfun_sum
GaussianAnalysis.random_matrix.goe_rotation: Rint_sum2, goe_diag_var_identityS
GaussianAnalysis.random_matrix.wigner: semicircle_poly
GaussianAnalysis.comparison.gauss_concentration: herbst_df_lower
GaussianAnalysis.comparison.escape: gauss_frobenius_mean_le, gauss_sqr_mulmx
GaussianAnalysis.comparison.brascamp_lieb: dLambda_le0, Lambda_lip

sectiongauss_entry_integrable

Context {R : realType}.

lemma integrable_gauss_entry source, line 143

forall {R : realType} [n : nat] (i : 'I_n) [G : 'rV_n -> R] [c : R] [q : nat],
measurable_fun [set: 'rV_n] G ->
(forall x : 'rV_n, `|G x| <= c * (1 + `|x| ^+ q)) ->
(gauss n).-integrable [set: 'rV_n] (EFin \o (fun x : 'rV_n => x 0 i * G x))

Statement as written in the source

Lemma integrable_gauss_entry n (i : 'I_n) (G : 'rV[R]_n -> R) (c : R) q :
  measurable_fun [set: 'rV[R]_n] G ->
  (forall x, `|G x| <= c * (1 + `|x| ^+ q)) ->
  (gauss n).-integrable [set: 'rV[R]_n]
    (EFin \o (fun x : 'rV[R]_n => x 0 i * G x)).

Used by 1 declaration in 1 file

this file: gauss_ibp_gradient

F is of class C^2, and F and its partial derivatives of order 1 and 2 are bounded by C (1 + |z|^p).

sectiongauss_interpolation

Context {R : realType} {k : nat}.
Variable F : 'rV[R]_k -> R.
Local Notation DF j := ('D_(delta_mx 0 j) F).
Local Notation D2F j l := ('D_(delta_mx 0 l) ('D_(delta_mx 0 j) F)).
Hypothesis F_diff : forall z, differentiable F z.
Hypothesis DF_diff : forall j z, differentiable (DF j) 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).

let C_ge0 section-local source, line 173

Let C_ge0 : 0 <= C.

Used by 3 declarations in 1 file

this file: poly_mulmx, gauss_ibp_mulmx, gauss_interpolation

let poly_mulmx section-local source, line 176

Let poly_mulmx n (G : 'rV[R]_k -> R) (M : 'M[R]_(n, k)) (K : R) :
  `|M| <= K -> (forall z, `|G z| <= C * (1 + `|z| ^+ p)) ->
  forall x : 'rV[R]_n,
    `|G (x *m M)| <= C * (1 + (n%:R * K) ^+ p) * (1 + `|x| ^+ p).

Used by 5 declarations in 1 file

this file: integrable_D2F_mulmx, gauss_ibp_mulmx, gauss_ibp_gradient, gauss_interpolation, gauss_comparison

let integrable_D2F_mulmx section-local source, line 195

Let integrable_D2F_mulmx n (M : 'M[R]_(n, k)) j l :
  (gauss n).-integrable [set: 'rV[R]_n]
    (EFin \o (fun x : 'rV[R]_n => D2F j l (x *m M))).

Used by 1 declaration in 1 file

this file: gauss_comparison

lemma gauss_ibp_mulmx main result source, line 207

forall {R : realType} {k : nat} [F : 'rV_k -> R],
(forall (j : 'I_k)
   (z : 'rV[R]_k),
 differentiable ('D_(delta_mx 0 j) F) z) ->
(forall j l : 'I_k,
 continuous ('D_(delta_mx 0 l) ('D_(delta_mx 0 j) F))) ->
forall [C : R] [p : nat],
(forall z : 'rV_k, `|F z| <= C * (1 + `|z| ^+ p)) ->
(forall (j : 'I_k)
   (z : 'rV[R]_k),
 `|('D_(delta_mx 0 j) F) z| <= C * (1 + `|z| ^+ p)) ->
(forall (j l : 'I_k)
   (z : 'rV[R]_k),
 `|('D_(delta_mx 0 l) ('D_(delta_mx 0 j) F)) z| <= C * (1 + `|z| ^+ p)) ->
forall [n : nat] (M : 'M_(n, k)) (i : 'I_n) (j : 'I_k),
\int[gauss n]_x (x 0 i * ('D_(delta_mx 0 j) F) (x *m M)) =
\sum_(l < k) M i l * \int[gauss n]_x ('D_(delta_mx 0 l) ('D_(delta_mx 0 j) F)) (x *m M)

Integration by parts for x_i against a partial derivative of F at x *m M.

Main result, as the README states it

Integration by parts through a linear map: E[x_i d_j F (x *m M)] = \sum_l M_(i, l) E[d_l d_j F (x *m M)].

Statement as written in the source

Lemma gauss_ibp_mulmx n (M : 'M[R]_(n, k)) (i : 'I_n) (j : 'I_k) :
  \int[gauss n]_x (x 0 i * DF j (x *m M)) =
  \sum_(l < k) M i l * \int[gauss n]_x D2F j l (x *m M).

Used by 1 declaration in 1 file

this file: gauss_ibp_gradient

lemma gauss_ibp_gradient source, line 261

forall {R : realType} {k : nat} [F : 'rV_k -> R],
(forall (j : 'I_k)
   (z : 'rV[R]_k),
 differentiable ('D_(delta_mx 0 j) F) z) ->
(forall j l : 'I_k,
 continuous ('D_(delta_mx 0 l) ('D_(delta_mx 0 j) F))) ->
forall [C : R] [p : nat],
(forall z : 'rV_k, `|F z| <= C * (1 + `|z| ^+ p)) ->
(forall (j : 'I_k)
   (z : 'rV[R]_k),
 `|('D_(delta_mx 0 j) F) z| <= C * (1 + `|z| ^+ p)) ->
(forall (j l : 'I_k)
   (z : 'rV[R]_k),
 `|('D_(delta_mx 0 l) ('D_(delta_mx 0 j) F)) z| <= C * (1 + `|z| ^+ p)) ->
forall [n : nat] (M M' : 'M_(n, k)),
\int[gauss n]_x \sum_(j < k) (x *m M') 0 j * ('D_(delta_mx 0 j) F) (x *m M) =
\sum_(j < k)
   \sum_(l < k)
      (M'^T *m M) j l * \int[gauss n]_x ('D_(delta_mx 0 l) ('D_(delta_mx 0 j) F)) (x *m M)

The same for the derivative of F at x *m M in the direction x *m M'.

Statement as written in the source

Lemma gauss_ibp_gradient n (M M' : 'M[R]_(n, k)) :
  \int[gauss n]_x (\sum_(j < k) (x *m M') 0 j * DF j (x *m M)) =
  \sum_(j < k) \sum_(l < k) (M'^T *m M) j l * \int[gauss n]_x D2F j l (x *m M).

Used by 1 declaration in 1 file

this file: gauss_interpolation

lemma gauss_interpolation main result source, line 294

forall {R : realType} {k : nat} [F : 'rV_k -> R],
(forall z : 'rV[R]_k, differentiable F z) ->
(forall (j : 'I_k)
   (z : 'rV[R]_k),
 differentiable ('D_(delta_mx 0 j) F) z) ->
(forall j l : 'I_k,
 continuous ('D_(delta_mx 0 l) ('D_(delta_mx 0 j) F))) ->
forall [C : R] [p : nat],
(forall z : 'rV_k, `|F z| <= C * (1 + `|z| ^+ p)) ->
(forall (j : 'I_k)
   (z : 'rV[R]_k),
 `|('D_(delta_mx 0 j) F) z| <= C * (1 + `|z| ^+ p)) ->
(forall (j l : 'I_k)
   (z : 'rV[R]_k),
 `|('D_(delta_mx 0 l) ('D_(delta_mx 0 j) F)) z| <= C * (1 + `|z| ^+ p)) ->
forall [n : nat] [M M' : R -> 'M_(n, k)] [u v K : R],
(forall s : R, s \in `]u, v[ -> is_derive s 1 M (M' s)) ->
(forall s : R, s \in `]u, v[ -> `|M s| <= K) ->
(forall s : R, s \in `]u, v[ -> `|M' s| <= K) ->
forall [t : R],
t \in `]u, v[ ->
is_derive t 1
  (fun s : R =>
   \int[gauss n]_x F (x *m M s))
  (\sum_(j < k)
      \sum_(l < k)
         ((M' t)^T *m M t) j l *
         \int[gauss n]_x ('D_(delta_mx 0 l) ('D_(delta_mx 0 j) F)) (x *m M t))

Main result, as the README states it

Gaussian interpolation: let x have law gauss n, let the path of matrices M t be differentiable on an open interval with derivative M' t, with |M t| <= K and |M' t| <= K on the interval, and let F be of class C^2 with F and its partial derivatives of order 1 and 2 all bounded by one C (1 + |z|^p). Then at every t of the interval the derivative of t |-> E[F (x *m M t)] is \sum_(j, l) ((M' t)^T M t)_(j, l) E[d_l d_j F (x *m M t)].

Statement as written in the source

Lemma gauss_interpolation n (M M' : R -> 'M[R]_(n, k)) (u v K : R) :
  (forall s, s \in `]u, v[ -> is_derive s 1 M (M' s)) ->
  (forall s, s \in `]u, v[ -> `|M s| <= K) ->
  (forall s, s \in `]u, v[ -> `|M' s| <= K) ->
  forall t, t \in `]u, v[ ->
  is_derive t 1 (fun s => \int[gauss n]_x F (x *m M s))
    (\sum_(j < k) \sum_(l < k) ((M' t)^T *m M t) j l *
      \int[gauss n]_x D2F j l (x *m M t)).

Used by 1 declaration in 1 file

this file: gauss_comparison

lemma gauss_comparison main result source, line 369

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

Main result, as the README states it

Kahane's comparison inequality, for F of class C^2 with the same growth hypothesis: if \sum_(j, l) (A^T A - B^T B)_(j, l) d_l d_j F <= 0 everywhere, then E[F (x *m A)] <= E[F (y *m B)] for x of law gauss n and y of law gauss m.

Statement as written in the source

Lemma gauss_comparison n m (A : 'M[R]_(n, k)) (B : 'M[R]_(m, k)) :
  (forall z,
    \sum_(j < k) \sum_(l < k) (A^T *m A - B^T *m B) j l * D2F j l z <= 0) ->
  (\int[gauss n]_x (F (x *m A))%:E <= \int[gauss m]_y (F (y *m B))%:E)%E.

Used by 3 declarations in 3 files

this file: gauss_comparison_partial
GaussianAnalysis.comparison.slepian: sudakov_fernique
GaussianAnalysis.comparison.gordon: gordon

Kahane's comparison inequality for F given by its partial derivatives of order 1 and 2, continuous at order 2: F is then of class C^2.

sectiongauss_comparison_partial

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).

let DF_diff section-local source, line 505

Let DF_diff j z : differentiable (DF j) z.

Used by 2 declarations in 1 file

this file: DF_cont, gauss_comparison_partial

let DF_cont section-local source, line 511

Let DF_cont j : continuous (DF j).

Used by 1 declaration in 1 file

this file: F_diff

let F_diff section-local source, line 514

Let F_diff z : differentiable F z.

Used by 1 declaration in 1 file

this file: gauss_comparison_partial

let DFE section-local source, line 519

Let DFE j : 'D_(delta_mx 0 j) F = DF j.

Used by 3 declarations in 1 file

this file: D2FE, D2FEz, gauss_comparison_partial

let D2FE section-local source, line 522

Let D2FE j l : 'D_(delta_mx 0 l) ('D_(delta_mx 0 j) F) = D2F j l.

Used by 1 declaration in 1 file

this file: gauss_comparison_partial

let DFEz section-local source, line 525

Let DFEz j z : 'D_(delta_mx 0 j) F z = DF j z.

Used by 1 declaration in 1 file

this file: gauss_comparison_partial

let D2FEz section-local source, line 528

Let D2FEz j l z : 'D_(delta_mx 0 l) ('D_(delta_mx 0 j) F) z = D2F j l z.

Used by 1 declaration in 1 file

this file: gauss_comparison_partial

lemma gauss_comparison_partial main result source, line 531

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)],
(forall z : 'rV_k, \sum_(j < k) \sum_(l < k) (A^T *m A - B^T *m B) j l * D2F j l z <= 0) ->
(\int[gauss n]_x (F (x *m A))%:E <= \int[gauss m]_y (F (y *m B))%:E)%E

Main result, as the README states it

The same comparison for F given by its partial derivatives of order 1 and 2, those of order 2 continuous.

Statement as written in the source

Lemma gauss_comparison_partial n m (A : 'M[R]_(n, k)) (B : 'M[R]_(m, k)) :
  (forall z,
    \sum_(j < k) \sum_(l < k) (A^T *m A - B^T *m B) j l * D2F j l z <= 0) ->
  (\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

GaussianAnalysis.comparison.gauss_law: gauss_law_smooth

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.