GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysiscomparisonsudakov

Sudakov's minoration and the dual Sudakov inequality

GaussianAnalysis.comparison.sudakovlibrary/comparison/sudakov.v551 lines7 lemmas and theorems, 1 definitionsource
Imports 9 library modules and 29 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.trigo, 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 2

Two classical entropy bounds for Gaussian processes, with explicit constants, and the facts they rest on. g has law gauss n.

  • gauss_max_lower: the largest of n independent standard normal variables has mean at least sqrt (ln n) / 2 - 2.
  • sudakov_minoration (Sudakov): if the points xs i of 'rV[R]_n, i < k + 1, are pairwise at distance at least eps, then eps (sqrt (ln (k + 1)) / 2 - 2) <= sqrt 2 E max_i <g, xs i>. Proof: the Sudakov-Fernique inequality (slepian.v) against independent normal variables of variance eps^2 / 2, then gauss_max_lower.
  • gauss_shift_sym: for a measurable symmetric set A, gauss n (h + A) >= exp (- |h|^2 / 2) gauss n A, by the Cameron-Martin formula (gauss_shift.v) and cosh >= 1.
  • dual_sudakov (Pajor and Tomczak-Jaegermann, by Talagrand's argument): if nrm is a measurable seminorm with E nrm(g) <= L, the points of the Euclidean ball of radius r that are pairwise more than eps apart for nrm are at most 2 exp (8 r^2 L^2 / eps^2).
  • separated_net: if the eps-separated lists of points of a set K have at most M points, K has an eps-net of at most M of its own points, a separated list of largest size.

These two bounds replace volume arguments: covering.v covers the nuclear-norm ball by products of column balls with them.

separated dist K eps ss is a list of distinct points of K, pairwise more than eps apart for dist

Main results

ResultsStatement
sudakov_minorationgauss_max_lower
Sudakov's minoration: if xs i, i < k + 1, are pairwise at distance at least eps in 'rV[R]_n, then eps (sqrt (ln (k + 1)) / 2 - 2) <= sqrt 2 E max_i <g, xs i> for g of law gauss n; the maximum of n independent standard normal variables has mean at least sqrt (ln n) / 2 - 2.
dual_sudakovgauss_shift_symseparated_net
The dual Sudakov inequality of Pajor and Tomczak-Jaegermann (Talagrand's proof): for a measurable seminorm nrm with E nrm(g) <= L, the points of the Euclidean ball of radius r that are pairwise more than eps apart for nrm are at most 2 exp (8 r^2 L^2 / eps^2). gauss n (h + A) >= exp (- |h|^2 / 2) gauss n A for A measurable and symmetric. A set whose eps-separated lists have at most M points has an eps-net of at most M of its points.

Declarations8 exported, 1 local

lemma, theoremdefinitioninstancelocal
sectionseparated_net
Context {R : realType} {T : eqType}.
Variables (dist : T -> T -> R) (K : set T) (eps : R).
Hypothesis dist_sym : forall x y, dist x y = dist y x.
Hypothesis dist_refl : forall x, dist x x <= eps.
definition separated source, line 66
Type
forall {R : realType} {T : eqType}, (T -> T -> R) -> set T -> R -> seq T -> Prop
Definition
Definition separated (s : seq T) := [/\ uniq s, {subset s <= K} &
  forall x y, x \in s -> y \in s -> x != y -> eps < dist x y].

s is a list of distinct points of K, pairwise more than eps apart.

Used by 4 declarations in 2 files
lemma separated_net main result source, line 71 
forall {R : realType} {T : eqType} [dist : T -> T -> R] [K : set T] [eps : R],
(forall x y : T, dist x y = dist y x) ->
(forall x : T, dist x x <= eps) ->
forall [M : nat],
(forall s : seq T, separated dist K eps s -> (size s <= M)%N) ->
exists s : seq T,
  [/\ {subset s <= K}, (size s <= M)%N
    & forall x : T, K x -> exists2 y : T, y \in s & dist x y <= eps]

If the eps-separated lists of points of K have at most M points, K has an eps-net of at most M of its points: a separated list of largest size.

Main result

Stated in the README together with dual_sudakov.

Statement as written in the source
Lemma separated_net (M : nat) : (forall s, separated s -> (size s <= M)%N) ->
  exists s : seq T, [/\ {subset s <= K}, (size s <= M)%N &
    forall x, K x -> exists2 y, y \in s & dist x y <= eps].
Used by 1 declaration in 1 file
sectiongauss_max
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
lemma normal_prob_itv_ge source, line 107 
forall {R : realType} [t : R],
0 <= t -> ((expR (- ((t + 1) ^+ 2 / 2)) / 3)%:E <= normal_prob 0 1 `]t, (t + 1)%R])%E

A lower bound on the standard normal probability of ]t, t + 1].

Statement as written in the source
Lemma normal_prob_itv_ge (t : R) : 0 <= t ->
  ((expR (- ((t + 1) ^+ 2 / 2)) / 3)%:E <= N `]t, (t + 1)%R]%classic)%E.
Used by 1 declaration in 1 file
let mx_norm_frob section-local source, line 138 
Let mx_norm_frob m n' (B : 'M[R]_(m, n')) : `|B| <= frobenius B.
Used by 1 declaration in 1 file
theorem gauss_max_lower main result source, line 147 
forall {R : realType} (k : nat),
Num.ExtraDef.sqrtr (ln k.+1%:R) / 2 - 2 <= \int[gauss k.+1]_g rmax (g : 'rV_k.+1)

The largest of n independent standard normal variables has mean at least sqrt (ln n) / 2 - 2.

Main result

Stated in the README together with sudakov_minoration.

Statement as written in the source
Theorem gauss_max_lower k :
  Num.sqrt (ln k.+1%:R) / 2 - 2 <= \int[gauss k.+1]_g rmax (g : 'rV[R]_k.+1).
Used by 1 declaration in 1 file
sectionsudakov_minoration
Context {R : realType}.
lemma rmaxZ source, line 294 
forall {R : realType} [k : nat] [c : R] (z : 'rV_k.+1),
0 <= c -> rmax (c *: z) = c * rmax z
Statement as written in the source
Lemma rmaxZ k (c : R) (z : 'rV[R]_k.+1) : 0 <= c -> rmax (c *: z) = c * rmax z.
Used by 1 declaration in 1 file
theorem sudakov_minoration main result source, line 304 
forall {R : realType} [n k : nat] [xs : 'I_k.+1 -> 'rV_n] [eps : R],
0 <= eps ->
(forall i j : 'I_k.+1,
 i != j -> eps <= frobenius (xs i - xs j)) ->
eps * (Num.ExtraDef.sqrtr (ln k.+1%:R) / 2 - 2) <=
Num.ExtraDef.sqrtr 2 * \int[gauss n]_g rmax (\row_i mxdot g (xs i))

Sudakov's minoration: if the points xs i of 'rV[R]_n are pairwise at distance at least eps, then E max_i <g, xs i> is at least eps (sqrt (ln (k + 1)) / 2 - 2) / sqrt 2.

Main result, as the README states it

Sudakov's minoration: if xs i, i < k + 1, are pairwise at distance at least eps in 'rV[R]_n, then eps (sqrt (ln (k + 1)) / 2 - 2) <= sqrt 2 E max_i <g, xs i> for g of law gauss n; the maximum of n independent standard normal variables has mean at least sqrt (ln n) / 2 - 2.

Statement as written in the source
Theorem sudakov_minoration n k (xs : 'I_k.+1 -> 'rV[R]_n) (eps : R) :
  0 <= eps -> (forall i j, i != j -> eps <= frobenius (xs i - xs j)) ->
  eps * (Num.sqrt (ln k.+1%:R) / 2 - 2) <=
  Num.sqrt 2 * \int[gauss n]_g rmax (\row_i mxdot g (xs i)).
Used by 2 declarations in 2 files
sectiondual_sudakov
Context {R : realType} {n : nat}.
lemma gauss_shift_sym main result source, line 372 
forall {R : realType} {n : nat} [A : set 'rV_n] (h : 'rV_n),
(measure_matrix_display default_measure_display).-measurable A ->
(forall x : 'rV_n, A x -> A (- x)) ->
((expR (- (mxdot h h / 2)))%:E * gauss n A <= gauss n [set x | A (x - h)%R])%E

The Gaussian measure of a symmetric set decreases at most by the factor exp (- |h|^2 / 2) under the translation by h (Cameron-Martin).

Main result

Stated in the README together with dual_sudakov.

Statement as written in the source
Lemma gauss_shift_sym (A : set 'rV[R]_n) (h : 'rV[R]_n) : measurable A ->
  (forall x, A x -> A (- x)) ->
  ((expR (- (mxdot h h / 2)))%:E * gauss n A <=
   gauss n [set x | A (x - h)%R])%E.
Used by 1 declaration in 1 file
theorem dual_sudakov main result source, line 440 
forall {R : realType} {n : nat} [nrm : 'rV_n -> R] [r eps L : R] 
  [k : nat] [xs : 'I_k.+1 -> 'rV_n],
measurable_fun [set: 'rV_n] nrm ->
(forall x : 'rV[R]_n, nrm (- x) = nrm x) ->
(forall x y : 'rV[R]_n,
 nrm (x + y) <= nrm x + nrm y) ->
(forall (c : R) (x : 'rV[R]_n),
 0 <= c -> nrm (c *: x) = c * nrm x) ->
(gauss n).-integrable [set: 'rV_n] (EFin \o nrm) ->
0 < eps ->
0 < L ->
\int[gauss n]_g nrm g <= L ->
(forall i : 'I_k.+1, frobenius (xs i) <= r) ->
(forall i j : 'I_k.+1,
 i != j -> eps < nrm (xs i - xs j)) ->
k.+1%:R <= 2 * expR (8 * r ^+ 2 * L ^+ 2 / eps ^+ 2)

The dual Sudakov inequality of Pajor and Tomczak-Jaegermann, by Talagrand's argument: if nrm is a seminorm with E nrm(g) <= L, points of the Euclidean ball of radius r that are pairwise more than eps apart for nrm are at most 2 exp (8 r^2 L^2 / eps^2).

Main result, as the README states it

The dual Sudakov inequality of Pajor and Tomczak-Jaegermann (Talagrand's proof): for a measurable seminorm nrm with E nrm(g) <= L, the points of the Euclidean ball of radius r that are pairwise more than eps apart for nrm are at most 2 exp (8 r^2 L^2 / eps^2). gauss n (h + A) >= exp (- |h|^2 / 2) gauss n A for A measurable and symmetric. A set whose eps-separated lists have at most M points has an eps-net of at most M of its points.

Statement as written in the source
Theorem dual_sudakov (nrm : 'rV[R]_n -> R) (r eps L : R) k
    (xs : 'I_k.+1 -> 'rV[R]_n) :
  measurable_fun setT nrm ->
  (forall x, nrm (- x) = nrm x) ->
  (forall x y, nrm (x + y) <= nrm x + nrm y) ->
  (forall (c : R) x, 0 <= c -> nrm (c *: x) = c * nrm x) ->
  (gauss n).-integrable setT (EFin \o nrm) ->
  0 < eps -> 0 < L -> \int[gauss n]_g nrm g <= L ->
  (forall i, frobenius (xs i) <= r) ->
  (forall i j, i != j -> eps < nrm (xs i - xs j)) ->
  k.+1%:R <= 2 * expR (8 * r ^+ 2 * L ^+ 2 / eps ^+ 2).
Used by 1 declaration in 1 file
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.