On this page
Norms of random vectors and matrices with subgaussian coordinates
Imports 8 library modules and 24 external
- GaussianAnalysis.gaussian.measurable_matrix
- GaussianAnalysis.matrix.euclidean
- GaussianAnalysis.matrix.opnorm
- GaussianAnalysis.matrix.nets
- GaussianAnalysis.comparison.normal_mgf
- GaussianAnalysis.comparison.gauss_smoothing
- GaussianAnalysis.probability.lindeberg
- GaussianAnalysis.probability.subgaussian
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.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.analysis.realfun, 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
Independent coordinates are functions f_i (x_i) of the coordinates of a tuple x of law tuple_prod mu n (lindeberg.v), subgaussian with a common constant K (subgaussian.v). The results are Theorems 3.1.1 and 4.4.5 of Vershynin, High-Dimensional Probability, with explicit constants.
Main results:
- subgaussian_unit_ge1: a subgaussian constant K of a variable X with E X^2 = 1 is at least 1;
- norm_concentration: if E f_i (x_i)^2 = 1 for every i, the Euclidean norm |x| = (\sum_i f_i (x_i)^2)^(1/2) satisfies, for t >= 0,
P(| |x| - sqrt n | >= t) <= 2 exp (- t^2 / (576 K^4)),
from Bernstein's inequality (bernstein_sum) for the centered subexponential variables f_i (x_i)^2 - 1; the f_i need not be centered;
- mgf_tail: P(|X| >= r) <= 2 exp (- r^2 / (4 s^2)) for r >= 0 when E exp (l X) <= exp (s^2 l^2) for every real l;
- opnorm_tail_mgf: for a random m x n matrix A with measurable entries whose bilinear forms u^T A v, |u|, |v| <= 1, satisfy E exp (l u^T A v) <= exp (s^2 l^2) for every real l, and t >= 0,
P(opnorm A > 12 s (sqrt m + sqrt n + t)) <= 2 exp (- t^2),
by 1/4-nets of the unit balls (unit_ball_net and opnorm_net_bilinear of nets.v) and the union bound;
- subgaussian_opnorm_tail: for the m x n matrix A = vec_mx (f_k (x_k))_k of independent centered entries, subgaussian with constant K, and t >= 0,
P(opnorm A > 21 K (sqrt m + sqrt n + t)) <= 2 exp (- t^2),
from Hoeffding's inequality (subgaussian_sum_mgf) with s = sqrt 3 K.
Main results
| Results | Statement |
|---|---|
A subgaussian constant K of X with E X^2 = 1 is at least 1. Concentration of the norm (Vershynin, Theorem 3.1.1): for x of law tuple_prod mu n and f_i (x_i) subgaussian with constant K and E f_i (x_i)^2 = 1 (not necessarily centered), P(|(sum_i f_i (x_i)^2)^(1/2) - sqrt n| >= t) <= 2 exp (- t^2 / (576 K^4)) for t >= 0. | |
P(|X| >= r) <= 2 exp (- r^2 / (4 s^2)) when E exp (l X) <= exp (s^2 l^2) for every l. For a random m x n matrix A with measurable entries (then opnorm A is measurable) whose bilinear forms u^T A v, |u|, |v| <= 1, satisfy that bound, P(opnorm A > 12 s (sqrt m + sqrt n + t)) <= 2 exp (- t^2) for t >= 0, by nets of the unit balls. For independent centered entries subgaussian with constant K (Vershynin, Theorem 4.4.5): P(opnorm A > 21 K (sqrt m + sqrt n + t)) <= 2 exp (- t^2). |
Declarations7 exported, 8 local
Context d (T : measurableType d) (R : realType) (P : probability T R).
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R] [K : R], subgaussian P X K -> \int[P]_t X t ^+ 2 = 1 -> 1 <= K
X^2 <= K^2 (exp (X^2 / K^2) - 1), integrated: 1 <= K^2 (2 - 1).
A subgaussian constant K of X with E X^2 = 1 is at least 1. Concentration of the norm (Vershynin, Theorem 3.1.1): for x of law tuple_prod mu n and f_i (x_i) subgaussian with constant K and E f_i (x_i)^2 = 1 (not necessarily centered), P(|(sum_i f_i (x_i)^2)^(1/2) - sqrt n| >= t) <= 2 exp (- t^2 / (576 K^4)) for t >= 0.
Statement as written in the source
Lemma subgaussian_unit_ge1 (X : T -> R) (K : R) : subgaussian P X K -> \int[P]_t X t ^+ 2 = 1 -> 1 <= K.
Used by 1 declaration in 1 file
- this file: norm_concentration
Context {R : realType}.
forall {R : realType} [a b t : R],
0 <= a ->
0 <= b -> 0 <= t -> t <= `|a - b| -> Num.max (t ^+ 2) (t * b) <= `|a ^+ 2 - b ^+ 2||a^2 - b^2| = |a - b| (a + b) >= t max (t, b) when |a - b| >= t.
Statement as written in the source
Local Lemma sqr_gap (a b t : R) : 0 <= a -> 0 <= b -> 0 <= t -> t <= `|a - b| -> Num.max (t ^+ 2) (t * b) <= `|a ^+ 2 - b ^+ 2|.
Used by 1 declaration in 1 file
- this file: norm_concentration
forall {R : realType} [K t N : R],
1 <= K ->
0 <= t ->
0 < N ->
t ^+ 2 / (576 * K ^+ 4) <=
Num.min (Num.max (t ^+ 2) (t * Num.ExtraDef.sqrtr N) ^+ 2 / (64 * N * (3 * K ^+ 2) ^+ 2))
(Num.max (t ^+ 2) (t * Num.ExtraDef.sqrtr N) / (4 * (3 * K ^+ 2)))The exponent of Bernstein's inequality for the norm.
Statement as written in the source
Local Lemma norm_conc_arith (K t N : R) : 1 <= K -> 0 <= t -> 0 < N -> t ^+ 2 / (576 * K ^+ 4) <= Num.min (Num.max (t ^+ 2) (t * Num.sqrt N) ^+ 2 / (64 * N * (3 * K ^+ 2) ^+ 2)) (Num.max (t ^+ 2) (t * Num.sqrt N) / (4 * (3 * K ^+ 2))).
Used by 1 declaration in 1 file
- this file: norm_concentration
forall {R : realType} (m n : nat), (m%:R + n%:R : R) <= ((Num.ExtraDef.sqrtr m%:R + Num.ExtraDef.sqrtr n%:R) ^+ 2 : R)
sqrt (m + n) <= sqrt m + sqrt n, squared.
Statement as written in the source
Local Lemma sqrt_add_sqr (m n : nat) : m%:R + n%:R <= (Num.sqrt m%:R + Num.sqrt n%:R) ^+ 2 :> R.
Used by 1 declaration in 1 file
- this file: net_count_arith
forall {R : realType} [m n : nat] [s t NU NV : R], 0 < s -> 0 <= t -> 0 <= NU -> NU <= (2 * expR 1 * (1 + 2 / 4^-1)) ^+ m -> 0 <= NV -> NV <= (2 * expR 1 * (1 + 2 / 4^-1)) ^+ n -> NU * (NV * (2 * expR (- ((2 * s * (3 * (Num.ExtraDef.sqrtr m%:R + Num.ExtraDef.sqrtr n%:R) + t)) ^+ 2 / (4 * s ^+ 2))))) <= 2 * expR (- t ^+ 2)
The count of the union bound over two 1/4-nets.
Statement as written in the source
Local Lemma net_count_arith (m n : nat) (s t NU NV : R) : 0 < s -> 0 <= t -> 0 <= NU -> NU <= (2 * expR 1 * (1 + 2 / 4^-1)) ^+ m -> 0 <= NV -> NV <= (2 * expR 1 * (1 + 2 / 4^-1)) ^+ n -> NU * (NV * (2 * expR (- ((2 * s * (3 * (Num.sqrt m%:R + Num.sqrt n%:R) + t)) ^+ 2 / (4 * s ^+ 2))))) <= 2 * expR (- t ^+ 2).
Used by 1 declaration in 1 file
- this file: opnorm_tail_mgf
Context d (T : measurableType d) (R : realType). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType] [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [K t : R], (forall i : nat, (i < n)%N -> subgaussian (mu i) (f i) K) -> (forall i : nat, (i < n)%N -> \int[mu i]_s f i s ^+ 2 = 1) -> 0 <= t -> (tuple_prod mu n [set x | (t <= `|Num.ExtraDef.sqrtr (\sum_(i < n) f i (tnth x i) ^+ 2) - Num.ExtraDef.sqrtr n%:R|)%R] <= (2 * expR (- (t ^+ 2 / (576 * K ^+ 4))))%:E)%E
Stated in the README together with subgaussian_unit_ge1.
Statement as written in the source
Theorem norm_concentration (mu : nat -> probability T R) n (f : nat -> T -> R) (K t : R) : (forall i, (i < n)%N -> subgaussian (mu i) (f i) K) -> (forall i, (i < n)%N -> \int[mu i]_s f i s ^+ 2 = 1)%R -> (0 <= t)%R -> tuple_prod mu n [set x | t <= `|Num.sqrt (\sum_(i < n) f i (tnth x i) ^+ 2) - Num.sqrt n%:R|]%R <= (2 * expR (- (t ^+ 2 / (576 * K ^+ 4))))%:E.
Context d (T : measurableType d) (R : realType) (P : probability T R). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType] (P : probability T R) [I : Type] (s : seq I) [F : I -> set T], (forall i : I, d.-measurable (F i)) -> (P (\big[setU/set0]_(i <- s) F i) <= (\sum_(i <- s) P (F i))%R)%E
Statement as written in the source
Local Lemma measure_bigsetU_seq (I : Type) (s : seq I) (F : I -> set T) : (forall i, measurable (F i)) -> P (\big[setU/set0]_(i <- s) F i) <= \sum_(i <- s) P (F i).
Used by 1 declaration in 1 file
- this file: opnorm_tail_mgf
forall [d : measure_display] [T : measurableType d] [I : eqType] [s : seq I] [F : I -> set T] [i : I] [x : T], i \in s -> F i x -> (\big[setU/set0]_(j <- s) F j) x
Statement as written in the source
Local Lemma in_bigsetU (I : eqType) (s : seq I) (F : I -> set T) i x : i \in s -> F i x -> (\big[setU/set0]_(j <- s) F j) x.
Used by 1 declaration in 1 file
- this file: opnorm_tail_mgf
Context d (T : measurableType d) (R : realType).
Statement as written in the source
Used by 1 declaration in 1 file
- this file: measurable_opnorm
Statement as written in the source
Used by 2 declarations in 1 file
- this file: measurable_opnorm, subgaussian_opnorm_tail
forall [d : measure_display] [T : measurableType d] [R : realType] [m n : nat] [A : T -> 'M_(m, n)], (forall (i : 'I_m) (j : 'I_n), measurable_fun [set: T] (fun x : T => A x i j)) -> measurable_fun [set: T] (fun x : T => opnorm (A x))
The operator norm of a random matrix with measurable entries is measurable: it is 1-Lipschitz for the Frobenius norm.
Stated in the README together with mgf_tail.
Statement as written in the source
Lemma measurable_opnorm m n (A : T -> 'M[R]_(m, n)) : (forall i j, measurable_fun [set: T] (fun x => A x i j)) -> measurable_fun [set: T] (fun x => opnorm (A x)).
Used by 2 declarations in 1 file
- this file: opnorm_tail_mgf, subgaussian_opnorm_tail
Context d (T : measurableType d) (R : realType) (P : probability T R). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R] [s r : R], measurable_fun [set: T] X -> 0 < s -> 0 <= r -> (forall l : R, (\int[P]_x (expR (l * X x))%:E <= (expR (s ^+ 2 * l ^+ 2))%:E)%E) -> (P [set x | (r <= X x)%R] <= (expR (- (r ^+ 2 / (4 * s ^+ 2))))%:E)%E
Chernoff's bound for a variable with a subgaussian moment generating function.
Statement as written in the source
Lemma mgf_upper_tail (X : T -> R) (s r : R) : measurable_fun [set: T] X -> (0 < s)%R -> (0 <= r)%R -> (forall l : R, \int[P]_x (expR (l * X x))%:E <= (expR (s ^+ 2 * l ^+ 2))%:E) -> P [set x | r <= X x]%R <= (expR (- (r ^+ 2 / (4 * s ^+ 2))))%:E.
Used by 1 declaration in 1 file
- this file: mgf_tail
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R] [s r : R], measurable_fun [set: T] X -> 0 < s -> 0 <= r -> (forall l : R, (\int[P]_x (expR (l * X x))%:E <= (expR (s ^+ 2 * l ^+ 2))%:E)%E) -> (P [set x | (r <= `|X x|)%R] <= (2 * expR (- (r ^+ 2 / (4 * s ^+ 2))))%:E)%E
P(|X| >= r) <= 2 exp (- r^2 / (4 s^2)) when E exp (l X) <= exp (s^2 l^2) for every l. For a random m x n matrix A with measurable entries (then opnorm A is measurable) whose bilinear forms u^T A v, |u|, |v| <= 1, satisfy that bound, P(opnorm A > 12 s (sqrt m + sqrt n + t)) <= 2 exp (- t^2) for t >= 0, by nets of the unit balls. For independent centered entries subgaussian with constant K (Vershynin, Theorem 4.4.5): P(opnorm A > 21 K (sqrt m + sqrt n + t)) <= 2 exp (- t^2).
Statement as written in the source
Lemma mgf_tail (X : T -> R) (s r : R) : measurable_fun [set: T] X -> (0 < s)%R -> (0 <= r)%R -> (forall l : R, \int[P]_x (expR (l * X x))%:E <= (expR (s ^+ 2 * l ^+ 2))%:E) -> P [set x | r <= `|X x|]%R <= (2 * expR (- (r ^+ 2 / (4 * s ^+ 2))))%:E.
Used by 1 declaration in 1 file
- this file: opnorm_tail_mgf
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [m n : nat] [A : T -> 'M_(m, n)] [s t : R], (forall (i : 'I_m) (j : 'I_n), measurable_fun [set: T] (fun x : T => A x i j)) -> 0 < s -> 0 <= t -> (forall (u : 'cV_m) (v : 'cV_n) (l : R), frobenius u <= 1 -> frobenius v <= 1 -> (\int[P]_x (expR (l * mxdot u (A x *m v)))%:E <= (expR (s ^+ 2 * l ^+ 2))%:E)%E) -> (P [set x | (12 * s * (Num.ExtraDef.sqrtr m%:R + Num.ExtraDef.sqrtr n%:R + t) < opnorm (A x))%R] <= (2 * expR (- t ^+ 2))%:E)%E
Stated in the README together with mgf_tail.
Statement as written in the source
Theorem opnorm_tail_mgf m n (A : T -> 'M[R]_(m, n)) (s t : R) : (forall i j, measurable_fun [set: T] (fun x => A x i j)) -> (0 < s)%R -> (0 <= t)%R -> (forall (u : 'cV[R]_m) (v : 'cV[R]_n) (l : R), (frobenius u <= 1)%R -> (frobenius v <= 1)%R -> \int[P]_x (expR (l * mxdot u (A x *m v)))%:E <= (expR (s ^+ 2 * l ^+ 2))%:E) -> P [set x | 12 * s * (Num.sqrt m%:R + Num.sqrt n%:R + t) < opnorm (A x)]%R <= (2 * expR (- t ^+ 2))%:E.
Used by 1 declaration in 1 file
- this file: subgaussian_opnorm_tail
Context d (T : measurableType d) (R : realType). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType] [mu : nat -> probability T R] [m n : nat] [f : nat -> T -> R] [K t : R], (forall k : nat, (k < m * n)%N -> subgaussian (mu k) (f k) K) -> (forall k : nat, (k < m * n)%N -> \int[mu k]_s f k s = 0) -> 0 < K -> 0 <= t -> (tuple_prod mu (m * n) [set x | (21 * K * (Num.ExtraDef.sqrtr m%:R + Num.ExtraDef.sqrtr n%:R + t) < opnorm (vec_mx (\row_k f k (tnth x k)) : 'M_(m, n)))%R] <= (2 * expR (- t ^+ 2))%:E)%E
Stated in the README together with mgf_tail.
Statement as written in the source
Theorem subgaussian_opnorm_tail (mu : nat -> probability T R) m n (f : nat -> T -> R) (K t : R) : (forall k, (k < m * n)%N -> subgaussian (mu k) (f k) K) -> (forall k, (k < m * n)%N -> \int[mu k]_s f k s = 0)%R -> (0 < K)%R -> (0 <= t)%R -> tuple_prod mu (m * n) [set x | 21 * K * (Num.sqrt m%:R + Num.sqrt n%:R + t) < opnorm (vec_mx (\row_k f k (tnth x k)) : 'M[R]_(m, n))]%R <= (2 * expR (- t ^+ 2))%:E.