On this page
Moment inequalities
Imports 0 library modules and 22 external
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, 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.hoelder, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.field_tactic
Imported by 5
Required by 2 files of the paper proofs
Lower bounds on probabilities from the first moments of a real random variable X on a probability space P, and the facts on square integrable variables they need.
- paley_zygmund: for X square integrable and 0 <= theta < E X, P(theta <= X) >= (E X - theta)^2 / E X^2, without sign condition on X.
- paley_zygmund_sqr: the same applied to X^2, a small-ball estimate from the second and fourth moments: for X in L^4 with E X^2 > 0 and 0 <= t < 1, P(t E X^2 <= X^2) >= (1 - t)^2 (E X^2)^2 / E X^4.
- expectation_sqr_le: (E X)^2 <= E X^2 for X square integrable.
- integrable_sqr_Lfun2, Lfun2_sqr, Lfun4_sqr: X is in L^2 when it is measurable and X^2 is integrable; X^2 is in L^1 when X is in L^2, and in L^2 when X is in L^4.
Main results
| Results | Statement | Used by theories/ |
|---|---|---|
Paley-Zygmund: if X is square integrable and 0 <= theta < E X, then P(theta <= X) >= (E X - theta)^2 / E X^2. No sign condition on X. | Head/ | |
Small-ball estimate from the second and fourth moments: if X is in L^4, E X^2 > 0 and 0 <= t < 1, then P(t E X^2 <= X^2) >= (1 - t)^2 (E X^2)^2 / E X^4. | none: Head/ applies paley_zygmund to the square directly | |
(E X)^2 <= E X^2 for square integrable X. A measurable X with X^2 integrable is in L^2. | Head/; comparison/ in the library |
Declarations7 exported
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], measurable_fun [set: T] X -> P.-integrable [set: T] (EFin \o (fun x : T => X x ^+ 2)) -> X \in Lfun P 2
Stated in the README together with expectation_sqr_le.
Statement as written in the source
Lemma integrable_sqr_Lfun2 (X : T -> R) : measurable_fun setT X -> P.-integrable setT (EFin \o (fun x => X x ^+ 2)) -> X \in Lfun P 2%:E.
Used by 7 declarations in 6 files
- this file: Lfun4_sqr
- GaussianAnalysis.probability.mixture: Lfun2_mixture
- GaussianAnalysis.probability.efron_stein: sqr_dev_Lfun2, efron_stein_fourth
- GaussianAnalysis.probability.small_ball_method: paley_zygmund_half
- GaussianAnalysis.comparison.escape: gauss_frobenius_mean_le
- GaussianAnalysis.convex.feature_mixture: moment4_Lfun2_quad
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R], X \in Lfun P 2 -> X ^+ 2 \in Lfun P 1
Statement as written in the source
Lemma Lfun2_sqr (X : T -> R) : X \in Lfun P 2%:E -> X ^+ 2 \in Lfun P 1.
Used by 3 declarations in 2 files
- this file: expectation_sqr_le, paley_zygmund
- GaussianAnalysis.probability.mixture: variance_mixture
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R], X \in Lfun P 4 -> X ^+ 2 \in Lfun P 2
Statement as written in the source
Lemma Lfun4_sqr (X : T -> R) : X \in Lfun P 4%:E -> X ^+ 2 \in Lfun P 2%:E.
Used by 1 declaration in 1 file
- this file: paley_zygmund_sqr
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R], X \in Lfun P 2 -> fine 'E_P[X] ^+ 2 <= fine 'E_P[(X ^+ 2)]
(E X)^2 <= E X^2 for square integrable X. A measurable X with X^2 integrable is in L^2.
Statement as written in the source
Lemma expectation_sqr_le (X : T -> R) : X \in Lfun P 2%:E -> fine 'E_P[X] ^+ 2 <= fine 'E_P[X ^+ 2].
Used by 2 declarations in 2 files
- GaussianAnalysis.probability.small_ball_method: paley_zygmund_half
- GaussianAnalysis.comparison.escape: gauss_frobenius_mean_le
forall [R : realType] (z : R) [theta s : R],
0 <= theta -> 0 <= s -> 2 * s * z <= 2 * s * theta + s ^+ 2 * z ^+ 2 + (theta <= z)%R%:RStatement as written in the source
Lemma paley_zygmund_point (z theta s : R) : 0 <= theta -> 0 <= s -> 2 * s * z <= 2 * s * theta + s ^+ 2 * z ^+ 2 + ((theta <= z)%R)%:R.
Used by 1 declaration in 1 file
- this file: paley_zygmund
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R] [theta : R], X \in Lfun P 2 -> 0 <= theta -> (theta%:E < 'E_P[X])%E -> (((fine 'E_P[X] - theta) ^+ 2 / fine 'E_P[(X ^+ 2)])%:E <= P [set x | (theta <= X x)%R])%E
Paley-Zygmund: if X is square integrable and 0 <= theta < E X, then P(theta <= X) >= (E X - theta)^2 / E X^2. No sign condition on X.
theories/ by: Head/SmallBallPZ Statement as written in the source
Lemma paley_zygmund (X : T -> R) (theta : R) : X \in Lfun P 2%:E -> 0 <= theta -> (theta%:E < 'E_P[X])%E -> (((fine 'E_P[X] - theta) ^+ 2 / fine 'E_P[X ^+ 2])%:E <= P [set x | (theta <= X x)%R])%E.
Used by 2 declarations in 2 files
- this file: paley_zygmund_sqr
- GaussianAnalysis.probability.small_ball_method: paley_zygmund_half
forall [d : measure_display] [T : measurableType d] [R : realType] [P : probability T R] [X : T -> R] [t : R], X \in Lfun P 4 -> 0 <= t < 1 -> (0%R < 'E_P[(X ^+ 2)])%E -> (((1 - t) ^+ 2 * fine 'E_P[(X ^+ 2)] ^+ 2 / fine 'E_P[(X ^+ 4)])%:E <= P [set x | (t * fine 'E_P[(X ^+ 2)] <= X x ^+ 2)%R])%E
Small-ball estimate from the second and fourth moments: if X is in L^4, E X^2 > 0 and 0 <= t < 1, then P(t E X^2 <= X^2) >= (1 - t)^2 (E X^2)^2 / E X^4.
Statement as written in the source
Lemma paley_zygmund_sqr (X : T -> R) (t : R) : X \in Lfun P 4%:E -> 0 <= t < 1 -> (0 < 'E_P[X ^+ 2])%E -> (((1 - t) ^+ 2 * fine 'E_P[X ^+ 2] ^+ 2 / fine 'E_P[X ^+ 4])%:E <= P [set x | (t * fine 'E_P[X ^+ 2] <= X x ^+ 2)%R])%E.