On this page

The Sudakov-Fernique and Slepian inequalities

GaussianAnalysis.comparison.slepianlibrary/comparison/slepian.v480 lines32 lemmas and theorems, 5 definitionssource

Imports 8 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 8

Required by 1 files of the paper proofs

theories/Gordon/Processes.v

Let x have law gauss n and y have law gauss m. For A : 'M[R]_(n, k.+1), x *m A is a centered Gaussian vector of covariance A^T *m A, and every centered Gaussian vector of 'rV[R]_k.+1 has this form. If every increment of x *m A has a variance at most that of the same increment of y *m B, that is incr_var A j l <= incr_var B j l for all j and l, then E[rmax (x *m A)] <= E[rmax (y *m B)], where rmax z is the largest coordinate of z (sudakov_fernique). Equal variances and larger covariances imply the hypothesis (slepian).

The proof applies Kahane's comparison inequality (gauss_comparison) to the log-sum-exp function lse b. For every square matrix M, the pairing of M with the Hessian of lse b at z is b / 2 * \sum_(j, l) p_j p_l (M j j + M l l - 2 M j l), with p = softmax b z (lse_hessian). For M = A^T *m A - B^T *m B it is nonpositive. Since rmax z <= lse b z <= rmax z + ln (k + 1) / b, letting b grow concludes.

`rmax z`	the largest coordinate of the row vector z
`lse b z`	b^-1 * ln (\sum_j expR (b * z 0 j))
`softmax b z j`	expR (b * z 0 j) / \sum_i expR (b * z 0 i)
`incr_var A j l`	(A^T m A) j j + (A^T m A) l l - 2 * (A^T m A) j l, the variance of (x m A) 0 j - (x *m A) 0 l

Main results

Results	Statement
sudakov_fernique	Sudakov-Fernique inequality: for `x` of law `gauss n` and `y` of law `gauss m`, if each increment `(x A)_j - (x A)_l` has variance at most that of `(y B)_j - (y B)_l`, then `E[max_j (x A)_j] <= E[max_j (y B)_j]`.
slepian	Slepian's inequality for expected maxima: if `x A` and `y B` have the same variances and each covariance of `x A` is at least that of `y B`, then `E[max_j (x A)_j] <= E[max_j (y B)_j]`.
rmax_le_lselse_le_rmaxlse_hessian	The log-sum-exp function `lse b z = ln (\sum_j expR (b z_j)) / b`, `b > 0`, satisfies `max_j z_j <= lse b z <= max_j z_j + ln (k + 1) / b`. Its Hessian paired with a matrix `M` is `b / 2 \sum_(j, l) p_j p_l (M_jj + M_ll - 2 M_jl)`, with `p` the softmax weights.

Declarations37 exported

sectionrmax

Context {R : realType} {k : nat}.
Implicit Types z : 'rV[R]_k.+1.

definition rmax source, line 60

Type

forall {R : realType} {k : nat}, 'rV_k.+1 -> R

Definition

Definition rmax z : R := \big[Num.max/z 0 ord0]_j z 0 j.

The largest coordinate of a row vector.

Used by 43 declarations in 6 files

GaussianAnalysis.matrix.covering: frob_sep
GaussianAnalysis.random_matrix.goe_edge: goe_form_max_mean, lambda_max_net_le, goe_lambda_max_mean
this file: le_rmax, rmax_le, rmax_eq, rmax_lipschitz, continuous_rmax, rmax_norm, rmax_le_lse, lse_le_rmax, integrable_gauss_rmax, lse_norm, sudakov_fernique, slepian
GaussianAnalysis.comparison.gordon: minmax, minmax_le, le_minmax, rmax_leD, minmax_leD, minmax_norm, smm_le, le_smm
GaussianAnalysis.comparison.escape: rmax_addr, minmax_add, rmax_vec_add, minmax_aux, rmax_aux, integral_minmax_aux, integral_rmax_aux, bil_aux_max, rmax_net_ge, minmax_bil_le, rmax_fam_width, gordon_escape, minmax_bil_sph_le, rmax_net_width, gordon_minmax, gauss_opnorm_mean
GaussianAnalysis.comparison.sudakov: gauss_max_lower, rmaxZ, sudakov_minoration

lemma le_rmax source, line 62

forall {R : realType} {k : nat} (z : 'rV_k.+1) (j : 'I_k.+1), z 0 j <= rmax z

Statement as written in the source

Lemma le_rmax z j : z 0 j <= rmax z.

Used by 12 declarations in 6 files

GaussianAnalysis.random_matrix.goe_edge: lambda_max_net_le
this file: rmax_lipschitz, lse_le_rmax
GaussianAnalysis.comparison.gordon: minmax_le, rmax_leD
GaussianAnalysis.comparison.escape: rmax_vec_add, rmax_net_ge, rmax_net_width, gauss_opnorm_mean
GaussianAnalysis.comparison.cgmt: infsup_net
GaussianAnalysis.comparison.sudakov: gauss_max_lower, rmaxZ

lemma rmax_le source, line 65

forall {R : realType} {k : nat} [z : 'rV_k.+1] [c : R],
(forall j : 'I_k.+1, z 0 j <= c) -> rmax z <= c

Statement as written in the source

Lemma rmax_le z c : (forall j, z 0 j <= c) -> rmax z <= c.

Used by 13 declarations in 7 files

GaussianAnalysis.matrix.covering: frob_sep
GaussianAnalysis.matrix.tensor_packing: sudakov_mx_series
GaussianAnalysis.random_matrix.goe_edge: goe_form_max_mean
GaussianAnalysis.comparison.gordon: le_minmax, rmax_leD
GaussianAnalysis.comparison.escape: rmax_vec_add, minmax_bil_le, rmax_fam_width, minmax_bil_sph_le, gauss_opnorm_mean
GaussianAnalysis.comparison.cgmt: infsup_net
GaussianAnalysis.comparison.sudakov: gauss_max_lower, rmaxZ

lemma rmax_eq source, line 68

forall {R : realType} {k : nat} (z : 'rV_k.+1), exists j : 'I_k.+1, rmax z = z 0 j

Statement as written in the source

Lemma rmax_eq z : exists j, rmax z = z 0 j.

Used by 7 declarations in 4 files

this file: rmax_lipschitz, rmax_norm, rmax_le_lse
GaussianAnalysis.comparison.gordon: minmax_norm
GaussianAnalysis.comparison.escape: rmax_vec_add, rmax_net_ge
GaussianAnalysis.comparison.sudakov: rmaxZ

lemma rmax_lipschitz source, line 75

forall {R : realType} {k : nat} (z z' : 'rV_k.+1), `|rmax z - rmax z'| <= `|z - z'|

Statement as written in the source

Lemma rmax_lipschitz z z' : `|rmax z - rmax z'| <= `|z - z'|.

Used by 4 declarations in 2 files

this file: continuous_rmax, rmax_norm
GaussianAnalysis.comparison.sudakov: gauss_max_lower, sudakov_minoration

lemma continuous_rmax source, line 86

forall {R : realType} {k : nat}, continuous rmax

Statement as written in the source

Lemma continuous_rmax : continuous rmax.

Used by 2 declarations in 2 files

this file: integrable_gauss_rmax
GaussianAnalysis.comparison.sudakov: gauss_max_lower

lemma rmax_norm source, line 93

forall {R : realType} {k : nat} (z : 'rV_k.+1), `|rmax z| <= `|z|

Statement as written in the source

Lemma rmax_norm z : `|rmax z| <= `|z|.

Used by 2 declarations in 1 file

this file: integrable_gauss_rmax, lse_norm

sectioncoord_calculus

Context {R : realType} {n : nat}.
Implicit Types z : 'rV[R]_n.

lemma delta_shiftE source, line 107

forall {R : realType} {n : nat} (z : 'rV_n)
  (j : 'I_n) (i : 'I_n) 
  (h : R),
(h *: delta_mx 0 j + z) 0 i = z 0 i + h * (i == j)%:R

Statement as written in the source

Lemma delta_shiftE z j i (h : R) :
  (h *: delta_mx 0 j + z) 0 i = z 0 i + h * (i == j)%:R.

Used by 1 declaration in 1 file

this file: is_derive_expR_coord

lemma is_derive_affine source, line 112

forall {R : realType} (c d h : R), is_derive h 1 (fun h0 : R => c + d * h0) d

A real affine function of h has derivative its slope.

Statement as written in the source

Lemma is_derive_affine (c d h : R) : is_derive h 1 (fun h : R => c + d * h) d.

Used by 2 declarations in 2 files

this file: is_derive_expR_coord
GaussianAnalysis.comparison.gauss_law: is_derive_affine_comp

lemma is_derive_expR_coord source, line 120

forall {R : realType} {n : nat} (b : R) (z : 'rV_n) (i : 'I_n)
  (j : 'I_n),
is_derive z (delta_mx 0 j) (fun z0 : 'rV_n => expR (b * z0 0 i))
  (b * (i == j)%:R * expR (b * z 0 i))

Statement as written in the source

Lemma is_derive_expR_coord (b : R) z i j :
  is_derive z (delta_mx 0 j) (fun z => expR (b * z 0 i))
    (b * (i == j)%:R * expR (b * z 0 i)).

Used by 4 declarations in 2 files

this file: is_derive_lse_sum, is_derive_softmax
GaussianAnalysis.comparison.gordon: is_derive_gsum, is_derive_smm_D

lemma is_derive_lift source, line 134

forall {R : realType} {n : nat} [F : 'rV_n -> R] [g : R -> R] [z v : 'rV_n] [d dg : R],
is_derive z v F d -> is_derive (F z) 1 g dg -> is_derive z v (g \o F) (dg * d)

The chain rule for a real function of a function of 'rV[R]_n.

Statement as written in the source

Lemma is_derive_lift (F : 'rV[R]_n -> R) (g : R -> R) z (v : 'rV[R]_n)
    (d dg : R) :
  is_derive z v F d -> is_derive (F z) 1 g dg -> is_derive z v (g \o F) (dg * d).

Used by 6 declarations in 2 files

this file: is_derive_lse, is_derive_softmax
GaussianAnalysis.comparison.gordon: is_derive_gtot, is_derive_gsumV, is_derive_smm_D, is_derive_smm

lemma continuous_expR_coord source, line 148

forall {R : realType} {n : nat} [b : R] [i : 'I_n],
continuous (fun z : 'rV_n => expR (b * z 0 i))

Statement as written in the source

Lemma continuous_expR_coord (b : R) i :
  continuous (fun z : 'rV[R]_n => expR (b * z 0 i)).

Used by 3 declarations in 2 files

this file: continuous_softmax
GaussianAnalysis.comparison.gordon: continuous_gsum, continuous_gp

sectionlse

Context {R : realType} {k : nat}.
Variable b : R.
Hypothesis b0 : 0 < b.
Implicit Types z : 'rV[R]_k.+1.

definition lse source, line 166

Type

forall {R : realType} {k : nat}, R -> 'rV_k.+1 -> R

Definition

Definition lse z : R := b^-1 * ln (\sum_j expR (b * z 0 j)).

The log-sum-exp function, a smooth approximation of rmax, and its gradient, the softmax weights.

Used by 12 declarations in 2 files

this file: rmax_le_lse, lse_le_rmax, is_derive_lse, lse_differentiable, lse_DE, lse_D2E, lse_norm, integrable_gauss_lse, sudakov_fernique
GaussianAnalysis.comparison.gordon: smm_lse, smm_le, le_smm

definition softmax source, line 168

Type

forall {R : realType} {k : nat}, R -> 'rV_k.+1 -> 'I_k.+1 -> R

Definition

Definition softmax z (j : 'I_k.+1) : R := expR (b * z 0 j) / \sum_i expR (b * z 0 i).

Used by 13 declarations in 1 file

this file: is_derive_lse, is_derive_softmax, continuous_softmax, softmax_ge0, softmax_sum, softmax_le1, lse_D2, lse_differentiable, lse_DE, continuous_lse_D2, softmax_differentiable, lse_hessian, sudakov_fernique

lemma lse_sum_gt0 source, line 170

forall {R : realType} {k : nat} (b : R) (z : 'rV_k.+1), 0 < \sum_j expR (b * z 0 j)

Statement as written in the source

Lemma lse_sum_gt0 z : 0 < \sum_j expR (b * z 0 j).

Used by 7 declarations in 1 file

this file: rmax_le_lse, lse_le_rmax, is_derive_lse, is_derive_softmax, continuous_softmax, softmax_ge0, softmax_sum

lemma rmax_le_lse main result source, line 175

forall {R : realType} {k : nat} [b : R], 0 < b -> forall z : 'rV_k.+1, rmax z <= lse b z

Main result, as the README states it

The log-sum-exp function lse b z = ln (\sum_j expR (b z_j)) / b, b > 0, satisfies max_j z_j <= lse b z <= max_j z_j + ln (k + 1) / b. Its Hessian paired with a matrix M is b / 2 \sum_(j, l) p_j p_l (M_jj + M_ll - 2 M_jl), with p the softmax weights.

Statement as written in the source

Lemma rmax_le_lse z : rmax z <= lse z.

Used by 4 declarations in 2 files

this file: lse_norm, sudakov_fernique
GaussianAnalysis.comparison.gordon: smm_le, le_smm

lemma lse_le_rmax main result source, line 182

forall {R : realType} {k : nat} [b : R],
0 < b -> forall z : 'rV_k.+1, lse b z <= rmax z + ln k.+1%:R / b

Main result

Stated in the README together with rmax_le_lse.

Statement as written in the source

Lemma lse_le_rmax z : lse z <= rmax z + ln k.+1%:R / b.

Used by 4 declarations in 2 files

this file: lse_norm, sudakov_fernique
GaussianAnalysis.comparison.gordon: smm_le, le_smm

lemma is_derive_lse_sum source, line 197

forall {R : realType} {k : nat} (b : R) (z : 'rV_k.+1)
  (j : 'I_k.+1),
is_derive z (delta_mx 0 j) (fun z0 : 'rV_k.+1 => \sum_i expR (b * z0 0 i))
  (b * expR (b * z 0 j))

Statement as written in the source

Lemma is_derive_lse_sum z j :
  is_derive z (delta_mx 0 j) (fun z => \sum_i expR (b * z 0 i)) (b * expR (b * z 0 j)).

Used by 2 declarations in 1 file

this file: is_derive_lse, is_derive_softmax

lemma is_derive_lse source, line 207

forall {R : realType} {k : nat} [b : R],
0 < b ->
forall (z : 'rV_k.+1) (j : 'I_k.+1),
is_derive z (delta_mx 0 j) (lse b) (softmax b z j)

Statement as written in the source

Lemma is_derive_lse z j : is_derive z (delta_mx 0 j) lse (softmax z j).

Used by 3 declarations in 1 file

this file: lse_differentiable, lse_DE, sudakov_fernique

lemma is_derive_softmax source, line 217

forall {R : realType} {k : nat} (b : R) (z : 'rV_k.+1) (j : 'I_k.+1)
  (l : 'I_k.+1),
is_derive z (delta_mx 0 l) ((softmax b)^~ j)
  (b * (softmax b z j * (j == l)%:R - softmax b z j * softmax b z l))

Statement as written in the source

Lemma is_derive_softmax z j l :
  is_derive z (delta_mx 0 l) (softmax ^~ j)
    (b * (softmax z j * (j == l)%:R - softmax z j * softmax z l)).

Used by 2 declarations in 1 file

this file: softmax_differentiable, lse_D2E

lemma continuous_softmax source, line 229

forall {R : realType} {k : nat} [b : R] [j : 'I_k.+1], continuous ((softmax b)^~ j)

Statement as written in the source

Lemma continuous_softmax j : continuous (softmax ^~ j).

Used by 2 declarations in 1 file

this file: lse_differentiable, continuous_lse_D2

lemma softmax_ge0 source, line 242

forall {R : realType} {k : nat} (b : R) (z : 'rV_k.+1) (j : 'I_k.+1), 0 <= softmax b z j

Statement as written in the source

Lemma softmax_ge0 z j : 0 <= softmax z j.

Used by 2 declarations in 1 file

this file: softmax_le1, sudakov_fernique

lemma softmax_sum source, line 245

forall {R : realType} {k : nat} (b : R) (z : 'rV_k.+1), \sum_j softmax b z j = 1

Statement as written in the source

Lemma softmax_sum z : \sum_j softmax z j = 1.

Used by 2 declarations in 1 file

this file: softmax_le1, lse_hessian

lemma softmax_le1 source, line 250

forall {R : realType} {k : nat} (b : R) (z : 'rV_k.+1) (j : 'I_k.+1), softmax b z j <= 1

Statement as written in the source

Lemma softmax_le1 z j : softmax z j <= 1.

Used by 1 declaration in 1 file

this file: sudakov_fernique

sectionlse_smooth

Context {R : realType} {k : nat}.
Variable b : R.
Hypothesis b0 : 0 < b.

definition lse_D2 source, line 264

Type

forall {R : realType} {k : nat}, R -> 'I_k.+1 -> 'I_k.+1 -> 'rV_k.+1 -> R

Definition

Definition lse_D2 (j l : 'I_k.+1) (z : 'rV[R]_k.+1) : R :=
  b * (softmax b z j * (j == l)%:R - softmax b z j * softmax b z l).

The second partial derivatives of lse b.

Used by 5 declarations in 1 file

this file: continuous_lse_D2, softmax_differentiable, lse_D2E, lse_hessian, sudakov_fernique

lemma lse_differentiable source, line 267

forall {R : realType} {k : nat} [b : R],
0 < b ->
forall z : 'rV[R]_k.+1,
differentiable (lse b : 'rV_k.+1 -> R^o) z

Statement as written in the source

Lemma lse_differentiable z : differentiable (lse b : 'rV[R]_k.+1 -> R^o) z.

Used by 2 declarations in 1 file

this file: integrable_gauss_lse, sudakov_fernique

lemma lse_DE source, line 274

forall {R : realType} {k : nat} [b : R],
0 < b ->
forall j : 'I_k.+1,
'D_(delta_mx 0 j) (lse b) = (softmax b)^~ j

Statement as written in the source

Lemma lse_DE j : 'D_(delta_mx 0 j) (lse b) = softmax b ^~ j :> ('rV[R]_k.+1 -> R).

Used by 2 declarations in 1 file

this file: lse_D2E, sudakov_fernique

lemma continuous_lse_D2 source, line 277

forall {R : realType} {k : nat} [b : R] [j l : 'I_k.+1], continuous (lse_D2 b j l)

Statement as written in the source

Lemma continuous_lse_D2 j l : continuous (lse_D2 j l).

Used by 2 declarations in 1 file

this file: softmax_differentiable, sudakov_fernique

lemma softmax_differentiable source, line 292

forall {R : realType} {k : nat} (b : R) (j : 'I_k.+1)
  (z : 'rV[R]_k.+1),
differentiable ((softmax b)^~ j : 'rV_k.+1 -> R^o) z

Statement as written in the source

Lemma softmax_differentiable j z :
  differentiable (softmax b ^~ j : 'rV[R]_k.+1 -> R^o) z.

Used by 1 declaration in 1 file

this file: sudakov_fernique

lemma lse_D2E source, line 300

forall {R : realType} {k : nat} [b : R],
0 < b ->
forall j l : 'I_k.+1,
'D_(delta_mx 0 l) ('D_(delta_mx 0 j) (lse b)) = lse_D2 b j l

Statement as written in the source

Lemma lse_D2E j l :
  'D_(delta_mx 0 l) ('D_(delta_mx 0 j) (lse b)) = lse_D2 j l :> ('rV[R]_k.+1 -> R).

Used by 1 declaration in 1 file

this file: sudakov_fernique

lemma lse_hessian main result source, line 307

forall {R : realType} {k : nat} (b : R) (M : 'M_k.+1) (z : 'rV_k.+1),
\sum_j \sum_l M j l * lse_D2 b j l z =
b / 2 * \sum_j \sum_l softmax b z j * softmax b z l * (M j j + M l l - 2 * M j l)

Main result

Stated in the README together with rmax_le_lse.

Statement as written in the source

Lemma lse_hessian (M : 'M[R]_k.+1) z :
  \sum_j \sum_l M j l * lse_D2 j l z =
  b / 2 * \sum_j \sum_l softmax b z j * softmax b z l * (M j j + M l l - 2 * M j l).

Used by 1 declaration in 1 file

this file: sudakov_fernique

sectionsudakov_fernique

Context {R : realType}.

definition incr_var source, line 345

Type

forall {R : realType} [n k : nat], 'M_(n, k) -> 'I_k -> 'I_k -> R

Definition

Definition incr_var n k (A : 'M[R]_(n, k)) (j l : 'I_k) : R :=
  (A^T *m A) j j + (A^T *m A) l l - 2 * (A^T *m A) j l.

For x of law gauss n, the variance of (x *m A)_j - (x *m A)_l.

Used by 10 declarations in 6 files

GaussianAnalysis.random_matrix.goe_edge: goe_form_incr_var
this file: sudakov_fernique, slepian
GaussianAnalysis.comparison.gordon: gordon, gordon_cov
GaussianAnalysis.comparison.escape: incr_var_bil_aux, bil_aux_max, incr_var_bilT_auxT
GaussianAnalysis.comparison.cgmt: incr_var_gamma
GaussianAnalysis.comparison.sudakov: sudakov_minoration

lemma integrable_gauss_rmax source, line 348

forall {R : realType} [n k : nat] (A : 'M_(n, k.+1)),
(gauss n).-integrable [set: 'rV_n] (EFin \o (fun x : 'rV_n => rmax (x *m A)))

Statement as written in the source

Lemma integrable_gauss_rmax n k (A : 'M[R]_(n, k.+1)) :
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o (fun x => rmax (x *m A))).

Used by 11 declarations in 6 files

GaussianAnalysis.matrix.covering: frob_sep
GaussianAnalysis.matrix.tensor_packing: sudakov_mx_series
GaussianAnalysis.random_matrix.goe_edge: goe_form_max_mean, goe_lambda_max_mean
this file: sudakov_fernique
GaussianAnalysis.comparison.escape: integral_minmax_aux, integral_rmax_aux, gordon_escape, gordon_minmax, gauss_opnorm_mean
GaussianAnalysis.comparison.sudakov: sudakov_minoration

lemma lse_norm source, line 361

forall {R : realType} [k : nat] [b : R] (z : 'rV_k.+1),
0 < b -> `|lse b z| <= `|z| + ln k.+1%:R / b

Statement as written in the source

Lemma lse_norm k (b : R) (z : 'rV[R]_k.+1) : 0 < b ->
  `|lse b z| <= `|z| + ln k.+1%:R / b.

Used by 2 declarations in 1 file

this file: integrable_gauss_lse, sudakov_fernique

lemma integrable_gauss_lse source, line 372

forall {R : realType} [n k : nat] [b : R] (A : 'M_(n, k.+1)),
0 < b -> (gauss n).-integrable [set: 'rV_n] (EFin \o (fun x : 'rV_n => lse b (x *m A)))

Statement as written in the source

Lemma integrable_gauss_lse n k (b : R) (A : 'M[R]_(n, k.+1)) : 0 < b ->
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o (fun x => lse b (x *m A))).

Used by 1 declaration in 1 file

this file: sudakov_fernique

theorem sudakov_fernique main result source, line 389

forall {R : realType} [n m k : nat] [A : 'M_(n, k.+1)] [B : 'M_(m, k.+1)],
(forall j l : 'I_k.+1, incr_var A j l <= incr_var B j l) ->
(\int[gauss n]_x (rmax (x *m A))%:E <= \int[gauss m]_y (rmax (y *m B))%:E)%E

Main result, as the README states it

Sudakov-Fernique inequality: for x of law gauss n and y of law gauss m, if each increment (x A)_j - (x A)_l has variance at most that of (y B)_j - (y B)_l, then E[max_j (x A)_j] <= E[max_j (y B)_j].

Statement as written in the source

Theorem sudakov_fernique n m k (A : 'M[R]_(n, k.+1)) (B : 'M[R]_(m, k.+1)) :
  (forall j l, incr_var A j l <= incr_var B j l) ->
  (\int[gauss n]_x (rmax (x *m A))%:E <= \int[gauss m]_y (rmax (y *m B))%:E)%E.

Used by 4 declarations in 4 files

GaussianAnalysis.random_matrix.goe_edge: goe_form_max_mean
this file: slepian
GaussianAnalysis.comparison.escape: bil_aux_max
GaussianAnalysis.comparison.sudakov: sudakov_minoration

corollary slepian main result source, line 471

forall {R : realType} [n m k : nat] [A : 'M_(n, k.+1)] [B : 'M_(m, k.+1)],
(forall j : 'I_k.+1, (A^T *m A) j j = (B^T *m B) j j) ->
(forall j l : 'I_k.+1, (B^T *m B) j l <= (A^T *m A) j l) ->
(\int[gauss n]_x (rmax (x *m A))%:E <= \int[gauss m]_y (rmax (y *m B))%:E)%E

Slepian's inequality for expected maxima: equal variances and larger covariances give a smaller expected maximum.

Main result, as the README states it

Slepian's inequality for expected maxima: if x A and y B have the same variances and each covariance of x A is at least that of y B, then E[max_j (x A)_j] <= E[max_j (y B)_j].

Statement as written in the source

Corollary slepian n m k (A : 'M[R]_(n, k.+1)) (B : 'M[R]_(m, k.+1)) :
  (forall j, (A^T *m A) j j = (B^T *m B) j j) ->
  (forall j l, (B^T *m B) j l <= (A^T *m A) j l) ->
  (\int[gauss n]_x (rmax (x *m A))%:E <= \int[gauss m]_y (rmax (y *m B))%:E)%E.

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.