On this page

GaussianAnalysiscomparisongauss_concentration

Gaussian concentration for Lipschitz functions

GaussianAnalysis.comparison.gauss_concentrationlibrary/comparison/gauss_concentration.v1,214 lines25 lemmas and theorems, 1 definitionsource

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

Required by 4 files of the paper proofs

Let x have law gauss n and let F : 'rV[R]_n -> R be L-Lipschitz for the Euclidean norm: |F x - F y| <= L |x - y|. Then E[expR (t (F x - E[F]))] <= expR (t^2 L^2 / 2) for every real t (gauss_concentration), with the sharp constant of Tsirelson, Ibragimov and Sudakov. For u >= 0, P(F x >= E[F] + u) and P(F x <= E[F] - u) are at most expR (- u^2 / (2 L^2)) (gauss_concentration_upper_tail, gauss_concentration_lower_tail), and P(|F x - E[F]| >= u) is at most twice that (gauss_concentration_abs_tail). The variance of F x is at most L^2: this is the Gaussian Poincare inequality for Lipschitz functions (gauss_poincare_lipschitz), from the bound on E[expR (t (F x - E[F]))] at t and - t, with cosh y >= 1 + y^2 / 2 (expR_cosh_ge), as t -> 0.

The proof follows Herbst. Let F be bounded, of class C^1, with gradient of Euclidean norm at most L, and let t >= 0. Let y be an independent copy of x and phi th = E[F x expR (t F (cos th x + sin th y))]. After the rotation of (x, y) by th, Gaussian integration by parts in y (gauss2_ibp_snd) shows that the derivative of phi is at least - sin th t L^2 E[expR (t F)]. Comparing phi 0 and phi (pi / 2) gives the covariance inequality E[F expR (t F)] <= (E[F] + t L^2) E[expR (t F)] (gauss_herbst_ineq), and integrating the resulting differential inequality for t |-> E[expR (t F)] gives the bound for such F (gauss_concentration_smooth). A general Lipschitz F is the pointwise limit of Gaussian smoothings (gauss_smoothing.v) of F clipped to [-(k + 1), k + 1] (clip), and Fatou's lemma concludes.

The file also proves facts on the law gauss n \x gauss n of two independent standard Gaussian vectors: its marginals (integral_gauss2_fst, integral_gauss2_snd), the independence of its components (integral_gauss2_prod) and integration by parts in the second component (gauss2_ibp_snd).

clip k x the point of [-k, k] closest to x

Main results

Results	Statement	Used by `theories/`
gauss_herbst_ineq	For `x` of law `gauss n`, `F` bounded of class C^1 with gradient norm at most `L`, and `t >= 0`: `E[F expR (t F)] <= (E[F] + t L^2) E[expR (t F)]`.
gauss_concentration	Gaussian concentration (Tsirelson, Ibragimov, Sudakov): if `F` is `L`-Lipschitz for the Euclidean norm, then `E[expR (t (F x - E F))] <= expR (t^2 L^2 / 2)` for every real `t`.	`Gaussian/Lipschitz/Concentration`
gauss_concentration_upper_tailgauss_concentration_lower_tailgauss_concentration_abs_tail	For such `F` and `u >= 0`, `P(F x >= E F + u)` and `P(F x <= E F - u)` are at most `expR (- u^2 / (2 L^2))`, and `P(\|F x - E F\| >= u)` is at most twice that.
gauss_poincare_lipschitz	Gaussian Poincaré inequality for Lipschitz functions: if `F` is `L`-Lipschitz for the Euclidean norm and `x` has law `gauss n`, then `E[(F x - E F)^2] <= L^2`.	`Gaussian/Lipschitz/Variance`
expR_cosh_geexpR_sinh_ge	`2 + x^2 <= expR x + expR (- x)` for every real `x`, and `2 y <= expR y - expR (- y)` for `y >= 0`.
integral_gauss2_fstintegral_gauss2_prodgauss2_ibp_snd	For `(x, y)` of law `gauss n \x gauss n`: the marginals are `gauss n`, the components are independent, and `E[y_j H(x, y)] = E[d_(y_j) H(x, y)]`.

Declarations26 exported, 50 local

sectionprob_bounded

Context d (T : measurableType d) (R : realType) (mu : probability T R).

lemma integrable_prob_bounded source, line 69

forall [d : measure_display] [T : measurableType d] [R : realType] 
  (mu : probability T R) [f : T -> R] [C : R],
measurable_fun [set: T] f ->
(forall x : T, `|f x| <= C) -> mu.-integrable [set: T] (EFin \o f)

Statement as written in the source

Lemma integrable_prob_bounded (f : T -> R) (C : R) :
  measurable_fun [set: T] f -> (forall x, `|f x| <= C) ->
  mu.-integrable [set: T] (EFin \o f).

Used by 11 declarations in 2 files

this file: integral_gauss2_prod, gauss2_ibp_snd, herbst_phi_derive, herbst_df_lower, gauss_herbst_ineq, herbst_mgf_derive, gauss_concentration_smooth_ge0, gauss_concentration_smooth, gauss_concentration
GaussianAnalysis.comparison.sudakov: gauss_max_lower, dual_sudakov

sectiongauss2

Context {R : realType} {n : nat}.
Local Notation P := (gauss n \x gauss n)%E.

lemma integrable_gauss2_fst source, line 85

forall {R : realType} {n : nat} [g : 'rV_n -> R],
(gauss n).-integrable [set: 'rV_n] (EFin \o g) ->
(gauss n \x gauss n)%E.-integrable [set: 'rV_n * 'rV_n]
  (fun p : ('rV_n * 'rV_n) =>
   (g p.1)%:E)

Statement as written in the source

Lemma integrable_gauss2_fst (g : 'rV[R]_n -> R) :
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o g) ->
  P.-integrable [set: 'rV[R]_n * 'rV[R]_n] (fun p => (g p.1)%:E).

Used by 3 declarations in 1 file

this file: integral_gauss2_fst, integrable_herbst_D, herbst_df_lower

lemma integrable_gauss2_snd source, line 103

forall {R : realType} {n : nat} [g : 'rV_n -> R],
(gauss n).-integrable [set: 'rV_n] (EFin \o g) ->
(gauss n \x gauss n)%E.-integrable [set: 'rV_n * 'rV_n]
  (fun p : ('rV_n * 'rV_n) =>
   (g p.2)%:E)

Statement as written in the source

Lemma integrable_gauss2_snd (g : 'rV[R]_n -> R) :
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o g) ->
  P.-integrable [set: 'rV[R]_n * 'rV[R]_n] (fun p => (g p.2)%:E).

Used by 4 declarations in 1 file

this file: integral_gauss2_snd, gauss2_ibp_snd, integrable_herbst_D, herbst_df_lower

lemma integral_gauss2_fst main result source, line 120

forall {R : realType} {n : nat} [g : 'rV_n -> R],
(gauss n).-integrable [set: 'rV_n] (EFin \o g) ->
(\int[gauss n \x gauss n]_p (g p.1)%:E)%E = (\int[gauss n]_x (g x)%:E)%E

Main result, as the README states it

For (x, y) of law gauss n \x gauss n: the marginals are gauss n, the components are independent, and E[y_j H(x, y)] = E[d_(y_j) H(x, y)].

Statement as written in the source

Lemma integral_gauss2_fst (g : 'rV[R]_n -> R) :
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o g) ->
  (\int[P]_p (g p.1)%:E = \int[gauss n]_x (g x)%:E)%E.

Used by 2 declarations in 1 file

this file: herbst_df_lower, gauss_herbst_ineq

lemma integral_gauss2_snd source, line 129

forall {R : realType} {n : nat} [g : 'rV_n -> R],
(gauss n).-integrable [set: 'rV_n] (EFin \o g) ->
(\int[gauss n \x gauss n]_p (g p.2)%:E)%E = (\int[gauss n]_x (g x)%:E)%E

Statement as written in the source

Lemma integral_gauss2_snd (g : 'rV[R]_n -> R) :
  (gauss n).-integrable [set: 'rV[R]_n] (EFin \o g) ->
  (\int[P]_p (g p.2)%:E = \int[gauss n]_x (g x)%:E)%E.

lemma integral_gauss2_prod main result source, line 139

forall {R : realType} {n : nat} [f g : 'rV_n -> R] [C : R],
measurable_fun [set: 'rV_n] f ->
measurable_fun [set: 'rV_n] g ->
(forall x : 'rV_n, `|f x| <= C) ->
(forall x : 'rV_n, `|g x| <= C) ->
(\int[gauss n \x gauss n]_p (f p.1 * g p.2)%:E)%E =
(\int[gauss n]_x (f x)%:E * \int[gauss n]_y (g y)%:E)%E

The two components of a vector of law gauss n \x gauss n are independent.

Main result

Stated in the README together with integral_gauss2_fst.

Statement as written in the source

Lemma integral_gauss2_prod (f g : 'rV[R]_n -> R) (C : R) :
    measurable_fun [set: 'rV[R]_n] f -> measurable_fun [set: 'rV[R]_n] g ->
    (forall x, `|f x| <= C) -> (forall x, `|g x| <= C) ->
  (\int[P]_p (f p.1 * g p.2)%:E =
   \int[gauss n]_x (f x)%:E * \int[gauss n]_y (g y)%:E)%E.

Used by 1 declaration in 1 file

this file: gauss_herbst_ineq

lemma gauss2_ibp_snd main result source, line 164

forall {R : realType} {n : nat} [j : 'I_n] [H dH : 'rV_n * 'rV_n -> R] [C : R],
measurable_fun [set: 'rV_n * 'rV_n] H ->
measurable_fun [set: 'rV_n * 'rV_n] dH ->
(forall (x : 'rV_n) (v : 'rV[R]_n),
 is_derive v (delta_mx 0 j)
   (fun v0 : 'rV[R]_n => H (x, v0))
   (dH (x, v))) ->
(forall x : 'rV_n,
 continuous
   (fun
      v : 'rV[R]_n =>
    H (x, v))) ->
(forall x : 'rV_n,
 continuous
   (fun
      v : 'rV[R]_n =>
    dH (x, v))) ->
(forall p : 'rV_n * 'rV_n, `|H p| <= C) ->
(forall p : 'rV_n * 'rV_n, `|dH p| <= C) ->
(\int[gauss n \x gauss n]_p (p.2 0 j * H p)%:E)%E =
(\int[gauss n \x gauss n]_p (dH p)%:E)%E

Gaussian integration by parts in the second component.

Main result

Stated in the README together with integral_gauss2_fst.

Statement as written in the source

Lemma gauss2_ibp_snd (j : 'I_n) (H dH : 'rV[R]_n * 'rV[R]_n -> R) (C : R) :
    measurable_fun [set: 'rV[R]_n * 'rV[R]_n] H ->
    measurable_fun [set: 'rV[R]_n * 'rV[R]_n] dH ->
    (forall x v, is_derive v (delta_mx 0 j) (fun v => H (x, v)) (dH (x, v))) ->
    (forall x, continuous (fun v => H (x, v))) ->
    (forall x, continuous (fun v => dH (x, v))) ->
    (forall p, `|H p| <= C) -> (forall p, `|dH p| <= C) ->
  (\int[P]_p (p.2 0 j * H p)%:E = \int[P]_p (dH p)%:E)%E.

Used by 1 declaration in 1 file

this file: herbst_ibp

F is bounded by K, of class C^1 with partial derivatives DF j, and its gradient has Euclidean norm at most L.

sectiongauss_herbst

Context {R : realType} {n : nat}.
Variables (F : 'rV[R]_n -> R) (DF : 'I_n -> 'rV[R]_n -> R) (K L : R).
Hypothesis dF : forall j x, is_derive x (delta_mx 0 j) F (DF j x).
Hypothesis cDF : forall j, continuous (DF j).
Hypothesis FK : forall x, `|F x| <= K.
Hypothesis gradL : forall x, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2.
Local Notation P := (gauss n \x gauss n)%E.

local lemma herbst_Fdiff not exported source, line 211

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
forall x : 'rV[R]_n,
differentiable (F : 'rV_n -> R^o) x

Statement as written in the source

Local Lemma herbst_Fdiff x : differentiable (F : 'rV[R]_n -> R^o) x.

Used by 3 declarations in 1 file

this file: herbst_cF, herbst_is_derive_Fz, herbst_is_derive_Fr

local lemma herbst_cF not exported source, line 214

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) -> continuous F

Statement as written in the source

Local Lemma herbst_cF : continuous F.

Used by 2 declarations in 1 file

this file: herbst_mF, herbst_ibp

local lemma herbst_mF not exported source, line 217

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) -> measurable_fun [set: 'rV_n] F

Statement as written in the source

Local Lemma herbst_mF : measurable_fun [set: 'rV[R]_n] F.

Used by 8 declarations in 1 file

this file: herbst_mf, herbst_mdf, herbst_mk, herbst_ibp, herbst_df_lower, gauss_herbst_ineq, herbst_mgf_derive, gauss_concentration_smooth_ge0

local lemma herbst_mDF not exported source, line 220

forall {R : realType} {n : nat} [DF : 'I_n -> 'rV_n -> R],
(forall j : 'I_n, continuous (DF j)) -> forall j : 'I_n, measurable_fun [set: 'rV_n] (DF j)

Statement as written in the source

Local Lemma herbst_mDF j : measurable_fun [set: 'rV[R]_n] (DF j).

Used by 4 declarations in 1 file

this file: herbst_mdf, herbst_mk, herbst_ibp, herbst_df_lower

local lemma herbst_K0 not exported source, line 223

forall {R : realType} {n : nat} [F : 'rV_n -> R] [K : R],
(forall x : 'rV_n, `|F x| <= K) -> 0 <= K

Statement as written in the source

Local Lemma herbst_K0 : 0 <= K.

Used by 7 declarations in 1 file

this file: herbst_df_bound, herbst_D_ge0, herbst_ibp, herbst_df_lower, gauss_herbst_ineq, herbst_mgf_derive, gauss_concentration_smooth_ge0

local lemma herbst_DFL not exported source, line 226

forall {R : realType} {n : nat} [DF : 'I_n -> 'rV_n -> R] [L : R],
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
forall (j : 'I_n) (x : 'rV_n), `|DF j x| <= `|L|

Statement as written in the source

Local Lemma herbst_DFL j x : `|DF j x| <= `|L|.

Used by 4 declarations in 1 file

this file: herbst_df_bound, herbst_k_bound, herbst_ibp, herbst_df_lower

local lemma herbst_DFdot not exported source, line 233

forall {R : realType} {n : nat} [DF : 'I_n -> 'rV_n -> R] [L : R],
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
forall x y : 'rV_n, \sum_j DF j x * DF j y <= L ^+ 2

Statement as written in the source

Local Lemma herbst_DFdot x y : \sum_j DF j x * DF j y <= L ^+ 2.

Used by 1 declaration in 1 file

this file: herbst_df_lower

local definition herbst_z not exported source, line 246

Type

forall {R : realType} {n : nat}, R -> 'rV_n * 'rV_n -> 'rV_n

Definition

Local Definition herbst_z (th : R) (p : 'rV[R]_n * 'rV[R]_n) : 'rV[R]_n :=
  cos th *: p.1 + sin th *: p.2.

The interpolation between x and y along a quarter circle, and its derivative.

Used by 9 declarations in 1 file

this file: herbst_is_derive_z, herbst_is_derive_Fz, herbst_mz, herbst_f, herbst_df, herbst_is_derive_f, herbst_df_bound, herbst_df_lower, gauss_herbst_ineq

local definition herbst_dz not exported source, line 248

Type

forall {R : realType} {n : nat}, R -> 'rV_n * 'rV_n -> 'rV_n

Definition

Local Definition herbst_dz (th : R) (p : 'rV[R]_n * 'rV[R]_n) : 'rV[R]_n :=
  - sin th *: p.1 + cos th *: p.2.

Used by 7 declarations in 1 file

this file: herbst_is_derive_z, herbst_is_derive_Fz, herbst_mdz, herbst_dz_bound, herbst_df, herbst_df_bound, herbst_df_lower

local lemma herbst_is_derive_z not exported source, line 251

forall {R : realType} {n : nat} (th : R) (p : 'rV_n * 'rV_n),
is_derive th 1 (gauss_concentration.herbst_z^~ p) (gauss_concentration.herbst_dz th p)

Statement as written in the source

Local Lemma herbst_is_derive_z (th : R) p : is_derive th 1 (herbst_z ^~ p) (herbst_dz th p).

Used by 1 declaration in 1 file

this file: herbst_is_derive_Fz

local lemma herbst_is_derive_Fz not exported source, line 257

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
forall (th : R) (p : 'rV_n * 'rV_n),
is_derive th 1
  (fun th0 : R =>
   F (gauss_concentration.herbst_z th0 p))
  (\sum_j gauss_concentration.herbst_dz th p 0 j * DF j (gauss_concentration.herbst_z th p))

Statement as written in the source

Local Lemma herbst_is_derive_Fz (th : R) p :
  is_derive th 1 (fun th => F (herbst_z th p))
    (\sum_j herbst_dz th p 0 j * DF j (herbst_z th p)).

Used by 1 declaration in 1 file

this file: herbst_is_derive_f

local lemma herbst_mz not exported source, line 266

forall {R : realType} {n : nat} (th : R),
measurable_fun [set: 'rV_n * 'rV_n] (gauss_concentration.herbst_z th)

Statement as written in the source

Local Lemma herbst_mz (th : R) :
  measurable_fun [set: 'rV[R]_n * 'rV[R]_n] (herbst_z th).

Used by 2 declarations in 1 file

this file: herbst_mf, herbst_mdf

local lemma herbst_mdz not exported source, line 274

forall {R : realType} {n : nat} (th : R),
measurable_fun [set: 'rV_n * 'rV_n] (gauss_concentration.herbst_dz th)

Statement as written in the source

Local Lemma herbst_mdz (th : R) :
  measurable_fun [set: 'rV[R]_n * 'rV[R]_n] (herbst_dz th).

Used by 1 declaration in 1 file

this file: herbst_mdf

local lemma herbst_dz_bound not exported source, line 282

forall {R : realType} {n : nat} (th : R) (p : 'rV_n * 'rV_n) (j : 'I_n),
`|gauss_concentration.herbst_dz th p 0 j| <= `|p.1| + `|p.2|

Statement as written in the source

Local Lemma herbst_dz_bound (th : R) p j : `|herbst_dz th p 0 j| <= `|p.1| + `|p.2|.

Used by 1 declaration in 1 file

this file: herbst_df_bound

local lemma continuous_affine_rV not exported source, line 293

forall {R : realType} {n : nat} [c s : R] [x : 'rV_n],
continuous (fun v : 'rV_n => c *: x - s *: v)

Statement as written in the source

Local Lemma continuous_affine_rV (c s : R) (x : 'rV[R]_n) :
  continuous (fun v : 'rV[R]_n => c *: x - s *: v).

Used by 1 declaration in 1 file

this file: herbst_ibp

local lemma measurable_affine2 not exported source, line 301

forall {R : realType} {n : nat} (c s : R),
measurable_fun [set: 'rV_n * 'rV_n]
  (fun
     p : ('rV_n * 'rV_n) =>
   c *: p.1 - s *: p.2)

Statement as written in the source

Local Lemma measurable_affine2 (c s : R) :
  measurable_fun [set: 'rV[R]_n * 'rV[R]_n] (fun p => c *: p.1 - s *: p.2).

Used by 2 declarations in 1 file

this file: herbst_ibp, herbst_df_lower

local lemma herbst_is_derive_Fr not exported source, line 310

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
forall (c s : R) (x v : 'rV_n) (j : 'I_n),
is_derive v (delta_mx 0 j)
  (fun v0 : 'rV[R]_n =>
   F (c *: x - s *: v0))
  (- s * DF j (c *: x - s *: v))

Statement as written in the source

Local Lemma herbst_is_derive_Fr (c s : R) (x v : 'rV[R]_n) j :
  is_derive v (delta_mx 0 j) (fun v => F (c *: x - s *: v))
    (- s * DF j (c *: x - s *: v)).

Used by 1 declaration in 1 file

this file: herbst_ibp

sectionherbst_t

Variable t : R.
Hypothesis t0 : 0 <= t.

local definition herbst_f not exported source, line 328

Type

forall {R : realType} {n : nat}, ('rV_n -> R) -> R -> R -> 'rV_n * 'rV_n -> R

Definition

Local Definition herbst_f (th : R) (p : 'rV[R]_n * 'rV[R]_n) : R :=
  F p.1 * expR (t * F (herbst_z th p)).

Used by 5 declarations in 1 file

this file: herbst_is_derive_f, herbst_mf, herbst_f_bound, herbst_phi_derive, gauss_herbst_ineq

local definition herbst_df not exported source, line 331

Type

forall {R : realType} {n : nat},
('rV_n -> R) -> ('I_n -> 'rV_n -> R) -> R -> R -> 'rV_n * 'rV_n -> R

Definition

Local Definition herbst_df (th : R) (p : 'rV[R]_n * 'rV[R]_n) : R :=
  F p.1 * (expR (t * F (herbst_z th p)) *
    (t * \sum_j herbst_dz th p 0 j * DF j (herbst_z th p))).

Used by 7 declarations in 1 file

this file: herbst_is_derive_f, herbst_mdf, herbst_df_bound, integrable_herbst_df, herbst_phi_derive, herbst_df_lower, gauss_herbst_ineq

local lemma herbst_is_derive_f not exported source, line 335

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
forall (t th : R) (p : 'rV_n * 'rV_n),
is_derive th 1 ((gauss_concentration.herbst_f F t)^~ p)
  (gauss_concentration.herbst_df F DF t th p)

Statement as written in the source

Local Lemma herbst_is_derive_f (th : R) p : is_derive th 1 (herbst_f ^~ p) (herbst_df th p).

Used by 1 declaration in 1 file

this file: herbst_phi_derive

local lemma herbst_mf not exported source, line 343

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
forall t th : R, measurable_fun [set: 'rV_n * 'rV_n] (gauss_concentration.herbst_f F t th)

Statement as written in the source

Local Lemma herbst_mf (th : R) : measurable_fun [set: 'rV[R]_n * 'rV[R]_n] (herbst_f th).

Used by 1 declaration in 1 file

this file: herbst_phi_derive

local lemma herbst_mdf not exported source, line 350

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
forall t th : R,
measurable_fun [set: 'rV_n * 'rV_n] (gauss_concentration.herbst_df F DF t th)

Statement as written in the source

Local Lemma herbst_mdf (th : R) : measurable_fun [set: 'rV[R]_n * 'rV[R]_n] (herbst_df th).

Used by 1 declaration in 1 file

this file: integrable_herbst_df

local lemma herbst_expR_le not exported source, line 362

forall {R : realType} {n : nat} [F : 'rV_n -> R] [K : R],
(forall x : 'rV_n, `|F x| <= K) ->
forall [t : R], 0 <= t -> forall x : 'rV_n, expR (t * F x) <= expR (t * K)

Statement as written in the source

Local Lemma herbst_expR_le (x : 'rV[R]_n) : expR (t * F x) <= expR (t * K).

Used by 5 declarations in 1 file

this file: herbst_f_bound, herbst_df_bound, herbst_k_bound, herbst_df_lower, gauss_herbst_ineq

local lemma herbst_f_bound not exported source, line 365

forall {R : realType} {n : nat} [F : 'rV_n -> R] [K : R],
(forall x : 'rV_n, `|F x| <= K) ->
forall [t : R],
0 <= t ->
forall (th : R) (p : 'rV_n * 'rV_n),
`|gauss_concentration.herbst_f F t th p| <= K * expR (t * K)

Statement as written in the source

Local Lemma herbst_f_bound (th : R) p : `|herbst_f th p| <= K * expR (t * K).

Used by 1 declaration in 1 file

this file: herbst_phi_derive

local lemma herbst_df_bound not exported source, line 371

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] [K L : R],
(forall x : 'rV_n, `|F x| <= K) ->
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
forall [t : R],
0 <= t ->
forall (th : R) (p : 'rV_n * 'rV_n),
`|gauss_concentration.herbst_df F DF t th p| <=
K * expR (t * K) * (t * (n%:R * `|L|)) * (`|p.1| + `|p.2|)

Statement as written in the source

Local Lemma herbst_df_bound (th : R) p :
  `|herbst_df th p| <= K * expR (t * K) * (t * (n%:R * `|L|)) * (`|p.1| + `|p.2|).

Used by 2 declarations in 1 file

this file: integrable_herbst_df, herbst_phi_derive

local definition herbst_D not exported source, line 394

Type

forall {R : realType} {n : nat}, R -> R -> R -> 'rV_n * 'rV_n -> R

Definition

Local Definition herbst_D (p : 'rV[R]_n * 'rV[R]_n) : R :=
  K * expR (t * K) * (t * (n%:R * `|L|)) * (`|p.1| + `|p.2|).

Used by 2 declarations in 1 file

this file: herbst_D_ge0, integrable_herbst_D

local lemma herbst_D_ge0 not exported source, line 397

forall {R : realType} {n : nat} [F : 'rV_n -> R] [K : R] (L : R),
(forall x : 'rV_n, `|F x| <= K) ->
forall [t : R],
0 <= t -> forall p : 'rV_n * 'rV_n, 0 <= gauss_concentration.herbst_D K L t p

Statement as written in the source

Local Lemma herbst_D_ge0 p : 0 <= herbst_D p.

Used by 2 declarations in 1 file

this file: integrable_herbst_df, herbst_phi_derive

local lemma integrable_herbst_D not exported source, line 400

forall {R : realType} {n : nat} (K L t : R),
(gauss n \x gauss n)%E.-integrable [set: 'rV_n * 'rV_n]
  (EFin \o gauss_concentration.herbst_D K L t)

Statement as written in the source

Local Lemma integrable_herbst_D :
  P.-integrable [set: 'rV[R]_n * 'rV[R]_n] (EFin \o herbst_D).

Used by 2 declarations in 1 file

this file: integrable_herbst_df, herbst_phi_derive

local lemma integrable_herbst_df not exported source, line 412

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] [K L : R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
(forall x : 'rV_n, `|F x| <= K) ->
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
forall [t : R],
0 <= t ->
forall th : R,
(gauss n \x gauss n)%E.-integrable [set: 'rV_n * 'rV_n]
  (EFin \o gauss_concentration.herbst_df F DF t th)

Statement as written in the source

Local Lemma integrable_herbst_df (th : R) :
  P.-integrable [set: 'rV[R]_n * 'rV[R]_n] (EFin \o herbst_df th).

Used by 1 declaration in 1 file

this file: herbst_df_lower

local lemma herbst_phi_derive not exported source, line 421

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] [K L : R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
(forall x : 'rV_n, `|F x| <= K) ->
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
forall [t : R],
0 <= t ->
forall [th : R],
th \in `]-1, 2[ ->
is_derive th 1
  (fun th0 : R =>
   \int[(gauss n \x gauss n)%E]_p gauss_concentration.herbst_f F t th0 p)
  (\int[(gauss n \x gauss n)%E]_p gauss_concentration.herbst_df F DF t th p)

Statement as written in the source

Local Lemma herbst_phi_derive (th : R) : th \in `]-1, 2[ ->
  is_derive th 1 (fun th => \int[P]_p herbst_f th p) (\int[P]_p herbst_df th p).

Used by 1 declaration in 1 file

this file: gauss_herbst_ineq

local definition herbst_k not exported source, line 430

Type

forall {R : realType} {n : nat},
('rV_n -> R) -> ('I_n -> 'rV_n -> R) -> R -> 'I_n -> 'rV_n -> R

Definition

Local Definition herbst_k (j : 'I_n) (x : 'rV[R]_n) : R := t * expR (t * F x) * DF j x.

Used by 4 declarations in 1 file

this file: herbst_k_bound, herbst_mk, herbst_ibp, herbst_df_lower

local lemma herbst_k_bound not exported source, line 432

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] [K L : R],
(forall x : 'rV_n, `|F x| <= K) ->
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
forall [t : R],
0 <= t ->
forall (j : 'I_n) (x : 'rV_n),
`|gauss_concentration.herbst_k F DF t j x| <= t * expR (t * K) * `|L|

Statement as written in the source

Local Lemma herbst_k_bound j x : `|herbst_k j x| <= t * expR (t * K) * `|L|.

Used by 2 declarations in 1 file

this file: herbst_ibp, herbst_df_lower

local lemma herbst_mk not exported source, line 439

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
forall (t : R) (j : 'I_n),
measurable_fun [set: 'rV_n] (gauss_concentration.herbst_k F DF t j)

Statement as written in the source

Local Lemma herbst_mk j : measurable_fun [set: 'rV[R]_n] (herbst_k j).

Used by 2 declarations in 1 file

this file: herbst_ibp, herbst_df_lower

local lemma herbst_ibp not exported source, line 448

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] [K L : R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
(forall x : 'rV_n, `|F x| <= K) ->
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
forall [t : R],
0 <= t ->
forall (c s : R) (j : 'I_n),
\int[(gauss n \x gauss n)%E]_p
   (p.2 0 j * (gauss_concentration.herbst_k F DF t j p.1 * F (c *: p.1 - s *: p.2))) =
\int[(gauss n \x gauss n)%E]_p
   (gauss_concentration.herbst_k F DF t j p.1 * (- s * DF j (c *: p.1 - s *: p.2)))

Gaussian integration by parts in the second component, for the test functions of the rotated covariance identity.

Statement as written in the source

Local Lemma herbst_ibp (c s : R) j :
  \int[P]_p (p.2 0 j * (herbst_k j p.1 * F (c *: p.1 - s *: p.2))) =
  \int[P]_p (herbst_k j p.1 * (- s * DF j (c *: p.1 - s *: p.2))).

Used by 1 declaration in 1 file

this file: herbst_df_lower

local lemma herbst_df_lower not exported source, line 476

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] [K L : R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
(forall x : 'rV_n, `|F x| <= K) ->
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
forall [t : R],
0 <= t ->
forall [th : R],
0 <= sin th ->
- (sin th * t * L ^+ 2) * \int[gauss n]_x expR (t * F x) <=
\int[(gauss n \x gauss n)%E]_p gauss_concentration.herbst_df F DF t th p

Statement as written in the source

Local Lemma herbst_df_lower (th : R) : 0 <= sin th ->
  - (sin th * t * L ^+ 2) * \int[gauss n]_x expR (t * F x) <=
  \int[P]_p herbst_df th p.

Used by 1 declaration in 1 file

this file: gauss_herbst_ineq

lemma gauss_herbst_ineq main result source, line 578

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] [K L : R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
(forall x : 'rV_n, `|F x| <= K) ->
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
forall [t : R],
0 <= t ->
\int[gauss n]_x (F x * expR (t * F x)) <=
(\int[gauss n]_x F x + t * L ^+ 2) * \int[gauss n]_x expR (t * F x)

The covariance inequality behind Herbst's argument: E[F expR (t F)] <= (E[F] + t L^2) E[expR (t F)].

Main result, as the README states it

For x of law gauss n, F bounded of class C^1 with gradient norm at most L, and t >= 0: E[F expR (t F)] <= (E[F] + t L^2) E[expR (t F)].

Statement as written in the source

Lemma gauss_herbst_ineq :
  \int[gauss n]_x (F x * expR (t * F x)) <=
  (\int[gauss n]_x F x + t * L ^+ 2) * \int[gauss n]_x expR (t * F x).

Used by 1 declaration in 1 file

this file: gauss_concentration_smooth_ge0

local lemma herbst_mgf_derive not exported source, line 639

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] [K : R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
(forall x : 'rV_n, `|F x| <= K) ->
forall s : R,
is_derive s 1
  (fun s0 : R =>
   \int[gauss n]_x expR (s0 * F x))
  (\int[gauss n]_x (F x * expR (s * F x)))

Statement as written in the source

Local Lemma herbst_mgf_derive (s : R) :
  is_derive s 1 (fun s => \int[gauss n]_x expR (s * F x))
    (\int[gauss n]_x (F x * expR (s * F x))).

Used by 1 declaration in 1 file

this file: gauss_concentration_smooth_ge0

lemma gauss_concentration_smooth_ge0 source, line 670

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] [K L : R],
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
(forall x : 'rV_n, `|F x| <= K) ->
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
forall [t : R],
0 <= t ->
\int[gauss n]_x expR (t * (F x - \int[gauss n]_y F y)) <= expR (t ^+ 2 * L ^+ 2 / 2)

Statement as written in the source

Lemma gauss_concentration_smooth_ge0 (t : R) : 0 <= t ->
  \int[gauss n]_x expR (t * (F x - \int[gauss n]_y F y)) <=
  expR (t ^+ 2 * L ^+ 2 / 2).

Used by 1 declaration in 1 file

this file: gauss_concentration_smooth

sectiongauss_concentration_smooth

Context {R : realType} {n : nat}.

theorem gauss_concentration_smooth source, line 733

forall {R : realType} {n : nat} [F : 'rV_n -> R] [DF : 'I_n -> 'rV_n -> R] 
  [K L : R] (t : R),
(forall (j : 'I_n)
   (x : 'rV[R]_n),
 is_derive x (delta_mx 0 j) F (DF j x)) ->
(forall j : 'I_n, continuous (DF j)) ->
(forall x : 'rV_n, `|F x| <= K) ->
(forall x : 'rV_n, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
\int[gauss n]_x expR (t * (F x - \int[gauss n]_y F y)) <= expR (t ^+ 2 * L ^+ 2 / 2)

Gaussian concentration for a bounded function of class C^1 whose gradient has Euclidean norm at most L, with the sharp constant.

Statement as written in the source

Theorem gauss_concentration_smooth (F : 'rV[R]_n -> R) (DF : 'I_n -> 'rV[R]_n -> R)
    (K L t : R) :
    (forall j x, is_derive x (delta_mx 0 j) F (DF j x)) ->
    (forall j, continuous (DF j)) -> (forall x, `|F x| <= K) ->
    (forall x, mxdot (\row_j DF j x) (\row_j DF j x) <= L ^+ 2) ->
  \int[gauss n]_x expR (t * (F x - \int[gauss n]_y F y)) <=
  expR (t ^+ 2 * L ^+ 2 / 2).

Used by 1 declaration in 1 file

this file: lip_approx_mgf

sectionclip

Context {R : realType}.

definition clip source, line 770

Type

forall {R : realType}, R -> R -> R

Definition

Definition clip (k x : R) : R := Num.max (- k) (Num.min k x).

The clipping of x to [-k, k].

Used by 21 declarations in 3 files

GaussianAnalysis.random_matrix.goe: clip_pow_lipschitz, clip_pow_err, goe_clip
GaussianAnalysis.random_matrix.wigner: goe_stat_poly_clip, continuous_clip, semicircle_clip, clip_comp_lipschitz, polyfun_goe_stat_clip, goe_stat_clip_mean_cvg, wigner, clip3_bound, semicircle_near
this file: clip_bound, clip_id, clip_abs, clip_lipschitz, lip_approx, clipL, clipK, lip_approx_mgf, lip_approx_dom

lemma clip_bound source, line 772

forall {R : realType} [k : R] (x : R), 0 <= k -> `|clip k x| <= k

Statement as written in the source

Lemma clip_bound (k x : R) : 0 <= k -> `|clip k x| <= k.

Used by 9 declarations in 3 files

GaussianAnalysis.random_matrix.goe: clip_pow_lipschitz, clip_pow_err, goe_clip_bound
GaussianAnalysis.random_matrix.wigner: clip_comp_lipschitz, polyfun_goe_stat_clip, goe_stat_clip_mean_cvg, clip3_bound
this file: clip_abs, clipK

lemma clip_id source, line 779

forall {R : realType} [k x : R], `|x| <= k -> clip k x = x

Statement as written in the source

Lemma clip_id (k x : R) : `|x| <= k -> clip k x = x.

Used by 5 declarations in 3 files

GaussianAnalysis.random_matrix.goe: clip_pow_err
GaussianAnalysis.random_matrix.wigner: semicircle_clip, wigner
this file: clip_abs, lip_approx_cvg

lemma clip_abs source, line 785

forall {R : realType} [k : R] (x : R), 0 <= k -> `|clip k x| <= `|x|

Statement as written in the source

Lemma clip_abs (k x : R) : 0 <= k -> `|clip k x| <= `|x|.

Used by 1 declaration in 1 file

this file: lip_approx_dom

lemma clip_lipschitz source, line 791

forall {R : realType} (k x y : R), `|clip k x - clip k y| <= `|x - y|

Statement as written in the source

Lemma clip_lipschitz (k x y : R) : `|clip k x - clip k y| <= `|x - y|.

Used by 4 declarations in 3 files

GaussianAnalysis.random_matrix.goe: clip_pow_lipschitz
GaussianAnalysis.random_matrix.wigner: continuous_clip, clip_comp_lipschitz
this file: clipL

sectiongauss_concentration_lipschitz

Context {R : realType} {n : nat}.
Variables (F : 'rV[R]_n -> R) (L : R).
Hypothesis FL : forall x y, `|F x - F y| <= L * frobenius (x - y).

let cF section-local source, line 813

Let cF : continuous F := lipschitz_frobenius_continuous FL.

Used by 1 declaration in 1 file

this file: mF

let mF section-local source, line 814

Let mF : measurable_fun [set: 'rV[R]_n] F := continuous_measurable_mx cF.

Used by 1 declaration in 1 file

this file: gauss_concentration_upper_tail

let M section-local source, line 815

Let M : R := \int[gauss n]_y frobenius y.

Used by 4 declarations in 1 file

this file: M0, lip_approx_dom, lip_approx_cvg, lip_approx_mean

let M0 section-local source, line 817

Let M0 : 0 <= M.

lemma lipschitz_frobenius_bound source, line 820

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
forall x : 'rV_n, `|F x| <= `|F 0| + `|L| * frobenius x

Statement as written in the source

Lemma lipschitz_frobenius_bound x : `|F x| <= `|F 0| + `|L| * frobenius x.

Used by 2 declarations in 1 file

this file: integrable_gauss_lipschitz, gauss_poincare_lipschitz

lemma integrable_gauss_lipschitz source, line 827

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
(gauss n).-integrable [set: 'rV_n] (EFin \o F)

Statement as written in the source

Lemma integrable_gauss_lipschitz : (gauss n).-integrable [set: 'rV[R]_n] (EFin \o F).

Used by 22 declarations in 9 files

GaussianAnalysis.matrix.covering: gopnorm_mean, colmax_sep
GaussianAnalysis.matrix.tensor_packing: sudakov_mx_series, tensor_packing
GaussianAnalysis.random_matrix.goe: integrable_goe_opnorm
GaussianAnalysis.random_matrix.goe_edge: integrable_goe_lambda_max, integrable_goe_lambda_maxN
this file: lip_approx_mean, gauss_concentration_lower_tail
GaussianAnalysis.comparison.escape: integrable_gwidth, integrable_escape_inf, integrable_minmax_sph, integrable_gauss_opnorm, gauss_proj_mean_ge
GaussianAnalysis.comparison.cgmt: integrable_infsupX, integrable_infsupY, infsup_compare, cgmt_lower, cgmt_upper
GaussianAnalysis.comparison.cone_escape: cone_escape_lower_tail
GaussianAnalysis.comparison.sudakov: gauss_max_lower, sudakov_minoration

local definition lip_approx not exported source, line 839

Type

forall {R : realType} {n : nat}, ('rV_n -> R) -> nat -> 'rV_n -> R

Definition

Local Definition lip_approx (k : nat) : 'rV[R]_n -> R :=
  gauss_smooth (k.+1%:R^-1) (fun x => clip k.+1%:R (F x)).

The approximations of F: clip it to [-(k + 1), k + 1], then smooth it at the scale 1 / (k + 1).

Used by 6 declarations in 1 file

this file: lip_approx_mgf, lip_approx_dom, lip_approx_cvg, mA, lip_approx_mean, gauss_concentration

let clipL section-local source, line 842

Let clipL k x y : `|clip k.+1%:R (F x) - clip k.+1%:R (F y)| <= L * frobenius (x - y).

Used by 5 declarations in 1 file

this file: lip_approx_mgf, lip_approx_dom, lip_approx_cvg, mA, gauss_concentration

let clipK section-local source, line 845

Let clipK k x : `|clip k.+1%:R (F x)| <= k.+1%:R.

Used by 5 declarations in 1 file

this file: lip_approx_mgf, lip_approx_dom, lip_approx_cvg, mA, gauss_concentration

let ek0 section-local source, line 848

Let ek0 (k : nat) : 0 < k.+1%:R^-1 :> R.

Used by 3 declarations in 1 file

this file: lip_approx_mgf, lip_approx_dom, lip_approx_cvg

local lemma lip_approx_mgf not exported source, line 851

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
forall (k : nat) (t : R),
\int[gauss n]_x
   expR
     (t *
      (gauss_concentration.lip_approx F k x -
       \int[gauss n]_y gauss_concentration.lip_approx F k y)) <=
expR (t ^+ 2 * L ^+ 2 / 2)

Statement as written in the source

Local Lemma lip_approx_mgf k t :
  \int[gauss n]_x expR (t * (lip_approx k x - \int[gauss n]_y lip_approx k y)) <=
  expR (t ^+ 2 * L ^+ 2 / 2).

Used by 1 declaration in 1 file

this file: gauss_concentration

local lemma lip_approx_dom not exported source, line 863

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
forall (k : nat) (x : 'rV_n),
`|gauss_concentration.lip_approx F k x| <= `|F x| + `|L| * \int[gauss n]_y frobenius y

Statement as written in the source

Local Lemma lip_approx_dom k x : `|lip_approx k x| <= `|F x| + `|L| * M.

Used by 1 declaration in 1 file

this file: lip_approx_mean

local lemma lip_approx_cvg not exported source, line 873

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
forall [x : 'rV_n], gauss_concentration.lip_approx F x0 x @[x0 --> \oo] --> F x

Statement as written in the source

Local Lemma lip_approx_cvg x : lip_approx ^~ x @ \oo --> F x.

Used by 2 declarations in 1 file

this file: lip_approx_mean, gauss_concentration

let mA section-local source, line 890

Let mA k : measurable_fun [set: 'rV[R]_n] (lip_approx k).

Used by 2 declarations in 1 file

this file: lip_approx_mean, gauss_concentration

local lemma lip_approx_mean not exported source, line 896

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
\int[gauss n]_x gauss_concentration.lip_approx F k x @[k --> \oo] --> 
\int[gauss n]_x F x

Statement as written in the source

Local Lemma lip_approx_mean :
  (fun k => \int[gauss n]_x lip_approx k x) @ \oo --> \int[gauss n]_x F x.

Used by 1 declaration in 1 file

this file: gauss_concentration

theorem gauss_concentration main result source, line 930

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
forall t : R,
(\int[gauss n]_x (expR (t * (F x - \int[gauss n]_y F y)))%:E <=
 (expR (t ^+ 2 * L ^+ 2 / 2))%:E)%E

Gaussian concentration for Lipschitz functions (Tsirelson, Ibragimov and Sudakov), with the sharp constant.

Main result, as the README states it

Gaussian concentration (Tsirelson, Ibragimov, Sudakov): if F is L-Lipschitz for the Euclidean norm, then E[expR (t (F x - E F))] <= expR (t^2 L^2 / 2) for every real t.

Used in theories/ by: Gaussian/Lipschitz/Concentration

Statement as written in the source

Theorem gauss_concentration (t : R) :
  (\int[gauss n]_x (expR (t * (F x - \int[gauss n]_y F y)))%:E <=
   (expR (t ^+ 2 * L ^+ 2 / 2))%:E)%E.

Used by 4 declarations in 2 files

GaussianAnalysis.random_matrix.goe: goe_opnorm_mgf
this file: integrable_gauss_concentration, gauss_concentration_upper_tail, gauss_poincare_lipschitz

corollary integrable_gauss_concentration source, line 967

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
forall t : R,
(gauss n).-integrable [set: 'rV_n]
  (EFin \o (fun x : 'rV_n => expR (t * (F x - \int[gauss n]_y F y))))

Statement as written in the source

Corollary integrable_gauss_concentration (t : R) :
  (gauss n).-integrable [set: 'rV[R]_n]
    (EFin \o (fun x => expR (t * (F x - \int[gauss n]_y F y)))).

Used by 3 declarations in 2 files

GaussianAnalysis.random_matrix.goe: integrable_goe_opnorm_expR, goe_opnorm_mgf
this file: gauss_poincare_lipschitz

corollary gauss_concentration_upper_tail main result source, line 978

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
forall [u : R],
0 <= u ->
(gauss n [set x | (\int[gauss n]_y F y + u <= F x)%R] <=
 (expR (- u ^+ 2 / (2 * L ^+ 2)))%:E)%E

Main result, as the README states it

For such F and u >= 0, P(F x >= E F + u) and P(F x <= E F - u) are at most expR (- u^2 / (2 L^2)), and P(|F x - E F| >= u) is at most twice that.

Statement as written in the source

Corollary gauss_concentration_upper_tail (u : R) : 0 <= u ->
  (gauss n [set x | \int[gauss n]_y F y + u <= F x]%R <=
   (expR (- u ^+ 2 / (2 * L ^+ 2)))%:E)%E.

Used by 5 declarations in 3 files

GaussianAnalysis.random_matrix.goe_edge: goe_lambda_max_tail, goe_lambda_maxN_tail
this file: gauss_concentration_lower_tail, gauss_concentration_abs_tail
GaussianAnalysis.comparison.escape: gauss_opnorm_tail

sectiongauss_concentration_tails

Context {R : realType} {n : nat}.
Variables (F : 'rV[R]_n -> R) (L : R).
Hypothesis FL : forall x y, `|F x - F y| <= L * frobenius (x - y).

let mF section-local source, line 1014

Let mF : measurable_fun [set: 'rV[R]_n] F :=
  continuous_measurable_mx (lipschitz_frobenius_continuous FL).

Used by 1 declaration in 1 file

this file: gauss_concentration_abs_tail

corollary gauss_concentration_lower_tail main result source, line 1017

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
forall [u : R],
0 <= u ->
(gauss n [set x | (F x <= \int[gauss n]_y F y - u)%R] <=
 (expR (- u ^+ 2 / (2 * L ^+ 2)))%:E)%E

Main result

Stated in the README together with gauss_concentration_upper_tail.

Statement as written in the source

Corollary gauss_concentration_lower_tail (u : R) : 0 <= u ->
  (gauss n [set x | F x <= \int[gauss n]_y F y - u]%R <=
   (expR (- u ^+ 2 / (2 * L ^+ 2)))%:E)%E.

Used by 3 declarations in 2 files

this file: gauss_concentration_abs_tail
GaussianAnalysis.comparison.escape: gordon_escape_tail, gordon_projection_tail

corollary gauss_concentration_abs_tail main result source, line 1033

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
forall [u : R],
0 <= u ->
(gauss n [set x | (u <= `|F x - \int[gauss n]_y F y|)%R] <=
 (2 * expR (- u ^+ 2 / (2 * L ^+ 2)))%:E)%E

Main result

Stated in the README together with gauss_concentration_upper_tail.

Statement as written in the source

Corollary gauss_concentration_abs_tail (u : R) : 0 <= u ->
  (gauss n [set x | u <= `|F x - \int[gauss n]_y F y|]%R <=
   (2 * expR (- u ^+ 2 / (2 * L ^+ 2)))%:E)%E.

Used by 3 declarations in 2 files

GaussianAnalysis.random_matrix.wigner: goe_stat_conc
GaussianAnalysis.comparison.cgmt: cgmt_escape_tail, cgmt_aux_tail

Two inequalities for the exponential, by monotonicity: 2 y <= expR y - expR (- y) for y >= 0, and 2 + x^2 <= expR x + expR (- x), that is cosh x >= 1 + x^2 / 2.

sectionexpR_cosh

Context {R : realType}.

lemma is_derive_expRN source, line 1061

forall {R : realType} (z : R), is_derive z 1 (fun z0 : R => expR (- z0)) (- expR (- z))

Statement as written in the source

Lemma is_derive_expRN (z : R) : is_derive z 1 (fun z : R => expR (- z)) (- expR (- z)).

Used by 2 declarations in 1 file

this file: expR_sinh_ge, expR_cosh_ge

lemma expR_sinh_ge main result source, line 1068

forall {R : realType} [y : R], 0 <= y -> 2 * y <= expR y - expR (- y)

Main result

Stated in the README together with expR_cosh_ge.

Statement as written in the source

Lemma expR_sinh_ge (y : R) : 0 <= y -> 2 * y <= expR y - expR (- y).

Used by 1 declaration in 1 file

this file: expR_cosh_ge

lemma expR_cosh_ge main result source, line 1088

forall {R : realType} (x : R), 2 + x ^+ 2 <= expR x + expR (- x)

Main result, as the README states it

2 + x^2 <= expR x + expR (- x) for every real x, and 2 y <= expR y - expR (- y) for y >= 0.

Statement as written in the source

Lemma expR_cosh_ge (x : R) : 2 + x ^+ 2 <= expR x + expR (- x).

Used by 2 declarations in 2 files

this file: gauss_poincare_lipschitz
GaussianAnalysis.comparison.sudakov: gauss_shift_sym

The Gaussian Poincare inequality for Lipschitz functions: the variance of F x is at most L^2. For t > 0, cosh (t Y) >= 1 + t^2 Y^2 / 2 with Y = F x - E[F], and gauss_concentration bounds E[expR (t Y)] and E[expR (- t Y)]; so E[Y^2] <= L^2 expR (t^2 L^2 / 2), and t -> 0.

sectiongauss_poincare

Context {R : realType} {n : nat}.
Variables (F : 'rV[R]_n -> R) (L : R).
Hypothesis FL : forall x y, `|F x - F y| <= L * frobenius (x - y).

theorem gauss_poincare_lipschitz main result source, line 1124

forall {R : realType} {n : nat} [F : 'rV_n -> R] [L : R],
(forall x y : 'rV_n, `|F x - F y| <= L * frobenius (x - y)) ->
\int[gauss n]_x (F x - \int[gauss n]_y F y) ^+ 2 <= L ^+ 2

Main result, as the README states it

Gaussian Poincaré inequality for Lipschitz functions: if F is L-Lipschitz for the Euclidean norm and x has law gauss n, then E[(F x - E F)^2] <= L^2.

Used in theories/ by: Gaussian/Lipschitz/Variance

Statement as written in the source

Theorem gauss_poincare_lipschitz :
  \int[gauss n]_x (F x - \int[gauss n]_y F y) ^+ 2 <= L ^+ 2.

Used by 2 declarations in 2 files

GaussianAnalysis.random_matrix.goe: goe_tr_var
GaussianAnalysis.comparison.escape: gauss_proj_mean_ge

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.