On this page

The operator norm of a sum of independent random matrices

GaussianAnalysis.matrix.random_opnormlibrary/matrix/random_opnorm.v524 lines13 lemmas and theorems, 1 definitionsource

Imports 7 library modules and 24 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_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.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

Required by 1 files of the paper proofs

extension/Unsat/Ridge.v

A bound by nets and the moment generating function of sums of independent subexponential variables, used for Lemma 4.3 of Koehler and Sohn (arXiv 2608.27372, lines 4604-4615) in place of the matrix Bernstein inequality that the paper cites; it gives the bound without the logarithmic factor.

Main results:

Quadratic forms, mxdot_psd_le: for S symmetric positive semidefinite and any square A, |<A, S>| <= opnorm (sym_part A) tr S, where <., .> is the Frobenius product mxdot; sym_part_form, mxdot_sym_part: v^T A v and <A, S> only see the symmetric part.
Nets, unit_ball_quarter_net: the unit ball of 'cV[R]_n has a 1/4-net of at most (18 e)^n of its points; opnorm_sym_part_net: for such a net V, opnorm (sym_part A) <= 2 max_{v in V} |v^T A v|.
Maximal inequality, subexponential_max_sum: for x of law tuple_prod mu n, a finite family of functions g_v, each centered and subexponential with constant L under every mu i, and |a_i| <= 1,
```
E max_v |sum_i a_i g_v(x_i)| <= 8 L (sqrt (n Lam) + Lam)
```
with Lam = 1 + ln (1 + 2 N), N the size of the family. Proof: the moment generating function of each sum (subexponential_sum_mgf of subgaussian.v), expR_bigmax_le (exp (l max_v |S_v|) is at most 1 + sum_v (exp (l S_v) + exp (- l S_v))), expectation_le_ln_mgf (if E exp (l Z) <= B with ln B >= 1, then E Z <= ln B / l, from e^y >= 1 + y), and a choice of l.
Random matrices, opnorm_sum_subexponential: for x of law tuple_prod mu n and Y : T -> 'M[R]_m whose quadratic forms v^T Y v (|v| <= 1) are centered and subexponential with constant L under every mu k, there are measurable functions N a such that, for all weights with |a_k| <= 1, opnorm (sym_part (sum_k a_k Y(x_k))) <= N a x and
```
E N a <= 96 L (sqrt (n (m + 1)) + m + 1).
```
N a x is 2 max_{v in V} |v^T (sum_k a_k Y(x_k)) v| on the net V; net_log_le bounds the logarithm of the size of the net by 6 (m + 1).

sym_part A (A + A^T) / 2, the symmetric part of a square matrix

Main results

Results	Statement
sym_partmxdot_psd_leopnorm_sym_part_netunit_ball_quarter_net	For `S` symmetric positive semidefinite and any square `A`, `\|<A, S>\| <= opnorm (sym_part A) tr S`, where `sym_part A = (A + A^T) / 2` and `<., .>` is the Frobenius product. The unit ball of `'cV[R]_n` has a `1/4`-net `V` of at most `(18 e)^n` of its points, and `opnorm (sym_part A) <= 2 max_{v in V} \|v^T A v\|`.
subexponential_max_sum	Maximal inequality: for `x` of law `tuple_prod mu n`, a family of `N` functions `g_v`, each centered and subexponential with constant `L` under every `mu i`, and `\|a_i\| <= 1`, `E max_v \|sum_i a_i g_v(x_i)\| <= 8 L (sqrt (n Lam) + Lam)` with `Lam = 1 + ln (1 + 2 N)`. Proved with the moment generating function of each sum and `e^y >= 1 + y`.
opnorm_sum_subexponential	For `x` of law `tuple_prod mu n` and `Y : T -> 'M[R]_m` whose quadratic forms `v^T Y v` (`\|v\| <= 1`) are centered and subexponential with constant `L` under every `mu k`, there are measurable `N a` with `opnorm (sym_part (sum_k a_k Y(x_k))) <= N a x` and `E N a <= 96 L (sqrt (n (m + 1)) + m + 1)` for all weights with `\|a_k\| <= 1`. Unlike the matrix Bernstein inequality, the bound has no logarithmic factor.

Declarations14 exported

sectionquadratic_forms

Context {R : realType}.

definition sym_part main result source, line 66

Type

forall {R : realType} [n : nat], 'M_n -> 'M_n

Definition

Definition sym_part n (A : 'M[R]_n) : 'M[R]_n := 2^-1 *: (A + A^T).

The symmetric part (A + A^T) / 2 of a square matrix.

Main result, as the README states it

For S symmetric positive semidefinite and any square A, |<A, S>| <= opnorm (sym_part A) tr S, where sym_part A = (A + A^T) / 2 and <., .> is the Frobenius product. The unit ball of 'cV[R]_n has a 1/4-net V of at most (18 e)^n of its points, and opnorm (sym_part A) <= 2 max_{v in V} |v^T A v|.

Used by 6 declarations in 1 file

this file: sym_part_sym, sym_part_form, mxdot_sym_part, mxdot_psd_le, opnorm_sym_part_net, opnorm_sum_subexponential

lemma sym_part_sym source, line 68

forall {R : realType} [n : nat] (A : 'M_n), sym_part A \is symmetricmx

Statement as written in the source

Lemma sym_part_sym n (A : 'M[R]_n) : sym_part A \is symmetricmx.

Used by 1 declaration in 1 file

this file: opnorm_sym_part_net

lemma mxdot_trmx_form source, line 73

forall {R : realType} [n : nat] (A : 'M_n) (v : 'cV_n),
mxdot v (A^T *m v) = mxdot v (A *m v)

Statement as written in the source

Lemma mxdot_trmx_form n (A : 'M[R]_n) (v : 'cV[R]_n) :
  mxdot v (A^T *m v) = mxdot v (A *m v).

Used by 1 declaration in 1 file

this file: sym_part_form

lemma sym_part_form source, line 77

forall {R : realType} [n : nat] (A : 'M_n) (v : 'cV_n),
mxdot v (sym_part A *m v) = mxdot v (A *m v)

Statement as written in the source

Lemma sym_part_form n (A : 'M[R]_n) (v : 'cV[R]_n) :
  mxdot v (sym_part A *m v) = mxdot v (A *m v).

Used by 1 declaration in 1 file

this file: opnorm_sym_part_net

lemma mxdot_sym_part source, line 84

forall {R : realType} [n : nat] (A : 'M_n) [S : 'M_n],
S \is symmetricmx -> mxdot (sym_part A) S = mxdot A S

Statement as written in the source

Lemma mxdot_sym_part n (A S : 'M[R]_n) : S \is symmetricmx ->
  mxdot (sym_part A) S = mxdot A S.

Used by 1 declaration in 1 file

this file: mxdot_psd_le

lemma mxdot_psd_le main result source, line 93

forall {R : realType} [n : nat] (A : 'M_n) [S0 : 'M_n],
S0 \is symmetricmx ->
(forall x : 'cV_n, 0 <= mxdot x (S0 *m x)) -> `|mxdot A S0| <= opnorm (sym_part A) * \tr S0

The Frobenius product with a positive semidefinite matrix.

Main result

Stated in the README together with sym_part.

Statement as written in the source

Lemma mxdot_psd_le n (A S : 'M[R]_n) : S \is symmetricmx ->
  (forall x : 'cV[R]_n, 0 <= mxdot x (S *m x)) ->
  `|mxdot A S| <= opnorm (sym_part A) * \tr S.

lemma opnorm_sym_part_net main result source, line 118

forall {R : realType} [n : nat] (A : 'M_n) [V : seq 'cV_n],
is_net (unit_ball (n:=n)) V 4^-1 ->
(forall v : 'cV[R]_n, v \in V -> frobenius v <= 1) ->
opnorm (sym_part A) <= 2 * \big[maxr/0]_(v <- V) `|mxdot v (A *m v)|

On a net of the unit ball, the quadratic forms bound the operator norm of the symmetric part.

Main result

Stated in the README together with sym_part.

Statement as written in the source

Lemma opnorm_sym_part_net n (A : 'M[R]_n) (V : seq 'cV[R]_n) :
  is_net (@unit_ball R n) V (4^-1) -> (forall v, v \in V -> frobenius v <= 1) ->
  opnorm (sym_part A) <= 2 * \big[Num.max/0]_(v <- V) `|mxdot v (A *m v)|.

Used by 1 declaration in 1 file

this file: opnorm_sum_subexponential

lemma unit_ball_quarter_net main result source, line 133

forall {R : realType} (n : nat),
exists V : seq 'cV_n,
  [/\ is_net (unit_ball (n:=n)) V 4^-1,
      forall v : 'cV[R]_n,
      v \in V -> frobenius v <= 1
    & ((size V)%:R : R) <= ((18 * expR 1) ^+ n : R)]

Main result

Stated in the README together with sym_part.

Statement as written in the source

Lemma unit_ball_quarter_net n : exists V : seq 'cV[R]_n,
  [/\ is_net (@unit_ball R n) V (4^-1),
    (forall v, v \in V -> frobenius v <= 1) &
    (size V)%:R <= (18 * expR 1) ^+ n :> R].

Used by 1 declaration in 1 file

this file: opnorm_sum_subexponential

sectionmaximal_inequality

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

lemma expectation_le_ln_mgf source, line 155

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [Z : T -> R] [l B : R],
measurable_fun [set: T] Z ->
(forall x : T, 0 <= Z x) ->
0 < l ->
1 <= ln B ->
(\int[P]_x (expR (l * Z x))%:E <= B%:E)%E -> (\int[P]_x (Z x)%:E <= (ln B / l)%:E)%E

Jensen's inequality for exp, from e^y >= 1 + y: if E e^(l Z) <= B with ln B >= 1, then l E Z <= ln B.

Statement as written in the source

Lemma expectation_le_ln_mgf (P : probability T R) (Z : T -> R) (l B : R) :
  measurable_fun [set: T] Z -> (forall x, 0 <= Z x)%R -> (0 < l)%R ->
  (1 <= ln B)%R ->
  \int[P]_x (expR (l * Z x))%:E <= B%:E ->
  \int[P]_x (Z x)%:E <= (ln B / l)%:E.

Used by 1 declaration in 1 file

this file: subexponential_max_sum

lemma measurable_bigmax_seq source, line 212

forall [d : measure_display] [T : measurableType d] [R : realType] 
  [I : Type] (V : seq I) [F : I -> T -> R],
(forall v : I, measurable_fun [set: T] (F v)) ->
measurable_fun [set: T] (fun x : T => \big[maxr/0]_(v <- V) F v x)

Statement as written in the source

Lemma measurable_bigmax_seq (I : Type) (V : seq I) (F : I -> T -> R) :
  (forall v, measurable_fun [set: T] (F v)) ->
  measurable_fun [set: T] (fun x => \big[Num.max/0%R]_(v <- V) F v x).

Used by 2 declarations in 1 file

this file: subexponential_max_sum, opnorm_sum_subexponential

lemma expR_bigmax_le source, line 221

forall [R : realType] [I : Type] (V : seq I) [l : R] (S : I -> R),
0 <= l ->
expR (l * \big[maxr/0]_(v <- V) `|S v|) <=
1 + \sum_(v <- V) (expR (l * S v) + expR (- (l * S v)))

Statement as written in the source

Lemma expR_bigmax_le (I : Type) (V : seq I) (l : R) (S : I -> R) :
  (0 <= l)%R ->
  (expR (l * \big[Num.max/0%R]_(v <- V) `|S v|) <=
   1 + \sum_(v <- V) (expR (l * S v) + expR (- (l * S v))))%R.

Used by 1 declaration in 1 file

this file: subexponential_max_sum

sectionmaximal_inequality_sum

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

theorem subexponential_max_sum main result source, line 247

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [I : Type] (V : seq I) 
  [g : I -> T -> R] [a : nat -> R] [L : R],
0 < L ->
(forall (v : I) (i : nat), (i < n)%N -> subexponential (mu i) (g v) L) ->
(forall (v : I) (i : nat), (i < n)%N -> \int[mu i]_t g v t = 0) ->
(forall i : nat, (i < n)%N -> `|a i| <= 1) ->
(\int[tuple_prod mu n]_x (\big[maxr/0]_(v <- V) `|\sum_(i < n) a i * g v (tnth x i)|)%:E <=
 (8 * L *
  (Num.ExtraDef.sqrtr (n%:R * (1 + ln (1 + 2 * (size V)%:R))) +
   (1 + ln (1 + 2 * (size V)%:R))))%:E)%E

A maximal inequality for sums of independent centered subexponential variables over a finite family.

Main result, as the README states it

Maximal inequality: for x of law tuple_prod mu n, a family of N functions g_v, each centered and subexponential with constant L under every mu i, and |a_i| <= 1, E max_v |sum_i a_i g_v(x_i)| <= 8 L (sqrt (n Lam) + Lam) with Lam = 1 + ln (1 + 2 N). Proved with the moment generating function of each sum and e^y >= 1 + y.

Statement as written in the source

Theorem subexponential_max_sum (mu : nat -> probability T R) n (I : Type)
    (V : seq I) (g : I -> T -> R) (a : nat -> R) (L : R) : (0 < L)%R ->
  (forall v i, (i < n)%N -> subexponential (mu i) (g v) L) ->
  (forall v i, (i < n)%N -> \int[mu i]_t g v t = 0)%R ->
  (forall i, (i < n)%N -> `|a i| <= 1)%R ->
  \int[tuple_prod mu n]_x
    (\big[Num.max/0]_(v <- V) `|\sum_(i < n) a i * g v (tnth x i)|)%:E <=
  (8 * L * (Num.sqrt (n%:R * (1 + ln (1 + 2 * (size V)%:R))) +
     (1 + ln (1 + 2 * (size V)%:R))))%:E.

Used by 1 declaration in 1 file

this file: opnorm_sum_subexponential

sectionrandom_matrix_sum

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

lemma net_log_le source, line 424

forall [R : realType] [m : nat] [N : R],
0 <= N -> N <= (18 * expR 1) ^+ m -> 1 + ln (1 + 2 * N) <= 6 * m.+1%:R

The logarithm of the number of points of the 1/4-net of the unit ball, as it enters subexponential_max_sum.

Statement as written in the source

Lemma net_log_le m (N : R) : (0 <= N)%R -> (N <= (18 * expR 1) ^+ m)%R ->
  (1 + ln (1 + 2 * N) <= 6 * m.+1%:R)%R.

Used by 1 declaration in 1 file

this file: opnorm_sum_subexponential

theorem opnorm_sum_subexponential main result source, line 456

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n m : nat] [Y : T -> 'M_m] [L : R],
0 < L ->
(forall (v : 'cV_m) (k : nat),
 frobenius v <= 1 -> (k < n)%N -> subexponential (mu k) (fun t : T => mxdot v (Y t *m v)) L) ->
(forall (v : 'cV_m) (k : nat),
 frobenius v <= 1 -> (k < n)%N -> \int[mu k]_t mxdot v (Y t *m v) = 0) ->
exists N : (nat -> R) -> n.-tuple T -> R,
  forall a : nat -> R,
  (forall k : nat, (k < n)%N -> `|a k| <= 1) ->
  [/\ measurable_fun [set: n.-tuple T] (N a),
      forall x : n.-tuple T, opnorm (sym_part (\sum_(k < n) a k *: Y (tnth x k))) <= N a x
    & (\int[tuple_prod mu n]_x (N a x)%:E <=
       (96 * L * (Num.ExtraDef.sqrtr (n%:R * m.+1%:R) + m.+1%:R))%:E)%E]

The operator norm of a weighted sum of independent random matrices whose quadratic forms are centered and subexponential, through a measurable majorant (the operator norm is a supremum over the unit ball), the same for all weights.

Main result, as the README states it

For x of law tuple_prod mu n and Y : T -> 'M[R]_m whose quadratic forms v^T Y v (|v| <= 1) are centered and subexponential with constant L under every mu k, there are measurable N a with opnorm (sym_part (sum_k a_k Y(x_k))) <= N a x and E N a <= 96 L (sqrt (n (m + 1)) + m + 1) for all weights with |a_k| <= 1. Unlike the matrix Bernstein inequality, the bound has no logarithmic factor.

Statement as written in the source

Theorem opnorm_sum_subexponential (mu : nat -> probability T R) n m
    (Y : T -> 'M[R]_m) (L : R) : (0 < L)%R ->
  (forall (v : 'cV[R]_m) k, (frobenius v <= 1)%R -> (k < n)%N ->
     subexponential (mu k) (fun t => mxdot v (Y t *m v)) L) ->
  (forall (v : 'cV[R]_m) k, (frobenius v <= 1)%R -> (k < n)%N ->
     \int[mu k]_t mxdot v (Y t *m v) = 0)%R ->
  exists N : (nat -> R) -> n.-tuple T -> R, forall a : nat -> R,
    (forall k, (k < n)%N -> `|a k| <= 1)%R ->
  [/\ measurable_fun [set: n.-tuple T] (N a),
    (forall x,
      opnorm (sym_part (\sum_(k < n) a k *: Y (tnth x k))) <= N a x)%R &
    \int[tuple_prod mu n]_x (N a x)%:E <=
      (96 * L * (Num.sqrt (n%:R * m.+1%:R) + m.+1%:R))%:E].

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.