On this page
Exponential moments and tails of chi-square variables
Imports 5 library modules and 27 external
- GaussianAnalysis.gaussian.measurable_matrix
- GaussianAnalysis.gaussian.normal_integral
- GaussianAnalysis.gaussian.gauss
- GaussianAnalysis.matrix.euclidean
- GaussianAnalysis.comparison.normal_mgf
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.measure_theory.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 3
Required by 4 files of the paper proofs
For X of law normal_prob 0 s and 2 t s^2 < 1, E[expR (t X^2)] = 1 / sqrt (1 - 2 t s^2) (integral_normal_expR_sqr). For the standard normal law, E[expR (t (X^2 - 1))] = expR (- t) / sqrt (1 - 2 t), which is at most expR (t^2 / (1 - 2 |t|)) when |2 t| < 1 (integral_normal_expR_sqrB1_le), by the inequality - ln (1 - u) - u <= u^2 / (2 (1 - |u|)) for |u| < 1 (ln_subgamma).
For x of law gauss n and a row vector of weights a, centered_chi2 a x is a centered weighted chi-square variable. Its moment generating function is the product of the one-dimensional ones (integral_gauss_expR_centered_chi2) and is sub-gamma: if |a_i| <= L for every i, then E[expR (t centered_chi2 a x)] <= expR (t^2 |a|^2 / (1 - 2 |t| L)) when 2 |t| L < 1 (integral_gauss_expR_centered_chi2_le). It follows that P(|centered_chi2 a x| >= u) <= 2 expR (- u^2 / (4 (|a|^2 + L u))) for u > 0 (gauss_centered_chi2_abs_tail), with one-sided versions.
centered_ | \sum_i a_i (x_i^2 - 1), for a x : 'rV[R]_n |
Main results
| Results | Statement | Used by theories/ |
|---|---|---|
For X of law normal_prob 0 s and 2 t s^2 < 1, E[expR (t X^2)] = 1 / sqrt (1 - 2 t s^2); for the standard law, E[expR (t (X^2 - 1))] = expR (- t) / sqrt (1 - 2 t). | Gaussian/, for Gaussian/ | |
- ln (1 - u) - u <= u^2 / (2 (1 - |u|)) for |u| < 1; hence E[expR (t (X^2 - 1))] <= expR (t^2 / (1 - 2 |t|)) for the standard normal law and |2 t| < 1. | ||
For x of law gauss n and weights a with |a_i| <= L, Q = sum_i a_i (x_i^2 - 1) satisfies E[expR (t Q)] <= expR (t^2 |a|^2 / (1 - 2 |t| L)) when 2 |t| L < 1, and P(|Q| >= u) <= 2 expR (- u^2 / (4 (|a|^2 + L u))) for u > 0. | Gaussian/ |
Declarations17 exported
Context {R : realType}. Implicit Types s t u x : R.
forall {R : realType} [s t : R] (x : R), s != 0 -> 2 * t * s ^+ 2 < 1 -> expR (t * x ^+ 2) * normal_pdf 0 s x = (Num.ExtraDef.sqrtr (1 - 2 * t * s ^+ 2))^-1 * normal_pdf 0 (s / Num.ExtraDef.sqrtr (1 - 2 * t * s ^+ 2)) x
Statement as written in the source
Lemma normal_pdf_expR_sqr s t x : s != 0 -> 2 * t * s ^+ 2 < 1 -> expR (t * x ^+ 2) * normal_pdf 0 s x = (Num.sqrt (1 - 2 * t * s ^+ 2))^-1 * normal_pdf 0 (s / Num.sqrt (1 - 2 * t * s ^+ 2)) x.
Used by 1 declaration in 1 file
- this file: integral_normal_expR_sqr
forall {R : realType} (t : R), measurable_fun [set: R] (fun x : R => expR (t * x ^+ 2))
Statement as written in the source
Lemma measurable_expR_sqr t : measurable_fun [set: R] (fun x : R => expR (t * x ^+ 2)).
Used by 3 declarations in 1 file
forall {R : realType} [s t : R], s != 0 -> 2 * t * s ^+ 2 < 1 -> (\int[normal_prob 0 s]_x (expR (t * x ^+ 2))%:E)%E = ((Num.ExtraDef.sqrtr (1 - 2 * t * s ^+ 2))^-1)%:E
For X of law normal_prob 0 s and 2 t s^2 < 1, E[expR (t X^2)] = 1 / sqrt (1 - 2 t s^2); for the standard law, E[expR (t (X^2 - 1))] = expR (- t) / sqrt (1 - 2 t).
Statement as written in the source
Lemma integral_normal_expR_sqr s t : s != 0 -> 2 * t * s ^+ 2 < 1 -> (\int[normal_prob 0 s]_x (expR (t * x ^+ 2))%:E = ((Num.sqrt (1 - 2 * t * s ^+ 2))^-1)%:E)%E.
Used by 3 declarations in 2 files
- GaussianAnalysis.probability.subgaussian: subgaussian_of_mgf
- this file: integrable_normal_expR_sqr, integral_normal_expR_sqrB1
forall {R : realType} [s t : R], s != 0 -> 2 * t * s ^+ 2 < 1 -> (normal_prob 0 s).-integrable [set: g_sigma_algebraType (R.-ocitv).-measurable] (fun x : R => (expR (t * x ^+ 2))%:E)
Statement as written in the source
Lemma integrable_normal_expR_sqr s t : s != 0 -> 2 * t * s ^+ 2 < 1 -> (normal_prob 0 s).-integrable setT (fun x => (expR (t * x ^+ 2))%:E).
forall {R : realType} [t : R], 2 * t < 1 -> (\int[normal_prob 0 1]_x (expR (t * (x ^+ 2 - 1)))%:E)%E = (expR (- t) / Num.ExtraDef.sqrtr (1 - 2 * t))%:E
Stated in the README together with integral_normal_expR_sqr.
Statement as written in the source
Lemma integral_normal_expR_sqrB1 t : 2 * t < 1 -> (\int[normal_prob 0 1]_x (expR (t * (x ^+ 2 - 1)))%:E = (expR (- t) / Num.sqrt (1 - 2 * t))%:E)%E.
Used by 3 declarations in 1 file
Context {R : realType}. Implicit Types t u y : R.
forall {R : realType} [y : R], 0 < y <= 1 -> (y - y^-1) / 2 <= ln y
Statement as written in the source
Lemma ln_ge_half_sub_inv y : 0 < y <= 1 -> (y - y^-1) / 2 <= ln y.
Used by 1 declaration in 1 file
- this file: ln_subgamma
forall {R : realType} [y : R], 1 <= y -> y - 1 - (y - 1) ^+ 2 / 2 <= ln y
Statement as written in the source
Lemma ln_ge_sub_half_sqr y : 1 <= y -> (y - 1) - (y - 1) ^+ 2 / 2 <= ln y.
Used by 1 declaration in 1 file
- this file: ln_subgamma
forall {R : realType} [u : R], `|u| < 1 -> - ln (1 - u) - u <= u ^+ 2 / (2 * (1 - `|u|))
- ln (1 - u) - u <= u^2 / (2 (1 - |u|)) for |u| < 1; hence E[expR (t (X^2 - 1))] <= expR (t^2 / (1 - 2 |t|)) for the standard normal law and |2 t| < 1.
Statement as written in the source
Lemma ln_subgamma u : `|u| < 1 -> - ln (1 - u) - u <= u ^+ 2 / (2 * (1 - `|u|)).
Used by 1 declaration in 1 file
- this file: integral_normal_expR_sqrB1_le
Context {R : realType}. Implicit Types t : R.
forall {R : realType} [t : R], `|2 * t| < 1 -> (\int[normal_prob 0 1]_x (expR (t * (x ^+ 2 - 1)))%:E <= (expR (t ^+ 2 / (1 - 2 * `|t|)))%:E)%E
Stated in the README together with ln_subgamma.
Statement as written in the source
Lemma integral_normal_expR_sqrB1_le t : `|2 * t| < 1 -> (\int[normal_prob 0 1]_x (expR (t * (x ^+ 2 - 1)))%:E <= (expR (t ^+ 2 / (1 - 2 * `|t|)))%:E)%E.
Used by 1 declaration in 1 file
- this file: integral_gauss_expR_centered_chi2_le
Context {R : realType}. Local Notation N := (@normal_prob R 0 1). Implicit Types (t u L : R).
forall {R : realType} [n : nat], 'rV_n -> 'rV_n -> RDefinition centered_chi2 n (a x : 'rV[R]_n) : R := \sum_i a 0 i * (x 0 i ^+ 2 - 1).
Used by 9 declarations in 3 files
- GaussianAnalysis.probability.hanson_wright: gauss_chaos_mgf
- GaussianAnalysis.random_matrix.goe_entries: goe_mx_row_tail
- this file: measurable_centered_chi2, integral_gauss_expR_centered_chi2, integral_gauss_expR_centered_chi2_le, gauss_centered_chi2_upper_tail, centered_chi2N, gauss_centered_chi2_lower_tail, gauss_centered_chi2_abs_tail
forall {R : realType} [n : nat] (a : 'rV_n), measurable_fun [set: 'rV_n] (centered_chi2 a)
Statement as written in the source
Lemma measurable_centered_chi2 n (a : 'rV[R]_n) : measurable_fun [set: 'rV[R]_n] (centered_chi2 a).
Used by 4 declarations in 3 files
- GaussianAnalysis.probability.hanson_wright: gauss_chaos_mgf
- GaussianAnalysis.random_matrix.goe_entries: goe_mx_row_tail
- this file: gauss_centered_chi2_upper_tail, gauss_centered_chi2_abs_tail
forall {R : realType} [n : nat] [a : 'rV_n] [t : R], (forall i : 'I_n, 2 * (t * a 0 i) < 1) -> (\int[gauss n]_x (expR (t * centered_chi2 a x))%:E)%E = (\prod_i (expR (- (t * a 0 i)) / Num.ExtraDef.sqrtr (1 - 2 * (t * a 0 i))))%:E
Statement as written in the source
Lemma integral_gauss_expR_centered_chi2 n (a : 'rV[R]_n) t : (forall i, 2 * (t * a 0 i) < 1) -> (\int[gauss n]_x (expR (t * centered_chi2 a x))%:E = (\prod_i (expR (- (t * a 0 i)) / Num.sqrt (1 - 2 * (t * a 0 i))))%:E)%E.
Used by 1 declaration in 1 file
- this file: integral_gauss_expR_centered_chi2_le
forall {R : realType} [n : nat] [a : 'rV_n] [t L : R], (forall i : 'I_n, `|a 0 i| <= L) -> `|2 * t| * L < 1 -> (\int[gauss n]_x (expR (t * centered_chi2 a x))%:E <= (expR (t ^+ 2 * mxdot a a / (1 - 2 * `|t| * L)))%:E)%E
For x of law gauss n and weights a with |a_i| <= L, Q = sum_i a_i (x_i^2 - 1) satisfies E[expR (t Q)] <= expR (t^2 |a|^2 / (1 - 2 |t| L)) when 2 |t| L < 1, and P(|Q| >= u) <= 2 expR (- u^2 / (4 (|a|^2 + L u))) for u > 0.
theories/ by: Gaussian/Orthogonal/WeightedSquareTail Statement as written in the source
Lemma integral_gauss_expR_centered_chi2_le n (a : 'rV[R]_n) t L : (forall i, `|a 0 i| <= L) -> `|2 * t| * L < 1 -> (\int[gauss n]_x (expR (t * centered_chi2 a x))%:E <= (expR (t ^+ 2 * mxdot a a / (1 - 2 * `|t| * L)))%:E)%E.
Used by 2 declarations in 2 files
- GaussianAnalysis.probability.hanson_wright: gauss_chaos_mgf
- this file: gauss_centered_chi2_upper_tail
forall {R : realType} [n : nat] [a : 'rV_n] [L u : R], 0 <= L -> (forall i : 'I_n, `|a 0 i| <= L) -> 0 < u -> 0 < mxdot a a + L * u -> (gauss n [set x | (u <= centered_chi2 a x)%R] <= (expR (- u ^+ 2 / (4 * (mxdot a a + L * u))))%:E)%E
Statement as written in the source
Theorem gauss_centered_chi2_upper_tail n (a : 'rV[R]_n) L u : 0 <= L -> (forall i, `|a 0 i| <= L) -> 0 < u -> 0 < mxdot a a + L * u -> (gauss n [set x | u <= centered_chi2 a x]%R <= (expR (- u ^+ 2 / (4 * (mxdot a a + L * u))))%:E)%E.
Used by 3 declarations in 2 files
- GaussianAnalysis.random_matrix.goe_entries: goe_mx_row_tail
- this file: gauss_centered_chi2_lower_tail, gauss_centered_chi2_abs_tail
forall {R : realType} [n : nat] (a x : 'rV_n), centered_chi2 (- a) x = - centered_chi2 a x
Statement as written in the source
Lemma centered_chi2N n (a x : 'rV[R]_n) : centered_chi2 (- a) x = - centered_chi2 a x.
Used by 1 declaration in 1 file
- this file: gauss_centered_chi2_lower_tail
forall {R : realType} [n : nat] [a : 'rV_n] [L u : R], 0 <= L -> (forall i : 'I_n, `|a 0 i| <= L) -> 0 < u -> 0 < mxdot a a + L * u -> (gauss n [set x | (centered_chi2 a x <= - u)%R] <= (expR (- u ^+ 2 / (4 * (mxdot a a + L * u))))%:E)%E
Statement as written in the source
Theorem gauss_centered_chi2_lower_tail n (a : 'rV[R]_n) L u : 0 <= L -> (forall i, `|a 0 i| <= L) -> 0 < u -> 0 < mxdot a a + L * u -> (gauss n [set x | centered_chi2 a x <= - u]%R <= (expR (- u ^+ 2 / (4 * (mxdot a a + L * u))))%:E)%E.
Used by 1 declaration in 1 file
- this file: gauss_centered_chi2_abs_tail
forall {R : realType} [n : nat] [a : 'rV_n] [L u : R], 0 <= L -> (forall i : 'I_n, `|a 0 i| <= L) -> 0 < u -> 0 < mxdot a a + L * u -> (gauss n [set x | (u <= `|centered_chi2 a x|)%R] <= (2 * expR (- u ^+ 2 / (4 * (mxdot a a + L * u))))%:E)%E
Stated in the README together with integral_gauss_expR_centered_chi2_le.
Statement as written in the source
Theorem gauss_centered_chi2_abs_tail n (a : 'rV[R]_n) L u : 0 <= L -> (forall i, `|a 0 i| <= L) -> 0 < u -> 0 < mxdot a a + L * u -> (gauss n [set x | u <= `|centered_chi2 a x|]%R <= (2 * expR (- u ^+ 2 / (4 * (mxdot a a + L * u))))%:E)%E.