GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisprobabilityhanson_wright

The Hanson-Wright inequality

GaussianAnalysis.probability.hanson_wrightlibrary/probability/hanson_wright.v985 lines26 lemmas and theorems, 9 definitionssource
Imports 11 library modules and 26 external

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

Required by 1 files of the paper proofs

Let x have law tuple_prod mu n, so that X_i = f_i (x_i) are independent, centered and subgaussian with constant K (subgaussian.v), and let A be a real n x n matrix. The quadratic form Q = \sum_(i, j) a_ij X_i X_j (hw_quad A) concentrates around hw_center A = \sum_i a_ii E X_i^2, which is its mean (an identity this file does not need): the inequality of Hanson and Wright in the form of Rudelson and Vershynin (Vershynin, High-Dimensional Probability, theorem 6.2.1), with explicit constants. This is item HW of phase 5 (Lemma 3.2 of Koehler and Sohn, arXiv 2608.27372, lines 2157-2185).

  • hanson_wright: for u >= 0, P(|Q - E Q| >= u) <= 2 exp (- min (u^2 / (6912 K^4 |A|_F^2), u / (136 K^2 opnorm A))), with 6912 written 4 * 1728 in the statement; hanson_wright_upper is the one-sided bound.
  • hanson_wright_subexponential: Q - E Q is subexponential with every constant L >= 252 K^2 |A|_F.
  • hanson_wright_mgf: E exp (l (Q - E Q)) <= exp (1728 l^2 K^4 |A|_F^2) when 68 |l| K^2 opnorm A <= 1. Q - E Q is the diagonal part \sum_i a_ii (X_i^2 - E X_i^2) (hw_diag_mgf, Bernstein's inequality, subexponential_sum_mgf) plus the off-diagonal part (hw_quad_split), and exp of their average is at most the average of the exps.
  • hw_offdiag_mgf: E exp (l \sum_(i != j) a_ij X_i X_j) <= exp (432 l^2 K^4 |A|_F^2) when 1152 l^2 K^4 opnorm A ^ 2 <= 1. The off-diagonal sum is 4 / 2^n times the sum over the sets S of the decoupled sums \sum_(i in S, j notin S) (offdiag_decouple, since a quarter of the sets contain i and not j: sum_set_indicator, by the involutions set_toggle), and expR_avg_le is Jensen's inequality for exp and a finite average.
  • hw_decoupled_mgf: E exp (l \sum_(i in S, j notin S) a_ij X_i X_j) <= exp (27 l^2 K^4 |A|_F^2) when 72 l^2 K^4 opnorm A ^ 2 <= 1. Resample the coordinates outside S (ge0_integral_tuple_prod_merge of conditioning.v), apply Hoeffding's inequality to them, write the result as a Gaussian integral (integral_gauss_expR_dot: E exp <g, w> = exp (|w|^2 / 2)), exchange the integrals (fubini_tonelli), apply Hoeffding's inequality to the coordinates in S, and bound the Gaussian chaos for the matrix hw_mask S A, whose norms are at most those of A.
  • gauss_chaos_mgf: for M : 'M_(n, m), 0 <= t and 4 t opnorm M ^ 2 <= 1, E exp (t |g M|^2) <= exp (3 / 2 t |M|_F^2): g M has the law of h B with B = diag (sqrt d) P for the spectral decomposition M^T M = P^T diag d P (ge0_integral_gauss_mulmx), and |h B|^2 is a weighted chi-square.
  • subexponential_of_mgf: if E exp (l Y) <= exp (l^2 s^2) for |l| b <= 1, then Y is subexponential with every constant L >= 3 max (2 s, b).

Main results

ResultsStatement
hanson_wrighthanson_wright_subexponentialhanson_wright_mgf
The Hanson-Wright inequality: for x of law tuple_prod mu n with X_i = f_i (x_i) centered and subgaussian with constant K, and A a real n x n matrix, Q = \sum_(i, j) a_ij X_i X_j satisfies P(|Q - E Q| >= u) <= 2 exp (- min (u^2 / (6912 K^4 |A|_F^2), u / (136 K^2 opnorm A))), and Q - E Q is subexponential with constant 252 K^2 |A|_F; E Q is written \sum_i a_ii E X_i^2 (hw_center). Proved by decoupling over the sets S of coordinates, Hoeffding's inequality twice and a Gaussian chaos bound, and Bernstein's inequality for the diagonal.
gauss_chaos_mgfintegral_gauss_expR_dotsubexponential_of_mgfoffdiag_decouple
For g of law gauss n: E exp <g, w> = exp (|w|^2 / 2), and E exp (t |g M|^2) <= exp (3/2 t |M|_F^2) when 4 t opnorm M ^ 2 <= 1. A bound E exp (l Y) <= exp (l^2 s^2) for |l| b <= 1 makes Y subexponential with constant 3 max (2 s, b). The off-diagonal sum \sum_(i != j) c_ij is 4 / 2^n times the sum over the sets S of \sum_(i in S, j notin S) c_ij.

Declarations35 exported, 8 local

lemma, theoremdefinitioninstancelocal
sectiongauss_mgf
Context {R : realType}.
lemma integral_gauss_expR_dot main result source, line 74 
forall {R : realType} [n : nat] (w : 'rV_n),
(\int[gauss n]_g (expR (mxdot g w))%:E)%E = (expR (mxdot w w / 2))%:E

The moment generating function of the standard Gaussian vector.

Main result

Stated in the README together with gauss_chaos_mgf.

Statement as written in the source
Lemma integral_gauss_expR_dot n (w : 'rV[R]_n) :
  (\int[gauss n]_g (expR (mxdot g w))%:E = (expR (mxdot w w / 2))%:E)%E.
Used by 1 declaration in 1 file
lemma gauss_chaos_mgf main result source, line 92 
forall {R : realType} [n m : nat] [M : 'M_(n, m)] [t : R],
0 <= t ->
4 * t * opnorm M ^+ 2 <= 1 ->
(\int[gauss n]_g (expR (t * mxdot (g *m M) (g *m M)))%:E <=
 (expR (3 / 2 * t * mxdot M M))%:E)%E

A Gaussian chaos: |g M|^2 for g of law gauss n.

Main result, as the README states it

For g of law gauss n: E exp <g, w> = exp (|w|^2 / 2), and E exp (t |g M|^2) <= exp (3/2 t |M|_F^2) when 4 t opnorm M ^ 2 <= 1. A bound E exp (l Y) <= exp (l^2 s^2) for |l| b <= 1 makes Y subexponential with constant 3 max (2 s, b). The off-diagonal sum \sum_(i != j) c_ij is 4 / 2^n times the sum over the sets S of \sum_(i in S, j notin S) c_ij.

Statement as written in the source
Lemma gauss_chaos_mgf n m (M : 'M[R]_(n, m)) (t : R) :
  0 <= t -> 4 * t * opnorm M ^+ 2 <= 1 ->
  (\int[gauss n]_g (expR (t * mxdot (g *m M) (g *m M)))%:E <=
   (expR (3 / 2 * t * mxdot M M))%:E)%E.
Used by 1 declaration in 1 file
sectiondecoupling
Context {R : realType} (n : nat).
Implicit Types (S : {set 'I_n}) (i j k l : 'I_n).
definition set_toggle source, line 166
Type
forall [n : nat], 'I_n -> {set 'I_n} -> {set 'I_n}
Definition
Definition set_toggle k S : {set 'I_n} := if k \in S then S :\ k else k |: S.

Remove k from S if it is there, add it otherwise.

Used by 2 declarations in 1 file
lemma set_toggleK source, line 168 
forall [n : nat] (k : 'I_n), involutive (set_toggle k)
Statement as written in the source
Lemma set_toggleK k : involutive (set_toggle k).
Used by 1 declaration in 1 file
lemma in_set_toggle source, line 175 
forall [n : nat] (k l : 'I_n) (S : {set 'I_n}),
(l \in set_toggle k S) = (if l == k then k \notin S else l \in S)
Statement as written in the source
Lemma in_set_toggle k l S :
  (l \in set_toggle k S) = (if l == k then k \notin S else l \in S).
Used by 1 declaration in 1 file
lemma card_set_ord source, line 185 
forall n : nat, #|{set 'I_n}| = 2 ^ n
Statement as written in the source
Lemma card_set_ord : #|{set 'I_n}| = 2 ^ n.
Used by 2 declarations in 1 file
lemma sum_set_indicator source, line 189 
forall {R : realType} [n : nat] [i j : 'I_n],
i != j -> \sum_S ((i \in S) && (j \notin S))%:R = (2 ^ n)%:R / 4

For i != j, a quarter of the sets contain i and not j.

Statement as written in the source
Lemma sum_set_indicator i j : i != j ->
  \sum_(S : {set 'I_n}) ((i \in S) && (j \notin S))%:R = (2 ^ n)%:R / 4 :> R.
Used by 1 declaration in 1 file
lemma offdiag_decouple main result source, line 221 
forall {R : realType} [n : nat] (c : 'I_n -> 'I_n -> R),
\sum_i \sum_j (i != j)%:R * c i j =
4 / (2 ^ n)%:R * \sum_S \sum_i \sum_j ((i \in S) && (j \notin S))%:R * c i j

The off-diagonal sum as an average over the sets S of the sums over i in S and j notin S.

Main result

Stated in the README together with gauss_chaos_mgf.

Statement as written in the source
Lemma offdiag_decouple (c : 'I_n -> 'I_n -> R) :
  \sum_i \sum_j (i != j)%:R * c i j =
  4 / (2 ^ n)%:R * \sum_(S : {set 'I_n})
    \sum_i \sum_j ((i \in S) && (j \notin S))%:R * c i j.
Used by 1 declaration in 1 file
sectionexpR_avg
Context {R : realType}.
lemma expR_avg_le source, line 247 
forall {R : realType} [I : finType] (y : I -> R),
(0 < #|I|)%N -> expR (#|I|%:R^-1 * \sum_k y k) <= #|I|%:R^-1 * \sum_k expR (y k)

Jensen's inequality for exp and a finite average.

Statement as written in the source
Lemma expR_avg_le (I : finType) (y : I -> R) : (0 < #|I|)%N ->
  expR (#|I|%:R^-1 * \sum_k y k) <= #|I|%:R^-1 * \sum_k expR (y k).
Used by 1 declaration in 1 file
sectionintegral_avg
Context d (T : measurableType d) (R : realType).
Variable mu : {measure set T -> \bar R}.
lemma ge0_integral_avg source, line 270 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [mu : measure T R] [I : finType] [g : I -> T -> R] [B : R],
(0 < #|I|)%N ->
(forall k : I, measurable_fun [set: T] (g k)) ->
(forall (k : I) (x : T), 0 <= g k x) ->
(forall k : I, (\int[mu]_x (g k x)%:E <= B%:E)%E) ->
(\int[mu]_x (#|I|%:R^-1 * \sum_k g k x)%:E <= B%:E)%E

If each g k has integral at most B, so has their average.

Statement as written in the source
Lemma ge0_integral_avg (I : finType) (g : I -> T -> R) (B : R) :
  (0 < #|I|)%N -> (forall k, measurable_fun [set: T] (g k)) ->
  (forall k x, 0 <= g k x) ->
  (forall k, \int[mu]_x (g k x)%:E <= B%:E)%E ->
  (\int[mu]_x (#|I|%:R^-1 * \sum_k g k x)%:E <= B%:E)%E.
Used by 3 declarations in 1 file
sectionsubexponential_of_mgf
Context d (T : measurableType d) (R : realType) (P : probability T R).
lemma subexponential_of_mgf main result source, line 301 
forall [d : measure_display] [T : measurableType d] [R : realType] 
  [P : probability T R] [Y : T -> R] [s b L : R],
measurable_fun [set: T] Y ->
0 <= s ->
0 < b ->
(forall l : join_Num_NumDomain_between_GRing_PzSemiRing_and_Num_SemiNormedZmodule R,
 `|l| * b <= 1 -> (\int[P]_x (expR (l * Y x))%:E <= (expR (l ^+ 2 * s ^+ 2))%:E)%E) ->
3 * Num.max (2 * s) b <= L -> subexponential P Y L

A bound on the moment generating function near 0 gives a subexponential constant: if E exp (l Y) <= exp (l^2 s^2) for |l| b <= 1, then Y is subexponential with every constant L >= 3 max (2 s, b).

Main result

Stated in the README together with gauss_chaos_mgf.

Statement as written in the source
Lemma subexponential_of_mgf (Y : T -> R) (s b L : R) :
  measurable_fun [set: T] Y -> 0 <= s -> 0 < b ->
  (forall l, `|l| * b <= 1 ->
     (\int[P]_x (expR (l * Y x))%:E <= (expR (l ^+ 2 * s ^+ 2))%:E)%E) ->
  3 * Num.max (2 * s) b <= L -> subexponential P Y L.
Used by 1 declaration in 1 file
sectionhanson_wright
Context d (T : measurableType d) (R : realType).
Variables (mu : nat -> probability T R) (n : nat) (f : nat -> T -> R) (K : R).
Hypothesis sf : forall i, (i < n)%N -> subgaussian (mu i) (f i) K.
Hypothesis f0 : forall i, (i < n)%N -> (\int[mu i]_t f i t = 0)%R.
Local Notation P := (tuple_prod mu n).
Local Notation X x i := (f (nat_of_ord i) (tnth x i)).
let mX section-local source, line 392 
Let mX (i : 'I_n) : measurable_fun [set: n.-tuple T] (fun x => X x i).
definition hw_decoupled source, line 399
Type
forall [d : measure_display] [T : measurableType d] [R : realType] [n : nat],
(nat -> T -> R) -> {set 'I_n} -> 'M_n -> n.-tuple T -> R
Definition
Definition hw_decoupled (S : {set 'I_n}) (A : 'M[R]_n) (x : n.-tuple T) : R :=
  \sum_i \sum_j ((i \in S) && (j \notin S))%:R * (A i j * (X x i * X x j)).

The decoupled form \sum_(i in S, j notin S) a_ij X_i X_j.

Used by 3 declarations in 1 file
definition ord_ext source, line 403
Type
forall [R : realType] [n : nat], ('I_n -> R) -> nat -> R
Definition
Definition ord_ext (c : 'I_n -> R) (k : nat) : R :=
  if insub k is Some i then c i else 0.

A function of the ordinals as a function of the integers.

Used by 3 declarations in 1 file
lemma ord_extE source, line 406 
forall [R : realType] [n : nat] (c : 'I_n -> R) (i : 'I_n), ord_ext c i = c i
Statement as written in the source
Lemma ord_extE (c : 'I_n -> R) (i : 'I_n) : ord_ext c i = c i.
Used by 2 declarations in 1 file
let hoeffding section-local source, line 410 
Let hoeffding (c : 'I_n -> R) (l : R) :
  (\int[P]_x (expR (l * \sum_i c i * X x i))%:E <=
   (expR (3 * l ^+ 2 * \sum_i c i ^+ 2 * K ^+ 2))%:E)%E.

Hoeffding's inequality for coefficients indexed by 'I_n.

Used by 1 declaration in 1 file
definition hw_mask source, line 421
Type
forall [R : realType] [n : nat], {set 'I_n} -> 'M_n -> 'M_n
Definition
Definition hw_mask (S : {set 'I_n}) (A : 'M[R]_n) : 'M[R]_n :=
  \matrix_(j, i) (((i \in S) && (j \notin S))%:R * A i j).

The matrix of the decoupled form: (g M)_i = \sum_(j notin S) g_j a_ij for i in S, 0 otherwise.

Used by 4 declarations in 1 file
lemma hw_mask_diag source, line 424 
forall [R : realType] [n : nat] (S0 : {set 'I_n}) (A : 'M_n),
hw_mask S0 A = diag_mx (\row_j (j \notin S0)%:R) *m A^T *m diag_mx (\row_i (i \in S0)%:R)
Statement as written in the source
Lemma hw_mask_diag (S : {set 'I_n}) (A : 'M[R]_n) :
  hw_mask S A = diag_mx (\row_j (j \notin S)%:R) *m A^T *m
    diag_mx (\row_i (i \in S)%:R).
Used by 1 declaration in 1 file
lemma opnorm_diag01 source, line 432 
forall [R : realType] [n : nat] [v : 'rV_n],
(forall i : 'I_n, v 0 i = 0 \/ v 0 i = 1) -> opnorm (diag_mx v) <= 1
Statement as written in the source
Lemma opnorm_diag01 (v : 'rV[R]_n) : (forall i, v 0 i = 0 \/ v 0 i = 1) ->
  opnorm (diag_mx v) <= 1.
Used by 1 declaration in 1 file
lemma opnorm_hw_mask source, line 442 
forall [R : realType] [n : nat] (S : {set 'I_n}) (A : 'M_n),
opnorm (hw_mask S A) <= opnorm A
Statement as written in the source
Lemma opnorm_hw_mask (S : {set 'I_n}) (A : 'M[R]_n) :
  opnorm (hw_mask S A) <= opnorm A.
Used by 1 declaration in 1 file
lemma mxdot_hw_mask source, line 455 
forall [R : realType] [n : nat] (S : {set 'I_n}) (A : 'M_n),
mxdot (hw_mask S A) (hw_mask S A) <= mxdot A A
Statement as written in the source
Lemma mxdot_hw_mask (S : {set 'I_n}) (A : 'M[R]_n) :
  mxdot (hw_mask S A) (hw_mask S A) <= mxdot A A.
Used by 1 declaration in 1 file
theorem hw_decoupled_mgf source, line 467 
forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [K : R],
(forall i : nat, (i < n)%N -> subgaussian (mu i) (f i) K) ->
(forall i : nat, (i < n)%N -> \int[mu i]_t f i t = 0) ->
forall (S0 : {set 'I_n}) [A : 'M_n] [l : R],
72 * l ^+ 2 * K ^+ 4 * opnorm A ^+ 2 <= 1 ->
(\int[tuple_prod mu n]_x (expR (l * hw_decoupled f S0 A x))%:E <=
 (expR (27 * l ^+ 2 * K ^+ 4 * mxdot A A))%:E)%E

The moment generating function of the decoupled form: resample the coordinates outside S, apply Hoeffding's inequality to them, write the result as a Gaussian integral, exchange the integrals, apply Hoeffding's inequality to the coordinates in S and bound the Gaussian chaos.

Statement as written in the source
Theorem hw_decoupled_mgf (S : {set 'I_n}) (A : 'M[R]_n) (l : R) :
  72 * l ^+ 2 * K ^+ 4 * opnorm A ^+ 2 <= 1 ->
  (\int[P]_x (expR (l * hw_decoupled S A x))%:E <=
   (expR (27 * l ^+ 2 * K ^+ 4 * mxdot A A))%:E)%E.
Used by 1 declaration in 1 file
definition hw_offdiag source, line 583
Type
forall [d : measure_display] [T : measurableType d] [R : realType] [n : nat],
(nat -> T -> R) -> 'M_n -> n.-tuple T -> R
Definition
Definition hw_offdiag (A : 'M[R]_n) (x : n.-tuple T) : R :=
  \sum_i \sum_j (i != j)%:R * (A i j * (X x i * X x j)).

The off-diagonal part \sum_(i != j) a_ij X_i X_j.

Used by 4 declarations in 1 file
let mdec section-local source, line 586 
Let mdec (S : {set 'I_n}) (A : 'M[R]_n) :
  measurable_fun [set: n.-tuple T] (hw_decoupled S A).
let moff section-local source, line 594 
Let moff (A : 'M[R]_n) : measurable_fun [set: n.-tuple T] (hw_offdiag A).
Used by 1 declaration in 1 file
theorem hw_offdiag_mgf source, line 602 
forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [K : R],
(forall i : nat, (i < n)%N -> subgaussian (mu i) (f i) K) ->
(forall i : nat, (i < n)%N -> \int[mu i]_t f i t = 0) ->
forall [A : 'M_n] [l : R],
1152 * l ^+ 2 * K ^+ 4 * opnorm A ^+ 2 <= 1 ->
(\int[tuple_prod mu n]_x (expR (l * hw_offdiag f A x))%:E <=
 (expR (432 * l ^+ 2 * K ^+ 4 * mxdot A A))%:E)%E

Decoupling: average the decoupled forms over the sets S.

Statement as written in the source
Theorem hw_offdiag_mgf (A : 'M[R]_n) (l : R) :
  1152 * l ^+ 2 * K ^+ 4 * opnorm A ^+ 2 <= 1 ->
  (\int[P]_x (expR (l * hw_offdiag A x))%:E <=
   (expR (432 * l ^+ 2 * K ^+ 4 * mxdot A A))%:E)%E.
Used by 1 declaration in 1 file
lemma entry_le_opnorm source, line 638 
forall [R : realType] [n : nat] (A : 'M_n) (i j : 'I_n), `|A i j| <= opnorm A
Statement as written in the source
Lemma entry_le_opnorm (A : 'M[R]_n) i j : `|A i j| <= opnorm A.
Used by 2 declarations in 1 file
definition hw_sqmean source, line 647
Type
forall [d : measure_display] [T : measurableType d] [R : realType],
(nat -> probability T R) -> (nat -> T -> R) -> nat -> R
Definition
Definition hw_sqmean (i : nat) : R := \int[mu i]_t f i t ^+ 2.

The second moments E X_i^2 and the diagonal part \sum_i a_ii (X_i^2 - E X_i^2).

Used by 5 declarations in 1 file
definition hw_diag source, line 649
Type
forall [d : measure_display] [T : measurableType d] [R : realType],
(nat -> probability T R) -> forall [n : nat], (nat -> T -> R) -> 'M_n -> n.-tuple T -> R
Definition
Definition hw_diag (A : 'M[R]_n) (x : n.-tuple T) : R :=
  \sum_i A i i * (X x i ^+ 2 - hw_sqmean i).
Used by 4 declarations in 1 file
let sub_center section-local source, line 652 
Let sub_center (i : nat) : (i < n)%N ->
  subexponential (mu i) (fun t => f i t ^+ 2 - hw_sqmean i) (3 * K ^+ 2).
Used by 1 declaration in 1 file
let center0 section-local source, line 658 
Let center0 (i : nat) : (i < n)%N ->
  \int[mu i]_t (f i t ^+ 2 - hw_sqmean i) = 0.
Used by 1 declaration in 1 file
theorem hw_diag_mgf source, line 668 
forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [K : R],
(forall i : nat, (i < n)%N -> subgaussian (mu i) (f i) K) ->
forall [A : 'M_n] [l : R],
6 * `|l| * K ^+ 2 * opnorm A <= 1 ->
(\int[tuple_prod mu n]_x (expR (l * hw_diag mu f A x))%:E <=
 (expR (144 * l ^+ 2 * K ^+ 4 * mxdot A A))%:E)%E

Bernstein's inequality for the diagonal part.

Statement as written in the source
Theorem hw_diag_mgf (A : 'M[R]_n) (l : R) :
  6 * `|l| * K ^+ 2 * opnorm A <= 1 ->
  (\int[P]_x (expR (l * hw_diag A x))%:E <=
   (expR (144 * l ^+ 2 * K ^+ 4 * mxdot A A))%:E)%E.
Used by 1 declaration in 1 file
definition hw_quad source, line 703
Type
forall [d : measure_display] [T : measurableType d] [R : realType] [n : nat],
(nat -> T -> R) -> 'M_n -> n.-tuple T -> R
Definition
Definition hw_quad (A : 'M[R]_n) (x : n.-tuple T) : R :=
  \sum_i \sum_j A i j * (X x i * X x j).

The quadratic form Q = \sum_(i, j) a_ij X_i X_j and the constant \sum_i a_ii E X_i^2, which is its mean.

Used by 8 declarations in 1 file
definition hw_center source, line 706
Type
forall [d : measure_display] [T : measurableType d] [R : realType],
(nat -> probability T R) -> forall [n : nat], (nat -> T -> R) -> 'M_n -> R
Definition
Definition hw_center (A : 'M[R]_n) : R := \sum_i A i i * hw_sqmean i.
Used by 7 declarations in 1 file
lemma hw_quad_split source, line 708 
forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] (f : nat -> T -> R) (A : 'M_n) 
  (x : n.-tuple T),
hw_quad f A x - hw_center mu f A = hw_diag mu f A x + hw_offdiag f A x
Statement as written in the source
Lemma hw_quad_split (A : 'M[R]_n) (x : n.-tuple T) :
  hw_quad A x - hw_center A = hw_diag A x + hw_offdiag A x.
Used by 1 declaration in 1 file
let mquad section-local source, line 726 
Let mquad (A : 'M[R]_n) : measurable_fun [set: n.-tuple T] (hw_quad A).
Used by 3 declarations in 1 file
let mdiag section-local source, line 732 
Let mdiag (A : 'M[R]_n) : measurable_fun [set: n.-tuple T] (hw_diag A).
Used by 1 declaration in 1 file
theorem hanson_wright_mgf main result source, line 739 
forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [K : R],
(forall i : nat, (i < n)%N -> subgaussian (mu i) (f i) K) ->
(forall i : nat, (i < n)%N -> \int[mu i]_t f i t = 0) ->
forall [A : 'M_n] [l : R],
68 * `|l| * K ^+ 2 * opnorm A <= 1 ->
(\int[tuple_prod mu n]_x (expR (l * (hw_quad f A x - hw_center mu f A)))%:E <=
 (expR (1728 * l ^+ 2 * K ^+ 4 * mxdot A A))%:E)%E

The moment generating function of Q - E Q.

Main result

Stated in the README together with hanson_wright.

Statement as written in the source
Theorem hanson_wright_mgf (A : 'M[R]_n) (l : R) :
  68 * `|l| * K ^+ 2 * opnorm A <= 1 ->
  (\int[P]_x (expR (l * (hw_quad A x - hw_center A)))%:E <=
   (expR (1728 * l ^+ 2 * K ^+ 4 * mxdot A A))%:E)%E.
Used by 2 declarations in 1 file
lemma hw_quad0 source, line 799 
forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] (f : nat -> T -> R) (x : n.-tuple T),
hw_quad f 0 x - hw_center mu f 0 = 0
Statement as written in the source
Lemma hw_quad0 (x : n.-tuple T) : hw_quad 0 x - hw_center 0 = 0.
Used by 1 declaration in 1 file
theorem hanson_wright_subexponential main result source, line 811 
forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [K : R],
(forall i : nat, (i < n)%N -> subgaussian (mu i) (f i) K) ->
(forall i : nat, (i < n)%N -> \int[mu i]_t f i t = 0) ->
forall [A : 'M_n] [L : R],
0 < L ->
252 * K ^+ 2 * frobenius A <= L ->
subexponential (tuple_prod mu n) (fun x : n.-tuple T => hw_quad f A x - hw_center mu f A) L

Hanson-Wright, subexponential form: Q - E Q is subexponential with constant 252 K^2 |A|_F.

Main result

Stated in the README together with hanson_wright.

Statement as written in the source
Theorem hanson_wright_subexponential (A : 'M[R]_n) (L : R) :
  0 < L -> 252 * K ^+ 2 * frobenius A <= L ->
  subexponential P (fun x => hw_quad A x - hw_center A) L.
theorem hanson_wright_upper source, line 858 
forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [K : R],
(forall i : nat, (i < n)%N -> subgaussian (mu i) (f i) K) ->
(forall i : nat, (i < n)%N -> \int[mu i]_t f i t = 0) ->
forall (A : 'M_n) [u : R],
0 <= u ->
(tuple_prod mu n [set x | (u <= hw_quad f A x - hw_center mu f A)%R] <=
 (expR
    (- Num.min (u ^+ 2 / (4 * 1728 * K ^+ 4 * mxdot A A)) (u / (136 * K ^+ 2 * opnorm A))))%:E)%E

Hanson-Wright, upper tail: P(Q - E Q >= u) <= exp (- min (u^2 / (6912 K^4 |A|_F^2), u / (136 K^2 opnorm A))).

Statement as written in the source
Theorem hanson_wright_upper (A : 'M[R]_n) (u : R) : 0 <= u ->
  (P [set x | (u <= hw_quad A x - hw_center A)%R] <=
   (expR (- Num.min (u ^+ 2 / (4 * 1728 * K ^+ 4 * mxdot A A))
                    (u / (136 * K ^+ 2 * opnorm A))))%:E)%E.
Used by 1 declaration in 1 file
lemma hw_quadN source, line 934 
forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] (f : nat -> T -> R) (A : 'M_n) 
  (x : n.-tuple T),
hw_quad f (- A) x - hw_center mu f (- A) = - (hw_quad f A x - hw_center mu f A)
Statement as written in the source
Lemma hw_quadN (A : 'M[R]_n) (x : n.-tuple T) :
  hw_quad (- A) x - hw_center (- A) = - (hw_quad A x - hw_center A).
Used by 1 declaration in 1 file
theorem hanson_wright main result source, line 947 
forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [f : nat -> T -> R] [K : R],
(forall i : nat, (i < n)%N -> subgaussian (mu i) (f i) K) ->
(forall i : nat, (i < n)%N -> \int[mu i]_t f i t = 0) ->
forall (A : 'M_n) [u : R],
0 <= u ->
(tuple_prod mu n [set x | (u <= `|hw_quad f A x - hw_center mu f A|)%R] <=
 (2 *
  expR
    (- Num.min (u ^+ 2 / (4 * 1728 * K ^+ 4 * mxdot A A)) (u / (136 * K ^+ 2 * opnorm A))))%:E)%E

The Hanson-Wright inequality: P(|Q - E Q| >= u) <= 2 exp (- min (u^2 / (6912 K^4 |A|_F^2), u / (136 K^2 opnorm A))).

Main result, as the README states it

The Hanson-Wright inequality: for x of law tuple_prod mu n with X_i = f_i (x_i) centered and subgaussian with constant K, and A a real n x n matrix, Q = \sum_(i, j) a_ij X_i X_j satisfies P(|Q - E Q| >= u) <= 2 exp (- min (u^2 / (6912 K^4 |A|_F^2), u / (136 K^2 opnorm A))), and Q - E Q is subexponential with constant 252 K^2 |A|_F; E Q is written \sum_i a_ii E X_i^2 (hw_center). Proved by decoupling over the sets S of coordinates, Hoeffding's inequality twice and a Gaussian chaos bound, and Bernstein's inequality for the diagonal.

Statement as written in the source
Theorem hanson_wright (A : 'M[R]_n) (u : R) : 0 <= u ->
  (P [set x | (u <= `|hw_quad A x - hw_center A|)%R] <=
   (2 * expR (- Num.min (u ^+ 2 / (4 * 1728 * K ^+ 4 * mxdot A A))
                        (u / (136 * K ^+ 2 * opnorm A))))%:E)%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.