On this page

Subgaussian and subexponential random variables

GaussianAnalysis.probability.subgaussianlibrary/probability/subgaussian.v967 lines31 lemmas and theorems, 3 definitionssource

Imports 4 library modules and 23 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, 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.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.numfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.analysis.probability_theory.normal_distribution

Imported by 6

Required by 19 files of the paper proofs

A real random variable X on a probability space P is subgaussian with constant K > 0 when E exp (X^2 / K^2) <= 2, and subexponential with constant L > 0 when E exp (|X| / L) <= 2. The least such constants are the norms psi_2 and psi_1 of Vershynin, High-Dimensional Probability, sections 2.5 and 2.7. Independent variables are functions f_i (x_i) of the coordinates of a tuple x of law tuple_prod mu n (lindeberg.v).

`subgaussian P X K`	0 < K, X is measurable and E exp (X^2 / K^2) <= 2
`subexponential P X L`	0 < L, X is measurable and E exp (\|X\| / L) <= 2
`psi2_norm P X`	the infimum of the K with subgaussian P X K

Main results, with explicit constants:

subgaussian_tail: P(|X| >= u) <= 2 exp (- u^2 / K^2) for u >= 0; subexponential_tail: P(|Y| >= u) <= 2 exp (- u / L);
subgaussian_moment: E X^(2k) <= 2 k! K^(2k), and every power of X is integrable (integrable_subgaussian_exprn);
subgaussian_mgf: if E X = 0, then E exp (l X) <= exp (3 l^2 K^2) for every real l;
subgaussian_of_mgf: conversely, if E exp (l X) <= exp (l^2 s^2) for every l, then X is subgaussian with every constant L > 0 such that 16 s^2 <= 3 L^2, by integrating against a standard normal law;
Hoeffding's inequality, for x of law tuple_prod mu n and centered f_i (x_i), subgaussian with constants K_i (subgaussian_sum_mgf, subgaussian_sum): E exp (l \sum_i a_i f_i (x_i)) <= exp (3 l^2 \sum_i a_i^2 K_i^2), and the sum is subgaussian with constant 4 (\sum_i a_i^2 K_i^2)^(1/2); for laws nu i of the line with mean 0, subgaussian with a common constant K (subgaussian_lincomb), E exp ((\sum_i a_i x_i)^2 / (16 K^2 \sum_i a_i^2)) <= 2 under tuple_prod nu n;
subexponential_sqr, subexponential_mul: X^2 is subexponential with constant K^2, and X Y with constant K L, for X, Y subgaussian with constants K, L; subexponential_center: Y - E Y is subexponential with constant 3 L when Y is with constant L; a subexponential Y is integrable (integrable_subexponential);
subexponential_mgf: if E Y = 0, then E exp (l Y) <= exp (16 l^2 L^2) for |l| <= 1 / (2 L);
Bernstein's inequality, for x of law tuple_prod mu n and centered f_i (x_i), subexponential with constants L_i, and reals a_i (subexponential_sum_mgf, bernstein_upper, bernstein): P(|\sum_i a_i f_i (x_i)| >= t) <= 2 exp (- min (t^2 / (64 s^2), t / (4 M))), where s^2 = \sum_i a_i^2 L_i^2 and M = \max_i |a_i| L_i; bernstein_sum: if every f_i has constant L, P(|\sum_(i < n) f_i (x_i)| >= t) <= 2 exp (- min (t^2 / (64 n L^2), t / (4 L))).

The scalar inequalities behind them: expR_le_quad (e^y <= 1 + y + y^2 e^|y|), exprn_le_expR (u^k <= k! e^u for u >= 0), le_expR34, expR_mean_le and expR_third_le; lee_prod_ge0 is the monotonicity of products of nonnegative extended reals.

Main results

Results	Statement
subgaussiansubexponentialpsi2_normsubgaussian_tailsubexponential_tailsubgaussian_momentintegrable_subgaussian_exprn	A random variable `X` is subgaussian with constant `K > 0` when `E exp (X^2 / K^2) <= 2`, subexponential with constant `L > 0` when `E exp (\|X\| / L) <= 2` (Vershynin's `psi_2` and `psi_1` conditions). A subgaussian `X` has `P(\|X\| >= u) <= 2 exp (- u^2 / K^2)` and `E X^(2k) <= 2 k! K^(2k)`, and every power of `X` is integrable; a subexponential `Y` has `P(\|Y\| >= u) <= 2 exp (- u / L)`.
subgaussian_mgfsubgaussian_of_mgfsubgaussian_sum_mgfsubgaussian_sumsubgaussian_lincomb	For `E X = 0`, `E exp (l X) <= exp (3 l^2 K^2)` for every `l`; conversely `E exp (l X) <= exp (l^2 s^2)` for every `l` gives the subgaussian condition for every `L` with `16 s^2 <= 3 L^2`. Hoeffding's inequality: for `x` of law `tuple_prod mu n` and centered subgaussian `f_i (x_i)` with constants `K_i`, `sum_i a_i f_i (x_i)` is subgaussian with constant `4 (sum_i a_i^2 K_i^2)^(1/2)`.
subexponential_sqrsubexponential_mulsubexponential_centerintegrable_subexponentialsubexponential_mgfbernsteinbernstein_sum	`X^2` and `X Y` are subexponential with constants `K^2` and `K L`, `Y - E Y` with `3 L`; for `E Y = 0`, `E exp (l Y) <= exp (16 l^2 L^2)` when `\|l\| <= 1 / (2 L)`. Bernstein's inequality: `P(\|sum_i a_i f_i (x_i)\| >= t) <= 2 exp (- min (t^2 / (64 s^2), t / (4 M)))` for independent centered subexponential `f_i (x_i)`, with `s^2 = sum_i a_i^2 L_i^2` and `M = max_i \|a_i\| L_i`.

Declarations34 exported

sectionscalar

Context {R : realType}.
Implicit Types (u y a : R).

lemma expR_mul1B_le1 source, line 81

forall {R : realType} (y : R), expR y * (1 - y) <= 1

e^y (1 - y) <= 1, from 1 - y <= e^(-y).

Statement as written in the source

Lemma expR_mul1B_le1 y : expR y * (1 - y) <= 1.

Used by 3 declarations in 2 files

this file: expR_le_quad, subexponential_center
GaussianAnalysis.probability.hanson_wright: subexponential_of_mgf

lemma expR_le_quad source, line 89

forall {R : realType} (y : R), expR y <= 1 + y + y ^+ 2 * expR `|y|

The remainder of the first-order Taylor expansion of exp.

Statement as written in the source

Lemma expR_le_quad y : expR y <= 1 + y + y ^+ 2 * expR `|y|.

Used by 2 declarations in 1 file

this file: subgaussian_mgf_pointwise, subexponential_mgf

lemma exprn_le_expR source, line 101

forall {R : realType} [u : R] (k : nat), 0 <= u -> u ^+ k <= k`!%:R * expR u

Statement as written in the source

Lemma exprn_le_expR u k : 0 <= u -> u ^+ k <= k`!%:R * expR u.

Used by 3 declarations in 2 files

this file: sqr_le_expR, subgaussian_exprn_le
GaussianAnalysis.probability.subgaussian_matrix: net_count_arith

lemma sqr_le_expR source, line 111

forall {R : realType} [u : R], 0 <= u -> u ^+ 2 <= 2 * expR u

Statement as written in the source

Lemma sqr_le_expR u : 0 <= u -> u ^+ 2 <= 2 * expR u.

Used by 1 declaration in 1 file

this file: subexponential_mgf

lemma le_expR34 source, line 114

forall {R : realType} [u : R], 0 <= u -> u <= expR (3 / 4 * u)

Statement as written in the source

Lemma le_expR34 u : 0 <= u -> u <= expR (3 / 4 * u).

Used by 1 declaration in 1 file

this file: subgaussian_mgf_pointwise

lemma expR_mean_le source, line 122

forall {R : realType} (a b : R), expR ((a + b) / 2) <= (expR a + expR b) / 2

Statement as written in the source

Lemma expR_mean_le a b : expR ((a + b) / 2) <= (expR a + expR b) / 2.

Used by 2 declarations in 2 files

this file: subexponential_mul
GaussianAnalysis.probability.hanson_wright: hanson_wright_mgf

lemma expR_third_le source, line 135

forall {R : realType} (y : R), expR (y / 3) <= (expR y + 2) / 3

Statement as written in the source

Lemma expR_third_le y : expR (y / 3) <= (expR y + 2) / 3.

Used by 2 declarations in 2 files

this file: subexponential_center
GaussianAnalysis.probability.hanson_wright: subexponential_of_mgf

sectionsubgaussian

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

definition subgaussian main result source, line 149

Type

forall [d : measure_display] [T : measurableType d] [R : realType],
probability T R -> (T -> R) -> R -> Prop

Definition

Definition subgaussian (X : T -> R) (K : R) : Prop :=
  [/\ 0 < K, measurable_fun [set: T] X &
      (\int[P]_t (expR (X t ^+ 2 / K ^+ 2))%:E <= 2%:E)%E].

Main result, as the README states it

A random variable X is subgaussian with constant K > 0 when E exp (X^2 / K^2) <= 2, subexponential with constant L > 0 when E exp (|X| / L) <= 2 (Vershynin's psi_2 and psi_1 conditions). A subgaussian X has P(|X| >= u) <= 2 exp (- u^2 / K^2) and E X^(2k) <= 2 k! K^(2k), and every power of X is integrable; a subexponential Y has P(|Y| >= u) <= 2 exp (- u / L).

Used by 16 declarations in 3 files

this file: psi2_norm, integrable_subgaussian_expR, subgaussian_moment, integrable_subgaussian_exprn, subgaussian_tail, subgaussian_mgf, subexponential_sqr, subexponential_mul, subgaussian_of_mgf, subgaussian_sum_mgf, subgaussian_sum, subgaussian_lincomb
GaussianAnalysis.probability.subgaussian_matrix: subgaussian_unit_ge1, norm_concentration, subgaussian_opnorm_tail
GaussianAnalysis.probability.mixture: subgaussian_mixture

definition subexponential main result source, line 153

Type

forall [d : measure_display] [T : measurableType d] [R : realType],
probability T R -> (T -> R) -> R -> Prop

Definition

Definition subexponential (Y : T -> R) (L : R) : Prop :=
  [/\ 0 < L, measurable_fun [set: T] Y &
      (\int[P]_t (expR (`|Y t| / L))%:E <= 2%:E)%E].

Main result

Stated in the README together with subgaussian.

Used by 19 declarations in 6 files

GaussianAnalysis.matrix.random_opnorm: subexponential_max_sum, opnorm_sum_subexponential
this file: subexponential_tail, subexponential_sqr, subexponential_mul, integrable_subexponential_expR, integrable_subexponential, subexponential_center, subexponential_mgf, subexponential_sum_mgf, bernstein_upper, bernstein, bernstein_sum
GaussianAnalysis.probability.subgaussian_matrix: norm_concentration
GaussianAnalysis.probability.mixture: subexponential_mixture
GaussianAnalysis.probability.hanson_wright: subexponential_of_mgf, sub_center, hanson_wright_subexponential
GaussianAnalysis.random_matrix.restricted_isometry: cross_tail

definition psi2_norm main result source, line 157

Type

forall [d : measure_display] [T : measurableType d] [R : realType],
probability T R -> (T -> R) -> R

Definition

Definition psi2_norm (X : T -> R) : R := inf [set K | subgaussian X K].

Main result

Stated in the README together with subgaussian.

sectionsubgaussian_props

Context d (T : measurableType d) (R : realType) (P : probability T R).
Local Open Scope ereal_scope.
Implicit Types (X Y : T -> R) (K L : R).

lemma measurable_expR_sqr source, line 166

forall [d : measure_display] [T : measurableType d] [R : realType] [X : T -> R] (K : R),
measurable_fun [set: T] X ->
measurable_fun [set: T] (fun t : T => expR (X t ^+ 2 / K ^+ 2))

Statement as written in the source

Lemma measurable_expR_sqr X K : measurable_fun [set: T] X ->
  measurable_fun [set: T] (fun t => expR (X t ^+ 2 / K ^+ 2)).

Used by 4 declarations in 1 file

this file: integrable_subgaussian_expR, subgaussian_moment, subgaussian_tail, subexponential_mul

lemma integrable_subgaussian_expR source, line 173

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [X : T -> R] [K : R],
subgaussian P X K -> P.-integrable [set: T] (fun t : T => (expR (X t ^+ 2 / K ^+ 2))%:E)

Statement as written in the source

Lemma integrable_subgaussian_expR X K : subgaussian P X K ->
  P.-integrable [set: T] (fun t => (expR (X t ^+ 2 / K ^+ 2))%:E).

Used by 2 declarations in 2 files

this file: subgaussian_mgf
GaussianAnalysis.probability.subgaussian_matrix: subgaussian_unit_ge1

lemma subgaussian_exprn_le source, line 182

forall [d : measure_display] [T : measurableType d] [R : realType] 
  (X : T -> R) [K : R] (k : nat) (t : T),
0 < K -> X t ^+ (2 * k) <= K ^+ (2 * k) * k`!%:R * expR (X t ^+ 2 / K ^+ 2)

Statement as written in the source

Lemma subgaussian_exprn_le X K k t : (0 < K)%R ->
  (X t ^+ (2 * k) <= K ^+ (2 * k) * k`!%:R * expR (X t ^+ 2 / K ^+ 2))%R.

Used by 1 declaration in 1 file

this file: subgaussian_moment

lemma subgaussian_moment main result source, line 191

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [X : T -> R] [K : R] (k : nat),
subgaussian P X K -> (\int[P]_t (X t ^+ (2 * k))%:E <= (2 * k`!%:R * K ^+ (2 * k))%:E)%E

Main result

Stated in the README together with subgaussian.

Statement as written in the source

Lemma subgaussian_moment X K k : subgaussian P X K ->
  \int[P]_t (X t ^+ (2 * k))%:E <= (2 * k`!%:R * K ^+ (2 * k))%:E.

Used by 1 declaration in 1 file

this file: integrable_subgaussian_exprn

lemma integrable_subgaussian_exprn main result source, line 210

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [X : T -> R] [K : R] (k : nat),
subgaussian P X K -> P.-integrable [set: T] (fun t : T => (X t ^+ k)%:E)

Main result

Stated in the README together with subgaussian.

Statement as written in the source

Lemma integrable_subgaussian_exprn X K k : subgaussian P X K ->
  P.-integrable [set: T] (fun t => (X t ^+ k)%:E).

Used by 3 declarations in 2 files

this file: subgaussian_mgf
GaussianAnalysis.probability.subgaussian_matrix: subgaussian_unit_ge1, norm_concentration

lemma subgaussian_tail main result source, line 237

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [X : T -> R] [K u : R],
subgaussian P X K ->
0 <= u -> (P [set t | (u <= `|X t|)%R] <= (2 * expR (- (u ^+ 2 / K ^+ 2)))%:E)%E

Main result

Stated in the README together with subgaussian.

Statement as written in the source

Lemma subgaussian_tail X K (u : R) : subgaussian P X K -> (0 <= u)%R ->
  P [set t | u <= `|X t|]%R <= (2 * expR (- (u ^+ 2 / K ^+ 2)))%:E.

Used by 1 declaration in 1 file

GaussianAnalysis.random_matrix.restricted_isometry: tuple_mx_dot_tail

lemma subexponential_tail main result source, line 258

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [Y : T -> R] [L : R] (u : R),
subexponential P Y L -> (P [set t | (u <= `|Y t|)%R] <= (2 * expR (- (u / L)))%:E)%E

Main result

Stated in the README together with subgaussian.

Statement as written in the source

Lemma subexponential_tail Y L (u : R) : subexponential P Y L ->
  P [set t | u <= `|Y t|]%R <= (2 * expR (- (u / L)))%:E.

lemma subgaussian_mgf_pointwise source, line 274

forall [R : realType] (x : R) [K : R] (l : R),
0 < K ->
expR (l * x) <=
1 + l * x + l ^+ 2 * K ^+ 2 * expR (l ^+ 2 * K ^+ 2) * expR (x ^+ 2 / K ^+ 2)

Statement as written in the source

Lemma subgaussian_mgf_pointwise (x K l : R) : (0 < K)%R ->
  (expR (l * x) <= 1 + l * x +
     l ^+ 2 * K ^+ 2 * expR (l ^+ 2 * K ^+ 2) * expR (x ^+ 2 / K ^+ 2))%R.

Used by 1 declaration in 1 file

this file: subgaussian_mgf

lemma subgaussian_mgf main result source, line 310

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [X : T -> R] [K : R] (l : R),
subgaussian P X K ->
\int[P]_t X t = 0 -> (\int[P]_t (expR (l * X t))%:E <= (expR (3 * l ^+ 2 * K ^+ 2))%:E)%E

Main result, as the README states it

For E X = 0, E exp (l X) <= exp (3 l^2 K^2) for every l; conversely E exp (l X) <= exp (l^2 s^2) for every l gives the subgaussian condition for every L with 16 s^2 <= 3 L^2. Hoeffding's inequality: for x of law tuple_prod mu n and centered subgaussian f_i (x_i) with constants K_i, sum_i a_i f_i (x_i) is subgaussian with constant 4 (sum_i a_i^2 K_i^2)^(1/2).

Statement as written in the source

Lemma subgaussian_mgf X K (l : R) :
  subgaussian P X K -> (\int[P]_t X t = 0)%R ->
  \int[P]_t (expR (l * X t))%:E <= (expR (3 * l ^+ 2 * K ^+ 2))%:E.

Used by 1 declaration in 1 file

this file: subgaussian_sum_mgf

sectionsubexponential_props

Context d (T : measurableType d) (R : realType) (P : probability T R).
Local Open Scope ereal_scope.
Implicit Types (X Y : T -> R) (K L : R).

lemma subexponential_sqr main result source, line 372

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [X : T -> R] [K : R],
subgaussian P X K -> subexponential P (fun t : T => X t ^+ 2) (K ^+ 2)

Main result, as the README states it

X^2 and X Y are subexponential with constants K^2 and K L, Y - E Y with 3 L; for E Y = 0, E exp (l Y) <= exp (16 l^2 L^2) when |l| <= 1 / (2 L). Bernstein's inequality: P(|sum_i a_i f_i (x_i)| >= t) <= 2 exp (- min (t^2 / (64 s^2), t / (4 M))) for independent centered subexponential f_i (x_i), with s^2 = sum_i a_i^2 L_i^2 and M = max_i |a_i| L_i.

Statement as written in the source

Lemma subexponential_sqr X K : subgaussian P X K ->
  subexponential P (fun t => X t ^+ 2)%R (K ^+ 2).

Used by 3 declarations in 2 files

GaussianAnalysis.probability.subgaussian_matrix: norm_concentration
GaussianAnalysis.probability.hanson_wright: sub_center, center0

lemma subexponential_mul main result source, line 382

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [X Y : T -> R] [K L : R],
subgaussian P X K -> subgaussian P Y L -> subexponential P (fun t : T => X t * Y t) (K * L)

Main result

Stated in the README together with subexponential_sqr.

Statement as written in the source

Lemma subexponential_mul X Y K L : subgaussian P X K -> subgaussian P Y L ->
  subexponential P (fun t => X t * Y t)%R (K * L).

lemma integrable_subexponential_expR source, line 421

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [Y : T -> R] [L : R],
subexponential P Y L -> P.-integrable [set: T] (fun t : T => (expR (`|Y t| / L))%:E)

Statement as written in the source

Lemma integrable_subexponential_expR Y L : subexponential P Y L ->
  P.-integrable [set: T] (fun t => (expR (`|Y t| / L))%:E).

Used by 3 declarations in 1 file

this file: integrable_subexponential, subexponential_center, subexponential_mgf

lemma integrable_subexponential main result source, line 433

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [Y : T -> R] [L : R],
subexponential P Y L -> P.-integrable [set: T] (EFin \o Y)

Main result

Stated in the README together with subexponential_sqr.

Statement as written in the source

Lemma integrable_subexponential Y L : subexponential P Y L ->
  P.-integrable [set: T] (EFin \o Y).

Used by 3 declarations in 2 files

this file: subexponential_center, subexponential_mgf
GaussianAnalysis.probability.hanson_wright: center0

lemma subexponential_center main result source, line 450

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [Y : T -> R] [L : R],
subexponential P Y L -> subexponential P (fun t : T => Y t - \int[P]_s Y s) (3 * L)

Main result

Stated in the README together with subexponential_sqr.

Statement as written in the source

Lemma subexponential_center Y L : subexponential P Y L ->
  subexponential P (fun t => Y t - \int[P]_s Y s)%R (3 * L).

Used by 2 declarations in 2 files

GaussianAnalysis.probability.subgaussian_matrix: norm_concentration
GaussianAnalysis.probability.hanson_wright: sub_center

lemma subexponential_mgf main result source, line 522

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [Y : T -> R] [L l : R],
subexponential P Y L ->
\int[P]_t Y t = 0 ->
`|l| <= (2 * L)^-1 -> (\int[P]_t (expR (l * Y t))%:E <= (expR (16 * l ^+ 2 * L ^+ 2))%:E)%E

Main result

Stated in the README together with subexponential_sqr.

Statement as written in the source

Lemma subexponential_mgf Y L (l : R) :
  subexponential P Y L -> (\int[P]_t Y t = 0)%R -> (`|l| <= (2 * L)^-1)%R ->
  \int[P]_t (expR (l * Y t))%:E <= (expR (16 * l ^+ 2 * L ^+ 2))%:E.

Used by 1 declaration in 1 file

this file: subexponential_sum_mgf

sectionsubgaussian_mgf_converse

Context d (T : measurableType d) (R : realType) (P : probability T R).
Local Open Scope ereal_scope.
Local Notation N := (@normal_prob R 0 1).

lemma subgaussian_of_mgf main result source, line 602

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [X : T -> R] [s L : R],
measurable_fun [set: T] X ->
0 < L ->
16 * s ^+ 2 <= 3 * L ^+ 2 ->
(forall l : R, (\int[P]_t (expR (l * X t))%:E <= (expR (l ^+ 2 * s ^+ 2))%:E)%E) ->
subgaussian P X L

Main result

Stated in the README together with subgaussian_mgf.

Statement as written in the source

Lemma subgaussian_of_mgf (X : T -> R) (s L : R) :
  measurable_fun [set: T] X -> (0 < L)%R -> (16 * s ^+ 2 <= 3 * L ^+ 2)%R ->
  (forall l : R,
    \int[P]_t (expR (l * X t))%:E <= (expR (l ^+ 2 * s ^+ 2))%:E) ->
  subgaussian P X L.

Used by 1 declaration in 1 file

this file: subgaussian_sum

sectionhoeffding

Context d (T : measurableType d) (R : realType).
Local Open Scope ereal_scope.

lemma lee_prod_ge0 source, line 658

forall [R : realType] [I : Type] (r : seq I) [P : pred I] [f g : I -> \bar R],
(forall i : I, P i -> (0%R <= f i)%E) ->
(forall i : I, P i -> (f i <= g i)%E) ->
(\prod_(i <- r | P i) f i <= \prod_(i <- r | P i) g i)%E

Products of nonnegative extended reals are monotone (as lee_prod of fourier/small_ball.v).

Statement as written in the source

Lemma lee_prod_ge0 I (r : seq I) (P : pred I) (f g : I -> \bar R) :
  (forall i, P i -> 0 <= f i) -> (forall i, P i -> f i <= g i) ->
  \prod_(i <- r | P i) f i <= \prod_(i <- r | P i) g i.

Used by 3 declarations in 2 files

GaussianAnalysis.matrix.covering: matrix_small_ball
this file: subgaussian_sum_mgf, subexponential_sum_mgf

lemma subgaussian_sum_mgf main result source, line 669

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [K : nat -> R] 
  (a : nat -> R) (l : R),
(forall i : nat, (i < n)%N -> subgaussian (mu i) (f i) (K i)) ->
(forall i : nat, (i < n)%N -> \int[mu i]_t f i t = 0) ->
(\int[tuple_prod mu n]_x (expR (l * \sum_(i < n) a i * f i (tnth x i)))%:E <=
 (expR (3 * l ^+ 2 * \sum_(i < n) a i ^+ 2 * K i ^+ 2))%:E)%E

Hoeffding: the moment generating function of a weighted sum of independent centered subgaussian variables.

Main result

Stated in the README together with subgaussian_mgf.

Statement as written in the source

Lemma subgaussian_sum_mgf (mu : nat -> probability T R) n (f : nat -> T -> R)
    (K a : nat -> R) (l : R) :
  (forall i, (i < n)%N -> subgaussian (mu i) (f i) (K i)) ->
  (forall i, (i < n)%N -> \int[mu i]_t f i t = 0)%R ->
  \int[tuple_prod mu n]_x (expR (l * \sum_(i < n) a i * f i (tnth x i)))%:E <=
  (expR (3 * l ^+ 2 * \sum_(i < n) a i ^+ 2 * K i ^+ 2))%:E.

Used by 3 declarations in 3 files

this file: subgaussian_sum
GaussianAnalysis.probability.subgaussian_matrix: subgaussian_opnorm_tail
GaussianAnalysis.probability.hanson_wright: hoeffding

lemma subgaussian_sum main result source, line 706

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [K a : nat -> R],
(forall i : nat, (i < n)%N -> subgaussian (mu i) (f i) (K i)) ->
(forall i : nat, (i < n)%N -> \int[mu i]_t f i t = 0) ->
0 < \sum_(i < n) a i ^+ 2 * K i ^+ 2 ->
subgaussian (tuple_prod mu n) (fun x : n.-tuple T => \sum_(i < n) a i * f i (tnth x i))
  (4 * Num.ExtraDef.sqrtr (\sum_(i < n) a i ^+ 2 * K i ^+ 2))

Main result

Stated in the README together with subgaussian_mgf.

Statement as written in the source

Lemma subgaussian_sum (mu : nat -> probability T R) n (f : nat -> T -> R)
    (K a : nat -> R) :
  (forall i, (i < n)%N -> subgaussian (mu i) (f i) (K i)) ->
  (forall i, (i < n)%N -> \int[mu i]_t f i t = 0)%R ->
  (0 < \sum_(i < n) a i ^+ 2 * K i ^+ 2)%R ->
  subgaussian (tuple_prod mu n) (fun x => \sum_(i < n) a i * f i (tnth x i))%R
    (4 * Num.sqrt (\sum_(i < n) a i ^+ 2 * K i ^+ 2))%R.

Used by 2 declarations in 2 files

this file: subgaussian_lincomb
GaussianAnalysis.random_matrix.restricted_isometry: tuple_mx_dot_tail

sectionlincomb

Context (R : realType).
Local Open Scope ereal_scope.

lemma subgaussian_lincomb main result source, line 736

forall [R : realType] [nu : nat -> probability (measurableTypeR R) R] 
  [n : nat] [K : R] (a : nat -> R),
(forall i : nat, (i < n)%N -> subgaussian (nu i) id K) ->
(forall i : nat, (i < n)%N -> \int[nu i]_x x = 0) ->
(\int[tuple_prod nu n]_x
    (expR ((\sum_(i < n) a i * tnth x i) ^+ 2 / (16 * K ^+ 2 * \sum_(i < n) a i ^+ 2)))%:E <=
 2)%E

Linear combinations of independent centered coordinates of the line, subgaussian with a common constant K.

Main result

Stated in the README together with subgaussian_mgf.

Statement as written in the source

Lemma subgaussian_lincomb (nu : nat -> probability (measurableTypeR R) R) n
    (K : R) (a : nat -> R) :
  (forall i, (i < n)%N -> subgaussian (nu i) (fun x => x) K) ->
  (forall i, (i < n)%N -> \int[nu i]_x x = 0)%R ->
  \int[tuple_prod nu n]_x (expR ((\sum_(i < n) a i * tnth x i) ^+ 2 /
     (16 * K ^+ 2 * \sum_(i < n) a i ^+ 2)))%:E <= 2%:E.

sectionbernstein

Context d (T : measurableType d) (R : realType).
Local Open Scope ereal_scope.

lemma subexponential_sum_mgf source, line 767

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [L a : nat -> R] 
  [l : R],
(forall i : nat, (i < n)%N -> subexponential (mu i) (f i) (L i)) ->
(forall i : nat, (i < n)%N -> \int[mu i]_t f i t = 0) ->
(forall i : nat, (i < n)%N -> `|l * a i| <= (2 * L i)^-1) ->
(\int[tuple_prod mu n]_x (expR (l * \sum_(i < n) a i * f i (tnth x i)))%:E <=
 (expR (16 * l ^+ 2 * \sum_(i < n) a i ^+ 2 * L i ^+ 2))%:E)%E

Statement as written in the source

Lemma subexponential_sum_mgf (mu : nat -> probability T R) n
    (f : nat -> T -> R) (L a : nat -> R) (l : R) :
  (forall i, (i < n)%N -> subexponential (mu i) (f i) (L i)) ->
  (forall i, (i < n)%N -> \int[mu i]_t f i t = 0)%R ->
  (forall i, (i < n)%N -> `|l * a i| <= (2 * L i)^-1)%R ->
  \int[tuple_prod mu n]_x (expR (l * \sum_(i < n) a i * f i (tnth x i)))%:E <=
  (expR (16 * l ^+ 2 * \sum_(i < n) a i ^+ 2 * L i ^+ 2))%:E.

Used by 3 declarations in 3 files

GaussianAnalysis.matrix.random_opnorm: subexponential_max_sum
this file: bernstein_upper
GaussianAnalysis.probability.hanson_wright: hw_diag_mgf

lemma bernstein_upper source, line 806

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [L : nat -> R] 
  (a : nat -> R) [t : R],
(forall i : nat, (i < n)%N -> subexponential (mu i) (f i) (L i)) ->
(forall i : nat, (i < n)%N -> \int[mu i]_s f i s = 0) ->
0 <= t ->
(tuple_prod mu n [set x | (t <= \sum_(i < n) a i * f i (tnth x i))%R] <=
 (expR
    (-
     Num.min (t ^+ 2 / (64 * \sum_(i < n) a i ^+ 2 * L i ^+ 2))
       (t / (4 * \big[Num.max/0]_(i < n) (`|a i| * L i)))))%:E)%E

Bernstein's inequality, upper tail.

Statement as written in the source

Lemma bernstein_upper (mu : nat -> probability T R) n (f : nat -> T -> R)
    (L a : nat -> R) (t : R) :
  (forall i, (i < n)%N -> subexponential (mu i) (f i) (L i)) ->
  (forall i, (i < n)%N -> \int[mu i]_s f i s = 0)%R -> (0 <= t)%R ->
  tuple_prod mu n [set x | t <= \sum_(i < n) a i * f i (tnth x i)]%R <=
  (expR (- Num.min (t ^+ 2 / (64 * \sum_(i < n) a i ^+ 2 * L i ^+ 2))
                   (t / (4 * \big[Num.max/0%R]_(i < n) (`|a i| * L i)))))%:E.

Used by 1 declaration in 1 file

this file: bernstein

lemma bernstein main result source, line 891

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [L : nat -> R] 
  (a : nat -> R) [t : R],
(forall i : nat, (i < n)%N -> subexponential (mu i) (f i) (L i)) ->
(forall i : nat, (i < n)%N -> \int[mu i]_s f i s = 0) ->
0 <= t ->
(tuple_prod mu n [set x | (t <= `|\sum_(i < n) a i * f i (tnth x i)|)%R] <=
 (2 *
  expR
    (-
     Num.min (t ^+ 2 / (64 * \sum_(i < n) a i ^+ 2 * L i ^+ 2))
       (t / (4 * \big[Num.max/0]_(i < n) (`|a i| * L i)))))%:E)%E

Bernstein's inequality.

Main result

Stated in the README together with subexponential_sqr.

Statement as written in the source

Lemma bernstein (mu : nat -> probability T R) n (f : nat -> T -> R)
    (L a : nat -> R) (t : R) :
  (forall i, (i < n)%N -> subexponential (mu i) (f i) (L i)) ->
  (forall i, (i < n)%N -> \int[mu i]_s f i s = 0)%R -> (0 <= t)%R ->
  tuple_prod mu n [set x | t <= `|\sum_(i < n) a i * f i (tnth x i)|]%R <=
  (2 * expR (- Num.min (t ^+ 2 / (64 * \sum_(i < n) a i ^+ 2 * L i ^+ 2))
      (t / (4 * \big[Num.max/0%R]_(i < n) (`|a i| * L i)))))%:E.

Used by 2 declarations in 2 files

this file: bernstein_sum
GaussianAnalysis.random_matrix.restricted_isometry: cross_tail

lemma bernstein_sum main result source, line 935

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [L t : R],
(forall i : nat, (i < n)%N -> subexponential (mu i) (f i) L) ->
(forall i : nat, (i < n)%N -> \int[mu i]_s f i s = 0) ->
0 <= t ->
(tuple_prod mu n [set x | (t <= `|\sum_(i < n) f i (tnth x i)|)%R] <=
 (2 * expR (- Num.min (t ^+ 2 / (64 * n%:R * L ^+ 2)) (t / (4 * L))))%:E)%E

Bernstein's inequality for a sum of independent centered variables subexponential with a common constant L.

Main result

Stated in the README together with subexponential_sqr.

Statement as written in the source

Lemma bernstein_sum (mu : nat -> probability T R) n (f : nat -> T -> R)
    (L t : R) :
  (forall i, (i < n)%N -> subexponential (mu i) (f i) L) ->
  (forall i, (i < n)%N -> \int[mu i]_s f i s = 0)%R -> (0 <= t)%R ->
  tuple_prod mu n [set x | t <= `|\sum_(i < n) f i (tnth x i)|]%R <=
  (2 * expR (- Num.min (t ^+ 2 / (64 * n%:R * L ^+ 2)) (t / (4 * L))))%:E.

Used by 1 declaration in 1 file

GaussianAnalysis.probability.subgaussian_matrix: norm_concentration

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.