GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysiscomparisongordon

Gordon's min-max inequality

GaussianAnalysis.comparison.gordonlibrary/comparison/gordon.v787 lines50 lemmas and theorems, 8 definitionssource
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 4
Required by 4 files of the paper proofs

Let x have law gauss n and y have law gauss m. For A : 'M[R]_(n, p.+1 * q.+1), X = vec_mx (x *m A) is a centered Gaussian matrix of size (p + 1) x (q + 1), whose entry X u t is the coordinate mxvec_index u t of x *m A; let Y = vec_mx (y *m B). Assume that each increment X u t - X u s within a row has a variance at most that of Y u t - Y u s, and that each increment X u t - X v s across two distinct rows has a variance at least that of Y u t - Y v s. Then E[minmax X] <= E[minmax Y], where minmax Z is the smallest over the rows of the largest entry of the row (gordon). With one row, this is the Sudakov-Fernique inequality. gordon_cov states the case of equal variances with covariances.

The proof applies Kahane's comparison inequality (gauss_comparison) to the soft min-max smm b. Its Hessian has zero row and column sums (smm_D2_rowsum, smm_D2_colsum), so its pairing with a matrix M only depends on the increments M i i + M j j - 2 * M i j (pairing_zero_sums). The Hessian is nonpositive inside a row and nonnegative across rows, which gives the sign (smm_hessian_sign). Since minmax Z - ln (p + 1) / b <= smm b z <= minmax Z + ln (q + 1) / b for Z = vec_mx z (le_smm, smm_le), letting b grow concludes.

minmax Zmin_u max_t Z u t, for Z : 'M[R]_(p.+1, q.+1)
gsum b z u\sum_t expR (b * z 0 (mxvec_index u t))
gtot b z\sum_u (gsum b z u)^-1
smm b z- b^-1 * ln (gtot b z), the soft min-max of vec_mx z
gq b z u(gsum b z u)^-1 / gtot b z, weights of the soft min
gp b z u texpR (b * z 0 (mxvec_index u t)) / gsum b z u, weights of the soft max of the row u
smm_D b z u tgq b z u * gp b z u t, the partial derivative of smm b along mxvec_index u t
smm_D2 b z u t v sthe partial derivative of z |-> smm_D b z u t along mxvec_index v s

Main results

ResultsStatementUsed by theories/
gordon
Gordon's min-max inequality: for x of law gauss n, y of law gauss m and the Gaussian matrices X = vec_mx (x A), Y = vec_mx (y B), if each increment X_ut - X_us within a row has variance at most that of Y_ut - Y_us, and each increment X_ut - X_vs across distinct rows has variance at least that of Y_ut - Y_vs, then E[min_u max_t X_ut] <= E[min_u max_t Y_ut].
gordon_cov
Gordon's inequality with equal variances: if the covariances of X are at least those of Y within each row and at most those of Y across rows, then E[min_u max_t X_ut] <= E[min_u max_t Y_ut].
pairing_zero_sumssmm_hessian_signle_smmsmm_le
If H has zero row and column sums, \sum_(i, j) M_ij H_ij = - 1/2 \sum_(i, j) H_ij (M_ii + M_jj - 2 M_ij). The soft min-max smm b z = - ln (\sum_u (\sum_t expR (b z_ut))^-1) / b is within ln (p + 1) / b below and ln (q + 1) / b above min_u max_t z_ut, and its Hessian is nonpositive within rows and nonnegative across rows.
mxvec_index_valsum_mxvec_index
mxvec_index i j is the row-major position i * n + j, and a sum over 'I_(m * n) is the double sum over the pairs (i, j).Gordon/Processes

Declarations58 exported, 6 local

lemma, theoremdefinitioninstancelocal
sectionmxvec_index
Context {m n : nat}.
lemma mxvec_index_eq source, line 68 
forall {m n : nat} (i i' : 'I_m) (j j' : 'I_n),
(mxvec_index i j == mxvec_index i' j') = (i == i') && (j == j')
Statement as written in the source
Lemma mxvec_index_eq (i i' : 'I_m) (j j' : 'I_n) :
  (mxvec_index i j == mxvec_index i' j') = (i == i') && (j == j').
Used by 2 declarations in 1 file
lemma mxvec_index_val main result source, line 77 
forall {m n : nat} (i : 'I_m) (j : 'I_n), (mxvec_index i j : nat) = (i * n + j)%N

mxvec_index is the row-major position.

Main result, as the README states it

mxvec_index i j is the row-major position i * n + j, and a sum over 'I_(m * n) is the double sum over the pairs (i, j).

Used in theories/ by: Gordon/Processes
Statement as written in the source
Lemma mxvec_index_val (i : 'I_m) (j : 'I_n) :
  (mxvec_index i j : nat) = (i * n + j)%N.
lemma sum_mxvec_index main result source, line 96 
forall {m n : nat} [V : GRing.Nmodule.Exports.nmodType] (f : 'I_(m * n) -> V),
\sum_k f k = \sum_i \sum_j f (mxvec_index i j)
Main result

Stated in the README together with mxvec_index_val.

Statement as written in the source
Lemma sum_mxvec_index (V : nmodType) (f : 'I_(m * n) -> V) :
  \sum_k f k = \sum_i \sum_j f (mxvec_index i j).
Used by 8 declarations in 4 files
sectionminmax
Context {R : realType} {p q : nat}.
Implicit Types Z : 'M[R]_(p.+1, q.+1).
definition minmax source, line 111
Type
forall {R : realType} {p q : nat}, 'M_(p.+1, q.+1) -> R
Definition
Definition minmax Z : R := - rmax (\row_u (- rmax (row u Z))).

The smallest of the largest entries of the rows of Z.

Used by 25 declarations in 3 files
lemma minmax_le source, line 113 
forall {R : realType} {p q : nat} (Z : 'M_(p.+1, q.+1)) (u : 'I_p.+1),
minmax Z <= rmax (row u Z)
Statement as written in the source
Lemma minmax_le Z u : minmax Z <= rmax (row u Z).
Used by 3 declarations in 2 files
lemma le_minmax source, line 119 
forall {R : realType} {p q : nat} [Z : 'M_(p.+1, q.+1)] [c : R],
(forall u : 'I_p.+1, c <= rmax (row u Z)) -> c <= minmax Z
Statement as written in the source
Lemma le_minmax Z c : (forall u, c <= rmax (row u Z)) -> c <= minmax Z.
Used by 1 declaration in 1 file
lemma rmax_leD source, line 124 
forall {R : realType} [k : nat] [z z' : 'rV_k.+1] [d : R],
(forall j : 'I_k.+1, z 0 j <= z' 0 j + d) -> rmax z <= rmax z' + d
Statement as written in the source
Lemma rmax_leD k (z z' : 'rV[R]_k.+1) d :
  (forall j, z 0 j <= z' 0 j + d) -> rmax z <= rmax z' + d.
Used by 4 declarations in 2 files
lemma minmax_leD source, line 128 
forall {R : realType} {p q : nat} [Z Z' : 'M_(p.+1, q.+1)] [d : R],
(forall (u : 'I_p.+1) (t : 'I_q.+1), Z u t <= Z' u t + d) -> minmax Z <= minmax Z' + d
Statement as written in the source
Lemma minmax_leD Z Z' d :
  (forall u t, Z u t <= Z' u t + d) -> minmax Z <= minmax Z' + d.
Used by 1 declaration in 1 file
lemma minmax_lipschitz source, line 140 
forall {R : realType} {p q : nat} (Z Z' : 'M_(p.+1, q.+1)),
`|minmax Z - minmax Z'| <= `|Z - Z'|
Statement as written in the source
Lemma minmax_lipschitz Z Z' : `|minmax Z - minmax Z'| <= `|Z - Z'|.
Used by 3 declarations in 2 files
lemma continuous_minmax source, line 151 
forall {R : realType} {p q : nat}, continuous minmax
Statement as written in the source
Lemma continuous_minmax : continuous minmax.
Used by 1 declaration in 1 file
lemma minmax_norm source, line 158 
forall {R : realType} {p q : nat} (Z : 'M_(p.+1, q.+1)), `|minmax Z| <= `|Z|
Statement as written in the source
Lemma minmax_norm Z : `|minmax Z| <= `|Z|.
Used by 2 declarations in 1 file
lemma norm_vec_mx_le source, line 168 
forall {R : realType} {p q : nat} (z : 'rV_(p.+1 * q.+1)), `|vec_mx z| <= `|z|
Statement as written in the source
Lemma norm_vec_mx_le (z : 'rV[R]_(p.+1 * q.+1)) : `|vec_mx z| <= `|z|.
Used by 2 declarations in 1 file
sectioncontinuity_helpers
Context {R : realType} {n : nat}.
Implicit Types f g : 'rV[R]_n -> R.
local lemma contM not exported source, line 180 
forall {R : realType} {n : nat} [f g : 'rV_n -> R],
continuous f ->
continuous g ->
continuous
  (fun
     z : 'rV[R]_n =>
   f z * g z)
Statement as written in the source
Local Lemma contM f g : continuous f -> continuous g ->
  continuous (fun z => f z * g z).
Used by 4 declarations in 1 file
local lemma contD not exported source, line 186 
forall {R : realType} {n : nat} [f g : 'rV_n -> R],
continuous f ->
continuous g ->
continuous
  (fun
     z : 'rV[R]_n =>
   f z + g z)
Statement as written in the source
Local Lemma contD f g : continuous f -> continuous g ->
  continuous (fun z => f z + g z).
Used by 1 declaration in 1 file
local lemma contB not exported source, line 192 
forall {R : realType} {n : nat} [f g : 'rV_n -> R],
continuous f ->
continuous g ->
continuous
  (fun
     z : 'rV[R]_n =>
   f z - g z)
Statement as written in the source
Local Lemma contB f g : continuous f -> continuous g ->
  continuous (fun z => f z - g z).
Used by 1 declaration in 1 file
local lemma contC not exported source, line 198 
forall {R : realType} {n : nat} [c : R], continuous (fun=> c)
Statement as written in the source
Local Lemma contC (c : R) : continuous (fun _ : 'rV[R]_n => c).
Used by 1 declaration in 1 file
local lemma contV not exported source, line 201 
forall {R : realType} {n : nat} [f : 'rV_n -> R],
(forall z : 'rV_n, f z != 0) ->
continuous f ->
continuous
  (fun
     z : 'rV[R]_n =>
   (f z)^-1)
Statement as written in the source
Local Lemma contV f : (forall z, f z != 0) -> continuous f ->
  continuous (fun z => (f z)^-1).
Used by 3 declarations in 1 file
sectionsoft_minmax
Context {R : realType} {p q : nat}.
Variable b : R.
Local Notation N := (p.+1 * q.+1)%N.
Local Notation idx := (@mxvec_index p.+1 q.+1).
Implicit Types z : 'rV[R]_N.
definition gsum source, line 215
Type
forall {R : realType} {p q : nat}, R -> 'rV_(p.+1 * q.+1) -> 'I_p.+1 -> R
Definition
Definition gsum z u : R := \sum_t expR (b * z 0 (idx u t)).

The sum of the expR (b * z_(u, t)) over the block u.

Used by 11 declarations in 1 file
definition gtot source, line 217
Type
forall {R : realType} {p q : nat}, R -> 'rV_(p.+1 * q.+1) -> R
Definition
Definition gtot z : R := \sum_u (gsum z u)^-1.
Used by 8 declarations in 1 file
definition smm source, line 220
Type
forall {R : realType} {p q : nat}, R -> 'rV_(p.+1 * q.+1) -> R
Definition
Definition smm z : R := - (b^-1 * ln (gtot z)).

The soft min-max of z: - b^-1 * ln (\sum_u (gsum z u)^-1).

Used by 11 declarations in 1 file
definition gq source, line 224
Type
forall {R : realType} {p q : nat}, R -> 'rV_(p.+1 * q.+1) -> 'I_p.+1 -> R
Definition
Definition gq z u : R := (gsum z u)^-1 / gtot z.

The weights of the soft minimum over the blocks, and of the soft maxima within each block.

Used by 10 declarations in 1 file
definition gp source, line 226
Type
forall {R : realType} {p q : nat}, R -> 'rV_(p.+1 * q.+1) -> 'I_p.+1 -> 'I_q.+1 -> R
Definition
Definition gp z u t : R := expR (b * z 0 (idx u t)) / gsum z u.
Used by 13 declarations in 1 file
definition smm_D source, line 229
Type
forall {R : realType} {p q : nat}, R -> 'rV_(p.+1 * q.+1) -> 'I_p.+1 -> 'I_q.+1 -> R
Definition
Definition smm_D z u t : R := gq z u * gp z u t.

The first and second partial derivatives of smm.

Used by 13 declarations in 1 file
definition smm_D2 source, line 231
Type
forall {R : realType} {p q : nat},
R ->
'rV_(p.+1 * q.+1) ->
'I_p.+1 ->
'I_q.+1 ->
'I_p.+1 ->
'I_q.+1 -> R
Definition
Definition smm_D2 z u t v s : R :=
  b * ((u == v)%:R * (t == s)%:R * smm_D z u t
       - 2 * (u == v)%:R * smm_D z u t * gp z v s + smm_D z u t * smm_D z v s).
Used by 8 declarations in 1 file
lemma gsum_gt0 source, line 235 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) (u : 'I_p.+1),
0 < gsum b z u
Statement as written in the source
Lemma gsum_gt0 z u : 0 < gsum z u.
Used by 11 declarations in 1 file
lemma gtot_gt0 source, line 238 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)), 0 < gtot b z
Statement as written in the source
Lemma gtot_gt0 z : 0 < gtot z.
Used by 5 declarations in 1 file
lemma gq_ge0 source, line 244 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) (u : 'I_p.+1),
0 <= gq b z u
Statement as written in the source
Lemma gq_ge0 z u : 0 <= gq z u.
Used by 3 declarations in 1 file
lemma gp_ge0 source, line 250 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) 
  (u : 'I_p.+1) (t : 'I_q.+1),
0 <= gp b z u t
Statement as written in the source
Lemma gp_ge0 z u t : 0 <= gp z u t.
Used by 5 declarations in 1 file
lemma gq_sum source, line 253 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)), \sum_u gq b z u = 1
Statement as written in the source
Lemma gq_sum z : \sum_u gq z u = 1.
Used by 4 declarations in 1 file
lemma gp_sum source, line 256 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) (u : 'I_p.+1),
\sum_t gp b z u t = 1
Statement as written in the source
Lemma gp_sum z u : \sum_t gp z u t = 1.
Used by 4 declarations in 1 file
lemma gq_le1 source, line 259 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) (u : 'I_p.+1),
gq b z u <= 1
Statement as written in the source
Lemma gq_le1 z u : gq z u <= 1.
Used by 2 declarations in 1 file
lemma gp_le1 source, line 264 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) 
  (u : 'I_p.+1) (t : 'I_q.+1),
gp b z u t <= 1
Statement as written in the source
Lemma gp_le1 z u t : gp z u t <= 1.
Used by 2 declarations in 1 file
lemma smm_D_ge0 source, line 269 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) 
  (u : 'I_p.+1) (t : 'I_q.+1),
0 <= smm_D b z u t
Statement as written in the source
Lemma smm_D_ge0 z u t : 0 <= smm_D z u t.
Used by 2 declarations in 1 file
lemma smm_D_le1 source, line 272 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) 
  (u : 'I_p.+1) (t : 'I_q.+1),
smm_D b z u t <= 1
Statement as written in the source
Lemma smm_D_le1 z u t : smm_D z u t <= 1.
Used by 1 declaration in 1 file
lemma smm_D_sum source, line 277 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)),
\sum_u \sum_t smm_D b z u t = 1
Statement as written in the source
Lemma smm_D_sum z : \sum_u \sum_t smm_D z u t = 1.
lemma is_derive_gsum source, line 283 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) 
  (u v : 'I_p.+1) (s : 'I_q.+1),
is_derive z (delta_mx 0 (mxvec_index v s)) ((gsum b)^~ u)
  ((u == v)%:R * (b * expR (b * z 0 (mxvec_index v s))))
Statement as written in the source
Lemma is_derive_gsum z u v s :
  is_derive z (delta_mx 0 (idx v s)) (gsum ^~ u)
    ((u == v)%:R * (b * expR (b * z 0 (idx v s)))).
Used by 2 declarations in 1 file
lemma is_derive_gtot source, line 299 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) 
  (v : 'I_p.+1) (s : 'I_q.+1),
is_derive z (delta_mx 0 (mxvec_index v s)) (gtot b)
  (- (gsum b z v ^- 2 * (b * expR (b * z 0 (mxvec_index v s)))))
Statement as written in the source
Lemma is_derive_gtot z v s :
  is_derive z (delta_mx 0 (idx v s)) gtot
    (- ((gsum z v) ^- 2 * (b * expR (b * z 0 (idx v s))))).
Used by 2 declarations in 1 file
lemma is_derive_gsumV source, line 315 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) 
  (u v : 'I_p.+1) (s : 'I_q.+1),
is_derive z (delta_mx 0 (mxvec_index v s)) ((fun x : R => (id x)^-1) \o (gsum b)^~ u)
  ((- gsum b z u ^- 2)%:A * ((u == v)%:R * (b * expR (b * z 0 (mxvec_index v s)))))

The derivative of the inverse of gsum z u along the direction (v, s).

Statement as written in the source
Lemma is_derive_gsumV z u v s :
  is_derive z (delta_mx 0 (idx v s)) ((fun x : R => (id x)^-1) \o gsum ^~ u)
    ((- (gsum z u) ^- 2)%:A * ((u == v)%:R * (b * expR (b * z 0 (idx v s))))).
Used by 1 declaration in 1 file
lemma is_derive_smm_D source, line 323 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1)) 
  (u : 'I_p.+1) (t : 'I_q.+1) (v : 'I_p.+1) (s : 'I_q.+1),
is_derive z (delta_mx 0 (mxvec_index v s)) (fun z0 : 'rV_(p.+1 * q.+1) => smm_D b z0 u t)
  (smm_D2 b z u t v s)
Statement as written in the source
Lemma is_derive_smm_D z u t v s :
  is_derive z (delta_mx 0 (idx v s)) ((fun z => smm_D z u t)) (smm_D2 z u t v s).
Used by 2 declarations in 1 file
lemma continuous_gsum source, line 344 
forall {R : realType} {p q : nat} [b : R] [u : 'I_p.+1], continuous ((gsum b)^~ u)
Statement as written in the source
Lemma continuous_gsum u : continuous (gsum ^~ u).
Used by 3 declarations in 1 file
lemma continuous_gtot source, line 347 
forall {R : realType} {p q : nat} [b : R], continuous (gtot b)
Statement as written in the source
Lemma continuous_gtot : continuous gtot.
Used by 1 declaration in 1 file
lemma continuous_gq source, line 353 
forall {R : realType} {p q : nat} [b : R] [u : 'I_p.+1], continuous ((gq b)^~ u)
Statement as written in the source
Lemma continuous_gq u : continuous (gq ^~ u).
Used by 1 declaration in 1 file
lemma continuous_gp source, line 360 
forall {R : realType} {p q : nat} [b : R] [u : 'I_p.+1] [t : 'I_q.+1],
continuous (fun z : 'rV_(p.+1 * q.+1) => gp b z u t)
Statement as written in the source
Lemma continuous_gp u t : continuous ((fun z => gp z u t)).
Used by 2 declarations in 1 file
lemma continuous_smm_D source, line 367 
forall {R : realType} {p q : nat} [b : R] [u : 'I_p.+1] [t : 'I_q.+1],
continuous (fun z : 'rV_(p.+1 * q.+1) => smm_D b z u t)
Statement as written in the source
Lemma continuous_smm_D u t : continuous ((fun z => smm_D z u t)).
Used by 2 declarations in 1 file
lemma continuous_smm_D2 source, line 374 
forall {R : realType} {p q : nat} [b : R]
  [u : 'I_p.+1]
  [t : 'I_q.+1]
  [v : 'I_p.+1]
  [s : 'I_q.+1],
continuous (fun z : 'rV_(p.+1 * q.+1) => smm_D2 b z u t v s)
Statement as written in the source
Lemma continuous_smm_D2 u t v s : continuous ((fun z => smm_D2 z u t v s)).
Used by 2 declarations in 1 file
lemma smm_D_differentiable source, line 386 
forall {R : realType} {p q : nat} (b : R) (u : 'I_p.+1) (t : 'I_q.+1)
  (z : 'rV_(p.+1 * q.+1)),
differentiable ((fun z0 : 'rV_(p.+1 * q.+1) => smm_D b z0 u t) : 'rV_(p.+1 * q.+1) -> R^o)
  z
Statement as written in the source
Lemma smm_D_differentiable u t z :
  differentiable ((fun z => smm_D z u t) : 'rV[R]_N -> R^o) z.
Used by 1 declaration in 1 file
local lemma sum_delta not exported source, line 399 
forall {R : realType} [I : finType] (i : I) (F : I -> R), \sum_j (i == j)%:R * F j = F i
Statement as written in the source
Local Lemma sum_delta (I : finType) (i : I) (F : I -> R) :
  \sum_j (i == j)%:R * F j = F i.
Used by 2 declarations in 1 file
lemma smm_D2_rowsum source, line 406 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1))
  (u : 'I_p.+1)
  (t : 'I_q.+1),
\sum_v \sum_s smm_D2 b z u t v s = 0
Statement as written in the source
Lemma smm_D2_rowsum z u t : \sum_v \sum_s smm_D2 z u t v s = 0.
Used by 1 declaration in 1 file
lemma smm_D2_colsum source, line 427 
forall {R : realType} {p q : nat} (b : R) (z : 'rV_(p.+1 * q.+1))
  (v : 'I_p.+1)
  (s : 'I_q.+1),
\sum_u \sum_t smm_D2 b z u t v s = 0
Statement as written in the source
Lemma smm_D2_colsum z v s : \sum_u \sum_t smm_D2 z u t v s = 0.
Used by 1 declaration in 1 file
sectionsoft_minmax_b0
Hypothesis b0 : 0 < b.
lemma smm_lse source, line 460 
forall {R : realType} {p q : nat} [b : R],
0 < b ->
forall z : 'rV_(p.+1 * q.+1), smm b z = - lse b (\row_u - lse b (row u (vec_mx z)))
Statement as written in the source
Lemma smm_lse z : smm z = - lse b (\row_u (- lse b (row u (vec_mx z)))).
Used by 2 declarations in 1 file
lemma smm_le main result source, line 470 
forall {R : realType} {p q : nat} [b : R],
0 < b -> forall z : 'rV_(p.+1 * q.+1), smm b z <= minmax (vec_mx z) + ln q.+1%:R / b
Main result

Stated in the README together with pairing_zero_sums.

Statement as written in the source
Lemma smm_le z : smm z <= minmax (vec_mx z) + ln q.+1%:R / b.
Used by 2 declarations in 1 file
lemma le_smm main result source, line 481 
forall {R : realType} {p q : nat} [b : R],
0 < b -> forall z : 'rV_(p.+1 * q.+1), minmax (vec_mx z) - ln p.+1%:R / b <= smm b z
Main result

Stated in the README together with pairing_zero_sums.

Statement as written in the source
Lemma le_smm z : minmax (vec_mx z) - ln p.+1%:R / b <= smm z.
Used by 2 declarations in 1 file
lemma is_derive_smm source, line 491 
forall {R : realType} {p q : nat} [b : R],
0 < b ->
forall (z : 'rV_(p.+1 * q.+1)) (v : 'I_p.+1) (s : 'I_q.+1),
is_derive z (delta_mx 0 (mxvec_index v s)) (smm b) (smm_D b z v s)
Statement as written in the source
Lemma is_derive_smm z v s :
  is_derive z (delta_mx 0 (idx v s)) smm (smm_D z v s).
Used by 2 declarations in 1 file
lemma smm_DE source, line 503 
forall {R : realType} {p q : nat} [b : R],
0 < b ->
forall (v : 'I_p.+1) (s : 'I_q.+1),
'D_(delta_mx 0 (mxvec_index v s)) (smm b) = (fun z : 'rV_(p.+1 * q.+1) => smm_D b z v s)
Statement as written in the source
Lemma smm_DE v s :
  'D_(delta_mx 0 (idx v s)) smm = (fun z => smm_D z v s) :> ('rV[R]_N -> R).
Used by 3 declarations in 1 file
lemma smm_D2E source, line 507 
forall {R : realType} {p q : nat} [b : R],
0 < b ->
forall (u : 'I_p.+1) (t : 'I_q.+1) (v : 'I_p.+1) (s : 'I_q.+1),
'D_(delta_mx 0 (mxvec_index v s)) ('D_(delta_mx 0 (mxvec_index u t)) (smm b)) =
(fun z : 'rV_(p.+1 * q.+1) => smm_D2 b z u t v s)
Statement as written in the source
Lemma smm_D2E u t v s :
  'D_(delta_mx 0 (idx v s)) ('D_(delta_mx 0 (idx u t)) smm) =
  (fun z => smm_D2 z u t v s) :> ('rV[R]_N -> R).
Used by 2 declarations in 1 file
lemma smm_differentiable source, line 515 
forall {R : realType} {p q : nat} [b : R],
0 < b -> forall z : 'rV_(p.+1 * q.+1), differentiable (smm b : 'rV_(p.+1 * q.+1) -> R^o) z
Statement as written in the source
Lemma smm_differentiable z : differentiable (smm : 'rV[R]_N -> R^o) z.
Used by 2 declarations in 1 file
sectionpairing
Context {R : realType}.
lemma pairing_zero_sums main result source, line 532 
forall {R : realType} [n : nat] (M : 'I_n -> 'I_n -> R) [H : 'I_n -> 'I_n -> R],
(forall i : 'I_n, \sum_j H i j = 0) ->
(forall j : 'I_n, \sum_i H i j = 0) ->
\sum_i \sum_j M i j * H i j = - 2^-1 * \sum_i \sum_j H i j * (M i i + M j j - 2 * M i j)

If H has zero row and column sums, its pairing with M only depends on the increments M i i + M j j - 2 * M i j.

Main result, as the README states it

If H has zero row and column sums, \sum_(i, j) M_ij H_ij = - 1/2 \sum_(i, j) H_ij (M_ii + M_jj - 2 M_ij). The soft min-max smm b z = - ln (\sum_u (\sum_t expR (b z_ut))^-1) / b is within ln (p + 1) / b below and ln (q + 1) / b above min_u max_t z_ut, and its Hessian is nonpositive within rows and nonnegative across rows.

Statement as written in the source
Lemma pairing_zero_sums (n : nat) (M H : 'I_n -> 'I_n -> R) :
  (forall i, \sum_j H i j = 0) -> (forall j, \sum_i H i j = 0) ->
  \sum_i \sum_j M i j * H i j =
  - 2^-1 * \sum_i \sum_j H i j * (M i i + M j j - 2 * M i j).
Used by 1 declaration in 1 file
sectionsmm_hessian
Context {R : realType} {p q : nat}.
Variable b : R.
Hypothesis b0 : 0 < b.
Local Notation N := (p.+1 * q.+1)%N.
Local Notation idx := (@mxvec_index p.+1 q.+1).
lemma smm_hessian_sign main result source, line 563 
forall {R : realType} {p q : nat} [b : R],
0 < b ->
forall (z : 'rV[R]_(p.+1 * q.+1))
  [Dl : 'I_(p.+1 * q.+1) -> 'I_(p.+1 * q.+1) -> R],
(forall j : 'I_(p.+1 * q.+1), Dl j j = 0) ->
(forall (u : 'I_p.+1) (t s : 'I_q.+1), Dl (mxvec_index u t) (mxvec_index u s) <= 0) ->
(forall (u v : 'I_p.+1) (t s : 'I_q.+1),
 u != v -> 0 <= Dl (mxvec_index u t) (mxvec_index v s)) ->
0 <= \sum_j \sum_l 'D_(delta_mx 0 l) ('D_(delta_mx 0 j) (smm b)) z * Dl j l

The pairing of the Hessian of smm b with a matrix that vanishes on the diagonal, is nonpositive inside the blocks and nonnegative across them, is nonnegative.

Main result

Stated in the README together with pairing_zero_sums.

Statement as written in the source
Lemma smm_hessian_sign z (Dl : 'I_N -> 'I_N -> R) :
  (forall j, Dl j j = 0) ->
  (forall u t s, Dl (idx u t) (idx u s) <= 0) ->
  (forall u v t s, u != v -> 0 <= Dl (idx u t) (idx v s)) ->
  0 <= \sum_j \sum_l 'D_(delta_mx 0 l) ('D_(delta_mx 0 j) (smm b)) z * Dl j l.
Used by 1 declaration in 1 file
sectiongordon
Context {R : realType}.
lemma continuous_vec_mx source, line 592 
forall {R : realType} [p q : nat], continuous vec_mx
Statement as written in the source
Lemma continuous_vec_mx p q : continuous (@vec_mx R p q).
Used by 1 declaration in 1 file
lemma integrable_gauss_minmax source, line 598 
forall {R : realType} [n p q : nat] (A : 'M_(n, p.+1 * q.+1)),
(gauss n).-integrable [set: 'rV_n] (EFin \o (fun x : 'rV_n => minmax (vec_mx (x *m A))))
Statement as written in the source
Lemma integrable_gauss_minmax n p q (A : 'M[R]_(n, p.+1 * q.+1)) :
  (gauss n).-integrable [set: 'rV[R]_n]
    (EFin \o (fun x => minmax (vec_mx (x *m A)))).
Used by 3 declarations in 2 files
lemma smm_norm source, line 617 
forall {R : realType} [p q : nat] [b : R] (z : 'rV_(p.+1 * q.+1)),
0 < b -> `|smm b z| <= `|z| + (ln p.+1%:R + ln q.+1%:R) / b
Statement as written in the source
Lemma smm_norm p q (b : R) (z : 'rV[R]_(p.+1 * q.+1)) : 0 < b ->
  `|smm b z| <= `|z| + (ln p.+1%:R + ln q.+1%:R) / b.
Used by 2 declarations in 1 file
lemma integrable_gauss_smm source, line 628 
forall {R : realType} [n p q : nat] [b : R] (A : 'M_(n, p.+1 * q.+1)),
0 < b -> (gauss n).-integrable [set: 'rV_n] (EFin \o (fun x : 'rV_n => smm b (x *m A)))
Statement as written in the source
Lemma integrable_gauss_smm n p q (b : R) (A : 'M[R]_(n, p.+1 * q.+1)) :
  0 < b -> (gauss n).-integrable [set: 'rV[R]_n] (EFin \o (fun x => smm b (x *m A))).
Used by 1 declaration in 1 file
theorem gordon main result source, line 648 
forall {R : realType} [n m p q : nat] [A : 'M_(n, p.+1 * q.+1)] [B : 'M_(m, p.+1 * q.+1)],
(forall (u : 'I_p.+1) (t s : 'I_q.+1),
 incr_var A (mxvec_index u t) (mxvec_index u s) <=
 incr_var B (mxvec_index u t) (mxvec_index u s)) ->
(forall (u v : 'I_p.+1) (t s : 'I_q.+1),
 u != v ->
 incr_var B (mxvec_index u t) (mxvec_index v s) <=
 incr_var A (mxvec_index u t) (mxvec_index v s)) ->
(\int[gauss n]_x (minmax (vec_mx (x *m A)))%:E <=
 \int[gauss m]_y (minmax (vec_mx (y *m B)))%:E)%E

Gordon's inequality for expected min-max: the rows u of vec_mx (x *m A) and vec_mx (y *m B) are the blocks.

Main result, as the README states it

Gordon's min-max inequality: for x of law gauss n, y of law gauss m and the Gaussian matrices X = vec_mx (x A), Y = vec_mx (y B), if each increment X_ut - X_us within a row has variance at most that of Y_ut - Y_us, and each increment X_ut - X_vs across distinct rows has variance at least that of Y_ut - Y_vs, then E[min_u max_t X_ut] <= E[min_u max_t Y_ut].

Statement as written in the source
Theorem gordon n m p q (A : 'M[R]_(n, p.+1 * q.+1)) (B : 'M[R]_(m, p.+1 * q.+1)) :
  (forall u t s, incr_var A (mxvec_index u t) (mxvec_index u s) <=
                 incr_var B (mxvec_index u t) (mxvec_index u s)) ->
  (forall u v t s, u != v ->
     incr_var B (mxvec_index u t) (mxvec_index v s) <=
     incr_var A (mxvec_index u t) (mxvec_index v s)) ->
  (\int[gauss n]_x (minmax (vec_mx (x *m A)))%:E <=
   \int[gauss m]_y (minmax (vec_mx (y *m B)))%:E)%E.
Used by 4 declarations in 3 files
corollary gordon_cov main result source, line 771 
forall {R : realType} [n m p q : nat] [A : 'M_(n, p.+1 * q.+1)] [B : 'M_(m, p.+1 * q.+1)],
(forall j : 'I_(p.+1 * q.+1), (A^T *m A) j j = (B^T *m B) j j) ->
(forall (u : 'I_p.+1) (t s : 'I_q.+1),
 (B^T *m B) (mxvec_index u t) (mxvec_index u s) <=
 (A^T *m A) (mxvec_index u t) (mxvec_index u s)) ->
(forall (u v : 'I_p.+1) (t s : 'I_q.+1),
 u != v ->
 (A^T *m A) (mxvec_index u t) (mxvec_index v s) <=
 (B^T *m B) (mxvec_index u t) (mxvec_index v s)) ->
(\int[gauss n]_x (minmax (vec_mx (x *m A)))%:E <=
 \int[gauss m]_y (minmax (vec_mx (y *m B)))%:E)%E

Gordon's inequality with equal variances: larger covariances inside the rows and smaller covariances across rows give a smaller expected min-max.

Main result, as the README states it

Gordon's inequality with equal variances: if the covariances of X are at least those of Y within each row and at most those of Y across rows, then E[min_u max_t X_ut] <= E[min_u max_t Y_ut].

Statement as written in the source
Corollary gordon_cov n m p q (A : 'M[R]_(n, p.+1 * q.+1))
    (B : 'M[R]_(m, p.+1 * q.+1)) :
  (forall j, (A^T *m A) j j = (B^T *m B) j j) ->
  (forall u t s, (B^T *m B) (mxvec_index u t) (mxvec_index u s) <=
                 (A^T *m A) (mxvec_index u t) (mxvec_index u s)) ->
  (forall u v t s, u != v ->
     (A^T *m A) (mxvec_index u t) (mxvec_index v s) <=
     (B^T *m B) (mxvec_index u t) (mxvec_index v s)) ->
  (\int[gauss n]_x (minmax (vec_mx (x *m A)))%:E <=
   \int[gauss m]_y (minmax (vec_mx (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.