On this page
Exponential moments and tails of the normal law
Imports 1 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.interval, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.classical.cardinality, mathcomp.classical.fsbigop, 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.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 9
- GaussianAnalysis.probability.subgaussian
- GaussianAnalysis.probability.subgaussian_matrix
- GaussianAnalysis.probability.hanson_wright
- GaussianAnalysis.comparison.chi_square
- GaussianAnalysis.comparison.normal_linear
- GaussianAnalysis.comparison.gauss_linear
- GaussianAnalysis.comparison.gauss_smoothing
- GaussianAnalysis.comparison.gauss_concentration
- GaussianAnalysis.comparison.ornstein_uhlenbeck
Required by 1 files of the paper proofs
For s != 0, normal_prob m s is the normal law of mean m and variance s^2 of MathComp-Analysis. This file computes its moment generating function, E[expR (t X)] = expR (t m + t^2 s^2 / 2) for X of law normal_prob m s (integral_normal_expR), and deduces Chernoff bounds for its tails: P(X >= m + u) and P(X <= m - u) are at most expR (- u^2 / (2 s^2)) for u >= 0 (normal_prob_upper_tail, normal_prob_lower_tail), and P(|X - m| >= u) is at most twice that (normal_prob_abs_tail).
measure_ge_expR is Chernoff's bound in integral form: P(u <= f) <= E[expR (t (f - u))] for every measure P, measurable f and t >= 0.
Main results
| Results | Statement |
|---|---|
The moment generating function of normal_prob m s, for s != 0, is t |-> expR (t m + t^2 s^2 / 2). | |
For X of law normal_prob m s and u >= 0, P(X >= m + u) and P(X <= m - u) are at most expR (- u^2 / (2 s^2)), and P(|X - m| >= u) is at most twice that. | |
Chernoff's bound: P(u <= f) <= E[expR (t (f - u))] for every measure, measurable f and t >= 0. |
Declarations9 exported
Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : {measure set T -> \bar R}).
forall [d : measure_display] [T : measurableType d] [R : realType] (P : measure T R) [f : T -> R] (u : R) [t : R], measurable_fun [set: T] f -> 0 <= t -> (P [set x | (u <= f x)%R] <= \int[P]_x (expR (t * (f x - u)))%:E)%E
Chernoff's bound: P(u <= f) <= E[expR (t (f - u))] for every measure, measurable f and t >= 0.
Statement as written in the source
Lemma measure_ge_expR (f : T -> R) (u t : R) : measurable_fun [set: T] f -> (0 <= t)%R -> P [set x | u <= f x]%R <= \int[P]_x (expR (t * (f x - u)))%:E.
Used by 7 declarations in 5 files
- GaussianAnalysis.probability.subgaussian: subgaussian_tail, subexponential_tail, bernstein_upper
- GaussianAnalysis.probability.subgaussian_matrix: mgf_upper_tail
- GaussianAnalysis.probability.hanson_wright: hanson_wright_upper
- GaussianAnalysis.comparison.chi_square: gauss_centered_chi2_upper_tail
- GaussianAnalysis.comparison.gauss_concentration: gauss_concentration_upper_tail
Context {R : realType}. Local Notation mu := (@lebesgue_measure R). Implicit Types m s t x a r u : R.
forall {R : realType} (m : R) [s : R] (t x : R), s != 0 -> expR (t * x) * normal_pdf m s x = expR (t * m + t ^+ 2 * s ^+ 2 / 2) * normal_pdf (m + t * s ^+ 2) s x
Statement as written in the source
Lemma normal_pdf_expR m s t x : s != 0 -> expR (t * x) * normal_pdf m s x = expR (t * m + t ^+ 2 * s ^+ 2 / 2) * normal_pdf (m + t * s ^+ 2) s x.
Used by 1 declaration in 1 file
- this file: integral_normal_expR
forall {R : realType} (m : R) [s : R] (t : R), s != 0 -> (\int[normal_prob m s]_x (expR (t * x))%:E)%E = (expR (t * m + t ^+ 2 * s ^+ 2 / 2))%:E
The moment generating function of normal_prob m s, for s != 0, is t |-> expR (t m + t^2 s^2 / 2).
Statement as written in the source
Lemma integral_normal_expR m s t : s != 0 -> (\int[normal_prob m s]_x (expR (t * x))%:E = (expR (t * m + t ^+ 2 * s ^+ 2 / 2))%:E)%E.
Used by 6 declarations in 4 files
- GaussianAnalysis.probability.subgaussian: subgaussian_of_mgf
- GaussianAnalysis.probability.hanson_wright: integral_gauss_expR_dot
- this file: integrable_normal_expR, normal_prob_ge, normal_prob_le
- GaussianAnalysis.comparison.gauss_linear: integral_gauss_expR_mxdot
forall {R : realType} (m : R) [s : R] (t : R), s != 0 -> (normal_prob m s).-integrable [set: g_sigma_algebraType (R.-ocitv).-measurable] (fun x : R => (expR (t * x))%:E)
Statement as written in the source
Lemma integrable_normal_expR m s t : s != 0 -> (normal_prob m s).-integrable setT (fun x => (expR (t * x))%:E).
Used by 1 declaration in 1 file
- GaussianAnalysis.comparison.gauss_smoothing: integrable_normal_expR_abs
forall {R : realType} (m : R) [s : R] (a : R) [r : R], s != 0 -> 0 <= r -> (normal_prob m s [set x | (a <= x)%R] <= (expR (r * (m - a) + r ^+ 2 * s ^+ 2 / 2))%:E)%E
Statement as written in the source
Lemma normal_prob_ge m s a r : s != 0 -> 0 <= r -> (normal_prob m s [set x | a <= x]%R <= (expR (r * (m - a) + r ^+ 2 * s ^+ 2 / 2))%:E)%E.
Used by 1 declaration in 1 file
- this file: normal_prob_upper_tail
forall {R : realType} (m : R) [s : R] (a : R) [r : R], s != 0 -> 0 <= r -> (normal_prob m s [set x | (x <= a)%R] <= (expR (r * (a - m) + r ^+ 2 * s ^+ 2 / 2))%:E)%E
Statement as written in the source
Lemma normal_prob_le m s a r : s != 0 -> 0 <= r -> (normal_prob m s [set x | x <= a]%R <= (expR (r * (a - m) + r ^+ 2 * s ^+ 2 / 2))%:E)%E.
Used by 1 declaration in 1 file
- this file: normal_prob_lower_tail
forall {R : realType} (m : R) [s u : R], s != 0 -> 0 <= u -> (normal_prob m s [set x | (m + u <= x)%R] <= (expR (- u ^+ 2 / (2 * s ^+ 2)))%:E)%E
For X of law normal_prob m s and u >= 0, P(X >= m + u) and P(X <= m - u) are at most expR (- u^2 / (2 s^2)), and P(|X - m| >= u) is at most twice that.
Statement as written in the source
Lemma normal_prob_upper_tail m s u : s != 0 -> 0 <= u -> (normal_prob m s [set x | m + u <= x]%R <= (expR (- u ^+ 2 / (2 * s ^+ 2)))%:E)%E.
Used by 2 declarations in 2 files
- this file: normal_prob_abs_tail
- GaussianAnalysis.comparison.gauss_linear: gauss_mxdot_upper_tail
forall {R : realType} (m : R) [s u : R], s != 0 -> 0 <= u -> (normal_prob m s [set x | (x <= m - u)%R] <= (expR (- u ^+ 2 / (2 * s ^+ 2)))%:E)%E
Stated in the README together with normal_prob_upper_tail.
Statement as written in the source
Lemma normal_prob_lower_tail m s u : s != 0 -> 0 <= u -> (normal_prob m s [set x | x <= m - u]%R <= (expR (- u ^+ 2 / (2 * s ^+ 2)))%:E)%E.
Used by 1 declaration in 1 file
- this file: normal_prob_abs_tail
forall {R : realType} (m : R) [s u : R], s != 0 -> 0 <= u -> (normal_prob m s [set x | (u <= `|x - m|)%R] <= (2 * expR (- u ^+ 2 / (2 * s ^+ 2)))%:E)%E
Stated in the README together with normal_prob_upper_tail.
Statement as written in the source
Lemma normal_prob_abs_tail m s u : s != 0 -> 0 <= u -> (normal_prob m s [set x | u <= `|x - m|]%R <= (2 * expR (- u ^+ 2 / (2 * s ^+ 2)))%:E)%E.
Used by 2 declarations in 2 files
- GaussianAnalysis.comparison.gauss_linear: gauss_mxdot_abs_tail
- GaussianAnalysis.comparison.ornstein_uhlenbeck: normal_continuous_approx