GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisprobabilityrademacher_lindeberg

Lindeberg's replacement of uniform signs by Gaussians

GaussianAnalysis.probability.rademacher_lindeberglibrary/probability/rademacher_lindeberg.v523 lines15 lemmas and theorems, 2 definitionssource
Imports 5 library modules and 26 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.algebra.interval, 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_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.numfun, mathcomp.analysis.measurable_realfun, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 1

For a bounded measurable F : 'rV[R]_n -> R whose third derivative along the coordinate j is at most c_j in absolute value, the average of F over the 2^n rows of signs and its integral against gauss n differ by at most (1/2) \sum_j c_j (rademacher_gauss_lindeberg). This is the coordinate-replacement form of the Lindeberg principle (Chatterjee, 'A generalization of the Lindeberg principle', Ann. Probab. 34 (2006), Theorem 1.1) for uniform signs and standard Gaussians, which have the same first two moments.

Part of target T6 of phase 12: a Rocq formalization of the credited argument of the first paragraph of the proof of Theorem ext:sign of 'The free energy of the Ising random perceptron' (family 222 of the OpenAI math collection, revision 1581d4cbd, sections/extensions.tex). The collection has no Lean version of it.

The coordinates are replaced one at a time, by induction on n: Fubini along rV_cons for gauss n.+1 (Rintegral_gauss_cons) and the decomposition of the rows of signs by their first coordinate (sum_sign_rowS). In one coordinate, Taylor's formula of order two and the first two moments give the constant (1 + E |g|^3) / 6 <= 1/2.

Proved:

sign_row sthe row of the signs (if s i then 1 else -1) of s : {ffun 'I_n -> bool}
ffun_cons b sthe function on 'I_n.+1 with value b at 0 and s on the other indices

Main results

ResultsStatement
rademacher_gauss_lindeberg
Lindeberg's replacement of uniform signs by Gaussians (Chatterjee 2006, Theorem 1.1, for signs and standard Gaussians): if F : 'rV[R]_n -> R is measurable and bounded, and for every x and j the map t |-> F (t e_j + x) has three derivatives with the third at most c_j in absolute value, then the average of F over the 2^n rows of signs and its integral against gauss n differ by at most (1/2) sum_j c_j. By induction on n, with Fubini along rV_cons for bounded measurable functions (Rintegral_gauss_cons) and the decomposition of the rows of signs by their first coordinate (sum_sign_rowS).
derive_le_cmptaylor2_lerademacher_gauss_stepRintegral_normal_quadraticRintegral_normal_abs3
The mean value inequality |g b - g a| <= k b - k a for a <= b and g, k differentiable everywhere with |g'| <= k' on [a, b], and Taylor's formula of order two: |f t - f 0 - f'(0) t - f''(0) t^2 / 2| <= c |t|^3 / 6 when |f'''| <= c everywhere. In one coordinate, |(f 1 + f (-1)) / 2 - E f(g)| <= c / 2 for g of law N(0, 1), from E (a + b g + c g^2) = a + c and E |g|^3 <= 2.

Declarations17 exported

lemma, theoremdefinitioninstancelocal
sectiontaylor2
Context {R : realType}.
lemma is_derive_continuous source, line 70 
forall {R : realType} [f f' : R -> R],
(forall u : R, is_derive u 1 f (f' u)) -> continuous f
Statement as written in the source
Lemma is_derive_continuous (f f' : R -> R) :
  (forall u : R, is_derive u 1 f (f' u)) -> continuous f.
Used by 3 declarations in 2 files
lemma derive_le_cmp main result source, line 79 
forall {R : realType} [g g' k k' : R -> R] [a b : R],
a <= b ->
(forall u : R, is_derive u 1 g (g' u)) ->
(forall u : R, is_derive u 1 k (k' u)) ->
(forall u : R, a <= u -> u <= b -> `|g' u| <= k' u) -> `|g b - g a| <= k b - k a

The mean value inequality with a comparison function: if |g'| <= k' on [a, b], then |g b - g a| <= k b - k a.

Main result, as the README states it

The mean value inequality |g b - g a| <= k b - k a for a <= b and g, k differentiable everywhere with |g'| <= k' on [a, b], and Taylor's formula of order two: |f t - f 0 - f'(0) t - f''(0) t^2 / 2| <= c |t|^3 / 6 when |f'''| <= c everywhere. In one coordinate, |(f 1 + f (-1)) / 2 - E f(g)| <= c / 2 for g of law N(0, 1), from E (a + b g + c g^2) = a + c and E |g|^3 <= 2.

Statement as written in the source
Lemma derive_le_cmp (g g' k k' : R -> R) (a b : R) : a <= b ->
  (forall u : R, is_derive u 1 g (g' u)) ->
  (forall u : R, is_derive u 1 k (k' u)) ->
  (forall u, a <= u -> u <= b -> `|g' u| <= k' u) ->
  `|g b - g a| <= k b - k a.
Used by 1 declaration in 1 file
lemma taylor2_le main result source, line 108 
forall {R : realType} [f f1 f2 f3 : R -> R] [c : R],
(forall t : R, is_derive t 1 f (f1 t)) ->
(forall t : R, is_derive t 1 f1 (f2 t)) ->
(forall t : R, is_derive t 1 f2 (f3 t)) ->
(forall t : R, `|f3 t| <= c) ->
forall t : R, `|f t - f 0 - f1 0 * t - f2 0 * t ^+ 2 / 2| <= c * `|t| ^+ 3 / 6

Taylor's formula of order two, with a bound c on the third derivative.

Main result

Stated in the README together with derive_le_cmp.

Statement as written in the source
Lemma taylor2_le (f f1 f2 f3 : R -> R) (c : R) :
  (forall t : R, is_derive t 1 f (f1 t)) ->
  (forall t : R, is_derive t 1 f1 (f2 t)) ->
  (forall t : R, is_derive t 1 f2 (f3 t)) -> (forall t, `|f3 t| <= c) ->
  forall t, `|f t - f 0 - f1 0 * t - f2 0 * t ^+ 2 / 2| <= c * `|t| ^+ 3 / 6.
Used by 1 declaration in 1 file
sectionrademacher_gauss_step
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
lemma integrable_normal_affine source, line 172 
forall {R : realType} (a b : R),
(normal_prob 0 1).-integrable [set: R] (EFin \o (fun t : R => a + b * t))
Statement as written in the source
Lemma integrable_normal_affine (a b : R) :
  N.-integrable [set: R] (EFin \o (fun t => a + b * t)).
Used by 1 declaration in 1 file
lemma integrable_normal_sqr source, line 181 
forall {R : realType} (a : R),
(normal_prob 0 1).-integrable [set: R] (EFin \o (fun t : R => a * t ^+ 2))
Statement as written in the source
Lemma integrable_normal_sqr (a : R) :
  N.-integrable [set: R] (EFin \o (fun t => a * t ^+ 2)).
Used by 1 declaration in 1 file
lemma Rintegral_normal_quadratic main result source, line 190 
forall {R : realType} (a b c : R), \int[normal_prob 0 1]_t (a + b * t + c * t ^+ 2) = a + c

E (a + b g + c g^2) = a + c for g of law N(0, 1).

Main result

Stated in the README together with derive_le_cmp.

Statement as written in the source
Lemma Rintegral_normal_quadratic (a b c : R) :
  \int[N]_t (a + b * t + c * t ^+ 2) = a + c.
Used by 1 declaration in 1 file
lemma Rintegral_normal_abs3 main result source, line 216 
forall {R : realType}, \int[normal_prob 0 1]_t `|t| ^+ 3 <= 2

E |g|^3 <= 2, from |t|^3 <= (t^2 + t^4) / 2.

Main result

Stated in the README together with derive_le_cmp.

Statement as written in the source
Lemma Rintegral_normal_abs3 : \int[N]_t `|t| ^+ 3 <= 2.
Used by 1 declaration in 1 file
lemma rademacher_gauss_step main result source, line 260 
forall {R : realType} [f f1 f2 f3 : R -> R] [c : R],
(forall t : R, is_derive t 1 f (f1 t)) ->
(forall t : R, is_derive t 1 f1 (f2 t)) ->
(forall t : R, is_derive t 1 f2 (f3 t)) ->
(forall t : R, `|f3 t| <= c) ->
`|(f 1 + f (-1)) / 2 - \int[normal_prob 0 1]_t f t| <= c / 2

One coordinate: if |f'''| <= c, then a uniform sign and a standard Gaussian give expectations of f within c / 2.

Main result

Stated in the README together with derive_le_cmp.

Statement as written in the source
Lemma rademacher_gauss_step (f f1 f2 f3 : R -> R) (c : R) :
  (forall t : R, is_derive t 1 f (f1 t)) ->
  (forall t : R, is_derive t 1 f1 (f2 t)) ->
  (forall t : R, is_derive t 1 f2 (f3 t)) -> (forall t, `|f3 t| <= c) ->
  `|(f 1 + f (-1)) / 2 - \int[N]_t f t| <= c / 2.
Used by 1 declaration in 1 file
sectionrademacher_gauss
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
definition sign_row source, line 341
Type
forall {R : realType} [n : nat], {ffun 'I_n -> bool} -> 'rV_n
Definition
Definition sign_row n (s : {ffun 'I_n -> bool}) : 'rV[R]_n :=
  \row_i (if s i then 1 else -1).

The row of the signs of s.

Used by 4 declarations in 2 files
definition ffun_cons source, line 345
Type
forall [n : nat], bool -> {ffun 'I_n -> bool} -> {ffun 'I_n.+1 -> bool}
Definition
Definition ffun_cons n (b : bool) (s : {ffun 'I_n -> bool}) :
  {ffun 'I_n.+1 -> bool} :=
  [ffun i => if unlift ord0 i is Some j then s j else b].

A function on 'I_n.+1, from its value at 0 and a function on 'I_n.

Used by 3 declarations in 1 file
lemma ffun_cons_bij source, line 349 
forall n : nat, bijective (fun p : bool * {ffun 'I_n -> bool} => ffun_cons p.1 p.2)
Statement as written in the source
Lemma ffun_cons_bij n :
  bijective (fun p : bool * {ffun 'I_n -> bool} => ffun_cons p.1 p.2).
Used by 1 declaration in 1 file
lemma sign_row_cons source, line 360 
forall {R : realType} [n : nat] (b : bool) (s : {ffun 'I_n -> bool}),
sign_row (ffun_cons b s) = rV_cons (if b then 1 else -1, sign_row s)
Statement as written in the source
Lemma sign_row_cons n b (s : {ffun 'I_n -> bool}) :
  sign_row (ffun_cons b s) = rV_cons ((if b then 1 else -1), sign_row s).
Used by 1 declaration in 1 file
lemma sum_sign_rowS source, line 368 
forall {R : realType} [n : nat] (G : 'rV_n.+1 -> R),
\sum_s G (sign_row s) = \sum_s (G (rV_cons (1, sign_row s)) + G (rV_cons (-1, sign_row s)))
Statement as written in the source
Lemma sum_sign_rowS n (G : 'rV[R]_n.+1 -> R) :
  \sum_(s : {ffun 'I_n.+1 -> bool}) G (sign_row s) =
  \sum_(s : {ffun 'I_n -> bool})
    (G (rV_cons (1, sign_row s)) + G (rV_cons (-1, sign_row s))).
Used by 1 declaration in 1 file
lemma rV_cons_line source, line 380 
forall {R : realType} [n : nat] (a t : R) (y : 'rV_n) (j : 'I_n),
rV_cons (a, t *: delta_mx 0 j + y) = t *: delta_mx 0 (lift ord0 j) + rV_cons (a, y)
Statement as written in the source
Lemma rV_cons_line n (a t : R) (y : 'rV[R]_n) (j : 'I_n) :
  rV_cons (a, t *: delta_mx 0 j + y) =
  t *: delta_mx 0 (lift ord0 j) + rV_cons (a, y).
Used by 1 declaration in 1 file
lemma rV_cons_line0 source, line 391 
forall {R : realType} [n : nat] (t : R) (y : 'rV_n),
rV_cons (t, y) = t *: delta_mx 0 ord0 + rV_cons (0, y)
Statement as written in the source
Lemma rV_cons_line0 n (t : R) (y : 'rV[R]_n) :
  rV_cons (t, y) = t *: delta_mx 0 ord0 + rV_cons (0, y).
Used by 1 declaration in 1 file
lemma Rintegral_gauss_cons source, line 401 
forall {R : realType} [n : nat] [F : 'rV_n.+1 -> R] [C : R],
measurable_fun [set: 'rV_n.+1] F ->
(forall x : 'rV_n.+1, `|F x| <= C) ->
\int[gauss n.+1]_x F x = \int[gauss n]_y \int[normal_prob 0 1]_t F (rV_cons (t, y))

Fubini along the first coordinate, for a bounded measurable F.

Statement as written in the source
Lemma Rintegral_gauss_cons n (F : 'rV[R]_n.+1 -> R) (C : R) :
  measurable_fun setT F -> (forall x, `|F x| <= C) ->
  \int[gauss n.+1]_x F x = \int[gauss n]_y \int[N]_t F (rV_cons (t, y)).
Used by 1 declaration in 1 file
theorem rademacher_gauss_lindeberg main result source, line 431 
forall {R : realType} [n : nat] [F : 'rV_n -> R] [C : R] [c : 'I_n -> R],
measurable_fun [set: 'rV_n] F ->
(forall x : 'rV_n, `|F x| <= C) ->
(forall (j : 'I_n) (x : 'rV_n),
 exists F1 F2 F3 : R -> R,
   [/\ forall t : R,
       is_derive t 1
         (fun s : R =>
          F (s *: delta_mx 0 j + x))
         (F1 t),
       forall t : R, is_derive t 1 F1 (F2 t), forall t : R, is_derive t 1 F2 (F3 t)
     & forall t : R, `|F3 t| <= c j]) ->
`|2 ^- n * \sum_s F (sign_row s) - \int[gauss n]_x F x| <= 2^-1 * \sum_j c j

Lindeberg's replacement of uniform signs by Gaussians: if F is bounded and measurable and its third derivative along the coordinate j is at most c_j in absolute value, then the averages of F over the rows of signs and against gauss n differ by at most (1/2) \sum_j c_j.

Main result, as the README states it

Lindeberg's replacement of uniform signs by Gaussians (Chatterjee 2006, Theorem 1.1, for signs and standard Gaussians): if F : 'rV[R]_n -> R is measurable and bounded, and for every x and j the map t |-> F (t e_j + x) has three derivatives with the third at most c_j in absolute value, then the average of F over the 2^n rows of signs and its integral against gauss n differ by at most (1/2) sum_j c_j. By induction on n, with Fubini along rV_cons for bounded measurable functions (Rintegral_gauss_cons) and the decomposition of the rows of signs by their first coordinate (sum_sign_rowS).

Statement as written in the source
Theorem rademacher_gauss_lindeberg n (F : 'rV[R]_n -> R) (C : R)
    (c : 'I_n -> R) :
  measurable_fun setT F -> (forall x, `|F x| <= C) ->
  (forall (j : 'I_n) (x : 'rV[R]_n), exists F1 F2 F3 : R -> R,
    [/\ forall t : R, is_derive t 1 (fun s => F (s *: delta_mx 0 j + x)) (F1 t),
        forall t : R, is_derive t 1 F1 (F2 t),
        forall t : R, is_derive t 1 F2 (F3 t) &
        forall t, `|F3 t| <= c j]) ->
  `|(2 ^+ n)^-1 * \sum_(s : {ffun 'I_n -> bool}) F (sign_row s) -
    \int[gauss n]_x F x| <= 2^-1 * \sum_j c j.
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.