On this page

The Efron-Stein inequality and moment bounds for product laws

GaussianAnalysis.probability.efron_steinlibrary/probability/efron_stein.v1,005 lines35 lemmas and theoremssource

Imports 3 library modules and 23 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.ring_tactic, mathcomp.algebra.field_tactic

Imported by 6

Required by 7 files of the paper proofs

For x of law tuple_prod mu n (lindeberg.v), x^(i) is x with its coordinate i replaced by an independent t of law mu i: tuple_set x i t. Variances are those of probability.v, with values in [0, +oo]: 'V_P[X] is +oo when X is measurable and not square integrable (varianceT, sqr_dev_variance).

Fubini at one coordinate, for F measurable and nonnegative (ge0_integral_tuple_prod_set) and for F integrable (integral_tuple_prod_set): \int[tuple_prod mu n]_x F x is \int[tuple_prod mu n]_x \int[mu i]_t F (tuple_set x i t). The inner integral is a measurable function of x (measurable_tuple_set_integral, measurable_integral_tuple_set), and for F integrable, t |-> F (tuple_set x i t) is integrable for almost every x (ae_integrable_tuple_set).
sqr_dev_variance: E (X - c)^2 = Var X + (E X - c)^2 for X measurable and c real; variance_le_sqr_dev: Var X <= E (X - c)^2; variance_resample: E (X - X')^2 = 2 Var X for an independent copy X'.
efron_stein_pair: for F integrable on a product of two probabilities, Var F <= E_y Var_x F (x, y) + E_x Var_y F (x, y).
efron_stein_integrable (F integrable) and efron_stein (F in L^2): 'V_(tuple_prod mu n)[F] <= \sum_(i < n) \int[tuple_prod mu n]_x V i x, where V i x = 'V_(mu i)[fun t => F (tuple_set x i t)].
efron_stein_resample: Var F <= 1/2 \sum_i E (F (x) - F (x^(i)))^2, since E (F (x) - F (x^(i)))^2 = 2 E V i (integral_resample_tuple_set).
One coordinate and the others: the coordinate i of tuple_prod mu n has law mu i (ge0_integral_tuple_prod_coord, integral_tuple_prod_coord), and E [f (x_i) H (x)] = E [f] E [H] when H does not depend on x_i (ge0_integral_tuple_prod_coordM, integral_tuple_prod_coordM, with the integrability of the product).
cauchy_schwarz: (int |f g|)^2 <= int f^2 int g^2, from Hoelder.
Moments from Efron-Stein (the L^p recursion of Koehler and Sohn, in the proof of their Proposition 2.6, at p = 4): efron_stein_fourth, if E (F (x) - F (x^(i)))^4 <= D_i^2 for every i, then E (F - E F)^4 <= 9/2 (sum_i D_i)^2; by Efron-Stein for (F - E F)^2, Cauchy-Schwarz and the two estimates resample_sqr_le and resample_sqr_sqr_le of one resampled coordinate.

Main results

Results	Statement
ge0_integral_tuple_prod_setintegral_tuple_prod_setge0_integral_tuple_prod_coordintegral_tuple_prod_coordM	Fubini at one coordinate of `tuple_prod mu n`: resampling coordinate `i` by an independent `t` of law `mu i` (`tuple_set x i t`) does not change the integral; coordinate `i` has law `mu i`, and `E[f (x_i) H (x)] = E[f] E[H]` when `H` does not depend on `x_i`.
efron_steinefron_stein_resampleefron_stein_pairvariance_resamplesqr_dev_variancecauchy_schwarz	The Efron-Stein inequality: `Var F <= sum_i E Var_(x_i) F = 1/2 sum_i E (F (x) - F (x^(i)))^2` for `F` square integrable under `tuple_prod mu n`, `x^(i)` being `x` with coordinate `i` resampled; `E (X - X')^2 = 2 Var X` for an independent copy; `(int \|f g\|)^2 <= int f^2 int g^2`.
efron_stein_fourth	The `L^4` step of the moment recursion of Koehler and Sohn (proof of their Proposition 2.6): if `E (F (x) - F (x^(i)))^4 <= D_i^2` for every `i`, then `E (F - E F)^4 <= 9/2 (sum_i D_i)^2`.

Declarations35 exported

lemma tuple_set_set source, line 59

forall [U : Type] [n : nat] (x : n.-tuple U) (i : 'I_n) (s t : U),
tuple_set (tuple_set x i s) i t = tuple_set x i t

Statement as written in the source

Lemma tuple_set_set (U : Type) n (x : n.-tuple U) (i : 'I_n) (s t : U) :
  tuple_set (tuple_set x i s) i t = tuple_set x i t.

Used by 2 declarations in 2 files

this file: integral_resample_tuple_set
GaussianAnalysis.convex.barrier_lindeberg: lindeberg_telescope

sectionresample

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

lemma measurable_tuple_set_pair source, line 67

forall [d : measure_display] [T : measurableType d] [n : nat] (i : 'I_n),
measurable_fun [set: n.-tuple T * T]
  (fun
     p : ((n.-tuple _) * T) =>
   tuple_set p.1 i p.2)

Statement as written in the source

Lemma measurable_tuple_set_pair n (i : 'I_n) :
  measurable_fun [set: n.-tuple T * T] (fun p => tuple_set p.1 i p.2).

Used by 8 declarations in 1 file

this file: measurable_tuple_set_integral, ge0_integral_tuple_prod_set, integrable_tuple_prod_set_pair, integral_tuple_prod_set, measurable_variance_tuple_set, integral_resample_tuple_set, resample_sqr_le, resample_sqr_sqr_le

lemma measurable_tuple_set_integral source, line 80

forall [d : measure_display] [T : measurableType d] [R : realType]
  (nu : nat -> probability T R) [n : nat] (i : 'I_n) [H : n.-tuple T -> \bar R],
measurable_fun [set: n.-tuple T] H ->
(forall x : n.-tuple T, (0%R <= H x)%E) ->
measurable_fun [set: n.-tuple T]
  (fun x : n.-tuple _ =>
   (\int[nu i]_t H (tuple_set x i t))%E)

The integral over one coordinate is a measurable function of the others.

Statement as written in the source

Lemma measurable_tuple_set_integral (nu : nat -> probability T R) n (i : 'I_n)
    (H : n.-tuple T -> \bar R) :
  measurable_fun [set: n.-tuple T] H -> (forall x, 0 <= H x) ->
  measurable_fun [set: n.-tuple T] (fun x => \int[nu i]_t H (tuple_set x i t)).

Used by 4 declarations in 3 files

GaussianAnalysis.probability.efron_stein_omission: efron_stein_omission
GaussianAnalysis.probability.symmetrization: jensen_step, fubini_pair
GaussianAnalysis.convex.barrier_lindeberg: lindeberg_telescope

lemma ge0_integral_tuple_prod_set main result source, line 94

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] (i : 'I_n) [F : n.-tuple T -> \bar R],
measurable_fun [set: n.-tuple T] F ->
(forall x : n.-tuple T, (0%R <= F x)%E) ->
(\int[tuple_prod mu n]_x F x)%E =
(\int[tuple_prod mu n]_x \int[mu i]_t F (tuple_set x i t))%E

Fubini at one coordinate: resampling coordinate i does not change the integral of a nonnegative function.

Main result, as the README states it

Fubini at one coordinate of tuple_prod mu n: resampling coordinate i by an independent t of law mu i (tuple_set x i t) does not change the integral; coordinate i has law mu i, and E[f (x_i) H (x)] = E[f] E[H] when H does not depend on x_i.

Statement as written in the source

Lemma ge0_integral_tuple_prod_set (mu : nat -> probability T R) n (i : 'I_n)
    (F : n.-tuple T -> \bar R) :
  measurable_fun [set: n.-tuple T] F -> (forall x, 0 <= F x) ->
  \int[tuple_prod mu n]_x F x =
  \int[tuple_prod mu n]_x \int[mu i]_t F (tuple_set x i t).

Used by 11 declarations in 4 files

this file: integrable_tuple_prod_set_pair, integral_tuple_prod_set, ge0_integral_tuple_prod_coord, ge0_integral_tuple_prod_coordM, integral_resample_tuple_set, resample_sqr_sqr_le
GaussianAnalysis.probability.efron_stein_omission: efron_stein_omission
GaussianAnalysis.probability.symmetrization: jensen_step, fubini_pair
GaussianAnalysis.convex.barrier_lindeberg: ge0_integral_tuple_prod_tnth, lindeberg_telescope

lemma integrable_tuple_prod_set_pair source, line 138

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] (i : 'I_n) [F : n.-tuple T -> \bar R],
(tuple_prod mu n).-integrable [set: n.-tuple T] F ->
(tuple_prod mu n \x mu i)%E.-integrable [set: n.-tuple T * T]
  (fun p : ((n.-tuple T) * T) =>
   F (tuple_set p.1 i p.2))

Statement as written in the source

Lemma integrable_tuple_prod_set_pair (mu : nat -> probability T R) n
    (i : 'I_n) (F : n.-tuple T -> \bar R) :
  (tuple_prod mu n).-integrable [set: n.-tuple T] F ->
  (tuple_prod mu n \x mu i).-integrable [set: n.-tuple T * T]
    (fun p => F (tuple_set p.1 i p.2)).

Used by 3 declarations in 1 file

this file: ae_integrable_tuple_set, measurable_integral_tuple_set, integral_tuple_prod_set

lemma ae_integrable_tuple_set source, line 161

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] (i : 'I_n) [F : n.-tuple T -> \bar R],
(tuple_prod mu n).-integrable [set: n.-tuple T] F ->
\forall x \ae tuple_prod mu n, (mu i).-integrable [set: T]
                                 (fun t : T => F (tuple_set x i t))

For F integrable, its restriction to the coordinate i is integrable for almost every value of the other coordinates.

Statement as written in the source

Lemma ae_integrable_tuple_set (mu : nat -> probability T R) n (i : 'I_n)
    (F : n.-tuple T -> \bar R) :
  (tuple_prod mu n).-integrable [set: n.-tuple T] F ->
  {ae tuple_prod mu n, forall x,
    (mu i).-integrable [set: T] (fun t => F (tuple_set x i t))}.

lemma measurable_integral_tuple_set source, line 170

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] (i : 'I_n) [F : n.-tuple T -> \bar R],
(tuple_prod mu n).-integrable [set: n.-tuple T] F ->
measurable_fun [set: n.-tuple T]
  (fun x : n.-tuple _ =>
   (\int[mu i]_t F (tuple_set x i t))%E)

Statement as written in the source

Lemma measurable_integral_tuple_set (mu : nat -> probability T R) n (i : 'I_n)
    (F : n.-tuple T -> \bar R) :
  (tuple_prod mu n).-integrable [set: n.-tuple T] F ->
  measurable_fun [set: n.-tuple T] (fun x => \int[mu i]_t F (tuple_set x i t)).

lemma integral_tuple_prod_set main result source, line 179

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] (i : 'I_n) [F : n.-tuple T -> \bar R],
(tuple_prod mu n).-integrable [set: n.-tuple T] F ->
(\int[tuple_prod mu n]_x F x)%E =
(\int[tuple_prod mu n]_x \int[mu i]_t F (tuple_set x i t))%E

Fubini at one coordinate, for integrable functions.

Main result

Stated in the README together with ge0_integral_tuple_prod_set.

Statement as written in the source

Lemma integral_tuple_prod_set (mu : nat -> probability T R) n (i : 'I_n)
    (F : n.-tuple T -> \bar R) :
  (tuple_prod mu n).-integrable [set: n.-tuple T] F ->
  \int[tuple_prod mu n]_x F x =
  \int[tuple_prod mu n]_x \int[mu i]_t F (tuple_set x i t).

Used by 1 declaration in 1 file

this file: integral_tuple_prod_coordM

lemma ge0_integral_tuple_prod_coord main result source, line 209

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] (i : 'I_n) [f : T -> \bar R],
measurable_fun [set: T] f ->
(forall t : T, (0%R <= f t)%E) ->
(\int[tuple_prod mu n]_x f (tnth x i))%E = (\int[mu i]_t f t)%E

The law of the coordinate i of tuple_prod mu n is mu i.

Main result

Stated in the README together with ge0_integral_tuple_prod_set.

Statement as written in the source

Lemma ge0_integral_tuple_prod_coord (mu : nat -> probability T R) n (i : 'I_n)
    (f : T -> \bar R) :
  measurable_fun setT f -> (forall t, 0 <= f t) ->
  \int[tuple_prod mu n]_x f (tnth x i) = \int[mu i]_t f t.

Used by 1 declaration in 1 file

this file: integral_tuple_prod_coord

lemma integral_tuple_prod_coord source, line 225

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] (i : 'I_n) [f : T -> \bar R],
measurable_fun [set: T] f ->
(\int[tuple_prod mu n]_x f (tnth x i))%E = (\int[mu i]_t f t)%E

Statement as written in the source

Lemma integral_tuple_prod_coord (mu : nat -> probability T R) n (i : 'I_n)
    (f : T -> \bar R) : measurable_fun setT f ->
  \int[tuple_prod mu n]_x f (tnth x i) = \int[mu i]_t f t.

lemma ge0_integral_tuple_prod_coordM source, line 237

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] [i : 'I_n] [f : T -> \bar R]
  [H : n.-tuple T -> \bar R],
measurable_fun [set: T] f ->
(forall t : T, (0%R <= f t)%E) ->
measurable_fun [set: n.-tuple _] H ->
(forall x : n.-tuple T, (0%R <= H x)%E) ->
(forall (x : n.-tuple T) (t : T), H (tuple_set x i t) = H x) ->
(\int[tuple_prod mu n]_x (f (tnth x i) * H x))%E =
(\int[mu i]_t f t * \int[tuple_prod mu n]_x H x)%E

Independence of the coordinate i from the others: for H that does not depend on the coordinate i, E [f (x_i) H (x)] = E [f (x_i)] E [H (x)].

Statement as written in the source

Lemma ge0_integral_tuple_prod_coordM (mu : nat -> probability T R) n
    (i : 'I_n) (f : T -> \bar R) (H : n.-tuple T -> \bar R) :
  measurable_fun setT f -> (forall t, 0 <= f t) ->
  measurable_fun setT H -> (forall x, 0 <= H x) ->
  (forall x t, H (tuple_set x i t) = H x) ->
  \int[tuple_prod mu n]_x (f (tnth x i) * H x) =
  \int[mu i]_t f t * \int[tuple_prod mu n]_x H x.

Used by 1 declaration in 1 file

this file: integral_tuple_prod_coordM

lemma integral_tuple_prod_coordM main result source, line 258

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [i : 'I_n] [f : T -> R] 
  [H : n.-tuple T -> R],
(mu i).-integrable [set: T] (EFin \o f) ->
(tuple_prod mu n).-integrable [set: n.-tuple T] (EFin \o H) ->
(forall (x : n.-tuple T) (t : T), H (tuple_set x i t) = H x) ->
(tuple_prod mu n).-integrable [set: n.-tuple T]
  (fun x : n.-tuple T => (f (tnth x i) * H x)%:E) /\
(\int[tuple_prod mu n]_x (f (tnth x i) * H x)%:E)%E =
(\int[mu i]_t (f t)%:E * \int[tuple_prod mu n]_x (H x)%:E)%E

Main result

Stated in the README together with ge0_integral_tuple_prod_set.

Statement as written in the source

Lemma integral_tuple_prod_coordM (mu : nat -> probability T R) n (i : 'I_n)
    (f : T -> R) (H : n.-tuple T -> R) :
  (mu i).-integrable setT (EFin \o f) ->
  (tuple_prod mu n).-integrable setT (EFin \o H) ->
  (forall x t, H (tuple_set x i t) = H x) ->
  (tuple_prod mu n).-integrable setT (fun x => (f (tnth x i) * H x)%:E) /\
  \int[tuple_prod mu n]_x (f (tnth x i) * H x)%:E =
  \int[mu i]_t (f t)%:E * \int[tuple_prod mu n]_x (H x)%:E.

sectionvariance_facts

Context d (U : measurableType d) (R : realType) (P : probability U R).
Local Open Scope ereal_scope.

lemma varianceT source, line 310

forall [d : measure_display] [U : measurableType d] [R : realType] 
  (P : probability U R) (X : U -> R),
'V_P[X] = (\int[P]_x ((X x - fine (\int[P]_y (X y)%:E)) ^+ 2)%:E)%E

The variance as an integral, with no integrability condition.

Statement as written in the source

Lemma varianceT (X : U -> R) :
  'V_P[X] = \int[P]_x ((X x - fine (\int[P]_y (X y)%:E)) ^+ 2)%:E.

Used by 9 declarations in 3 files

this file: sqr_dev_variance, variance_resample, measurable_variance1, measurable_variance2, efron_stein_pair, variance_distribution, efron_stein_fourth
GaussianAnalysis.convex.feature_moments: reg_quad_var
GaussianAnalysis.convex.gauss_feature: gauss_regular_feature

lemma sqr_dev_Lfun2 source, line 316

forall [d : measure_display] [U : measurableType d] [R : realType] 
  [P : probability U R] [X : U -> R] [c : R],
measurable_fun [set: U] X -> (\int[P]_x ((X x - c) ^+ 2)%:E < +oo)%E -> X \in Lfun P 2

Statement as written in the source

Lemma sqr_dev_Lfun2 (X : U -> R) (c : R) : measurable_fun setT X ->
  \int[P]_x ((X x - c) ^+ 2)%:E < +oo -> X \in Lfun P 2%:E.

Used by 1 declaration in 1 file

this file: sqr_dev_variance

lemma sqr_dev_variance main result source, line 333

forall [d : measure_display] [U : measurableType d] [R : realType] 
  (P : probability U R) [X : U -> R] (c : R),
measurable_fun [set: U] X ->
(\int[P]_x ((X x - c) ^+ 2)%:E)%E = ('V_P[X] + ((fine 'E_P[X] - c) ^+ 2)%:E)%E

The second moment about c is the variance plus the square of the distance from c to the mean, in [0, +oo] and for every measurable X.

Main result

Stated in the README together with efron_stein.

Statement as written in the source

Lemma sqr_dev_variance (X : U -> R) (c : R) : measurable_fun setT X ->
  \int[P]_x ((X x - c) ^+ 2)%:E = 'V_P[X] + ((fine 'E_P[X] - c) ^+ 2)%:E.

Used by 4 declarations in 1 file

this file: variance_le_sqr_dev, sqr_fine_expectation_le, variance_resample, efron_stein_pair

lemma variance_le_sqr_dev source, line 354

forall [d : measure_display] [U : measurableType d] [R : realType] 
  (P : probability U R) [X : U -> R] (c : R),
measurable_fun [set: U] X -> ('V_P[X] <= \int[P]_x ((X x - c) ^+ 2)%:E)%E

The variance is at most the second moment about any point.

Statement as written in the source

Lemma variance_le_sqr_dev (X : U -> R) (c : R) : measurable_fun setT X ->
  'V_P[X] <= \int[P]_x ((X x - c) ^+ 2)%:E.

Used by 2 declarations in 2 files

GaussianAnalysis.probability.efron_stein_omission: efron_stein_omission
GaussianAnalysis.convex.barrier_lindeberg: loo_variance

lemma sqr_fine_expectation_le source, line 360

forall [d : measure_display] [U : measurableType d] [R : realType] 
  (P : probability U R) [X : U -> R],
measurable_fun [set: U] X -> ((fine 'E_P[X] ^+ 2)%:E <= \int[P]_x (X x ^+ 2)%:E)%E

Statement as written in the source

Lemma sqr_fine_expectation_le (X : U -> R) : measurable_fun setT X ->
  ((fine 'E_P[X]) ^+ 2)%:E <= \int[P]_x ((X x) ^+ 2)%:E.

Used by 1 declaration in 1 file

this file: efron_stein_pair

lemma variance_resample main result source, line 369

forall [d : measure_display] [U : measurableType d] [R : realType] 
  (P : probability U R) [X : U -> R],
measurable_fun [set: U] X ->
(\int[P]_s \int[P]_t ((X s - X t) ^+ 2)%:E)%E = ('V_P[X] *+ 2)%E

For an independent copy X' of X, E (X - X')^2 = 2 Var X.

Main result

Stated in the README together with efron_stein.

Statement as written in the source

Lemma variance_resample (X : U -> R) : measurable_fun setT X ->
  \int[P]_s \int[P]_t ((X s - X t) ^+ 2)%:E = 'V_P[X] *+ 2.

Used by 1 declaration in 1 file

this file: integral_resample_tuple_set

sectioncauchy_schwarz

Context d (U : measurableType d) (R : realType).
Variable mu : {measure set U -> \bar R}.
Local Open Scope ereal_scope.

lemma poweR2 source, line 391

forall [R : realType] [y : \bar R], (0%R <= y)%E -> (y `^ 2)%E = (y ^+ 2)%E

Statement as written in the source

Lemma poweR2 (y : \bar R) : 0 <= y -> y `^ 2 = y ^+ 2.

Used by 1 declaration in 1 file

this file: cauchy_schwarz

lemma cauchy_schwarz main result source, line 398

forall [d : measure_display] [U : measurableType d] [R : realType] 
  (mu : measure U R) [f g : U -> R],
measurable_fun [set: U] f ->
measurable_fun [set: U] g ->
((\int[mu]_x `|f x * g x|%:E) ^+ 2 <= \int[mu]_x (f x ^+ 2)%:E * \int[mu]_x (g x ^+ 2)%:E)%E

The Cauchy-Schwarz inequality, in [0, +oo].

Main result

Stated in the README together with efron_stein.

Statement as written in the source

Lemma cauchy_schwarz (f g : U -> R) :
  measurable_fun setT f -> measurable_fun setT g ->
  (\int[mu]_x `|f x * g x|%:E) ^+ 2 <=
  \int[mu]_x (f x ^+ 2)%:E * \int[mu]_x (g x ^+ 2)%:E.

Used by 2 declarations in 1 file

this file: resample_sqr_le, resample_sqr_sqr_le

sectionefron_stein_pair

Context d1 d2 (U1 : measurableType d1) (U2 : measurableType d2) (R : realType).
Variables (m1 : probability U1 R) (m2 : probability U2 R).
Local Open Scope ereal_scope.

lemma measurable_integral1 source, line 431

forall [d1 d2 : measure_display] [U1 : measurableType d1] [U2 : measurableType d2]
  [R : realType] (m1 : probability U1 R) [f : U1 * U2 -> \bar R],
measurable_fun [set: (U1 * U2)] f ->
measurable_fun [set: U2] (fun y : U2 => (\int[m1]_x f (x, y))%E)

Integrating a measurable function in one coordinate gives a measurable function of the other one.

Statement as written in the source

Lemma measurable_integral1 (f : U1 * U2 -> \bar R) : measurable_fun setT f ->
  measurable_fun setT (fun y => \int[m1]_x f (x, y)).

Used by 1 declaration in 1 file

this file: measurable_variance1

lemma measurable_integral2 source, line 445

forall [d1 d2 : measure_display] [U1 : measurableType d1] [U2 : measurableType d2]
  [R : realType] (m2 : probability U2 R) [f : U1 * U2 -> \bar R],
measurable_fun [set: (U1 * U2)] f ->
measurable_fun [set: U1] (fun x : U1 => (\int[m2]_y f (x, y))%E)

Statement as written in the source

Lemma measurable_integral2 (f : U1 * U2 -> \bar R) : measurable_fun setT f ->
  measurable_fun setT (fun x => \int[m2]_y f (x, y)).

Used by 1 declaration in 1 file

this file: measurable_variance2

lemma measurable_variance1 source, line 461

forall [d1 d2 : measure_display] [U1 : measurableType d1] [U2 : measurableType d2]
  [R : realType] (m1 : probability U1 R) [F : U1 * U2 -> R],
measurable_fun [set: (U1 * U2)] F ->
measurable_fun [set: U2] (fun y : U2 => 'V_m1[(fun x : U1 => F (x, y))])

The variance in one coordinate is a measurable function of the other one.

Statement as written in the source

Lemma measurable_variance1 (F : U1 * U2 -> R) : measurable_fun setT F ->
  measurable_fun setT (fun y => 'V_m1[fun x => F (x, y)]).

Used by 1 declaration in 1 file

this file: efron_stein_pair

lemma measurable_variance2 source, line 478

forall [d1 d2 : measure_display] [U1 : measurableType d1] [U2 : measurableType d2]
  [R : realType] (m2 : probability U2 R) [F : U1 * U2 -> R],
measurable_fun [set: (U1 * U2)] F ->
measurable_fun [set: U1] (fun x : U1 => 'V_m2[(fun y : U2 => F (x, y))])

Statement as written in the source

Lemma measurable_variance2 (F : U1 * U2 -> R) : measurable_fun setT F ->
  measurable_fun setT (fun x => 'V_m2[fun y => F (x, y)]).

Used by 3 declarations in 1 file

this file: efron_stein_pair, measurable_variance_tuple_set, efron_stein_integrable

theorem efron_stein_pair main result source, line 496

forall [d1 d2 : measure_display] [U1 : measurableType d1] [U2 : measurableType d2]
  [R : realType] [m1 : probability U1 R] [m2 : probability U2 R] 
  [F : U1 * U2 -> R],
(m1 \x m2)%E.-integrable
  [set: (U1 * U2)] 
  (EFin \o F) ->
('V_(m1 \x m2)[F] <=
 \int[m2]_y 'V_m1[(fun x : U1 => F (x, y))] + \int[m1]_x 'V_m2[(fun y : U2 => F (x, y))])%E

The Efron-Stein inequality for two independent blocks.

Main result

Stated in the README together with efron_stein.

Statement as written in the source

Theorem efron_stein_pair (F : U1 * U2 -> R) :
  (m1 \x m2).-integrable setT (EFin \o F) ->
  'V_(m1 \x m2)[F] <=
    \int[m2]_y 'V_m1[fun x => F (x, y)] + \int[m1]_x 'V_m2[fun y => F (x, y)].

Used by 1 declaration in 1 file

this file: efron_stein_integrable

sectionvariance_distribution

Context d1 d2 (V : measurableType d1) (W : measurableType d2) (R : realType).
Local Open Scope ereal_scope.

lemma integral_distribution_measurable source, line 576

forall [d1 d2 : measure_display] [V : measurableType d1] [W : measurableType d2]
  [R : realType] (P : probability V R) (X : {mfun V >-> W}) [f : W -> \bar R],
measurable_fun [set: W] f -> (\int[distribution P X]_y f y)%E = (\int[P]_x f (X x))%E

Statement as written in the source

Lemma integral_distribution_measurable (P : probability V R)
    (X : {mfun V >-> W}) (f : W -> \bar R) : measurable_fun setT f ->
  \int[distribution P X]_y f y = \int[P]_x f (X x).

Used by 1 declaration in 1 file

this file: variance_distribution

lemma variance_distribution source, line 587

forall [d1 d2 : measure_display] [V : measurableType d1] [W : measurableType d2]
  [R : realType] (P : probability V R) (X : {mfun V >-> W}) [F : W -> R],
measurable_fun [set: W] F -> 'V_(distribution P X)[F] = 'V_P[(F \o X)]

Statement as written in the source

Lemma variance_distribution (P : probability V R) (X : {mfun V >-> W})
    (F : W -> R) : measurable_fun setT F ->
  'V_(distribution P X)[F] = 'V_P[F \o X].

Used by 1 declaration in 1 file

this file: efron_stein_integrable

sectionefron_stein

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

lemma measurable_variance_tuple_set source, line 602

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] (i : 'I_n) [F : n.-tuple T -> R],
measurable_fun [set: n.-tuple _] F ->
measurable_fun [set: n.-tuple _]
  (fun x : n.-tuple _ =>
   'V_(mu i)[(fun t : T => F (tuple_set x i t))])

Statement as written in the source

Lemma measurable_variance_tuple_set (mu : nat -> probability T R) n (i : 'I_n)
    (F : n.-tuple T -> R) : measurable_fun setT F ->
  measurable_fun setT (fun x => 'V_(mu i)[fun t => F (tuple_set x i t)]).

Used by 4 declarations in 3 files

this file: efron_stein_integrable, integral_resample_tuple_set
GaussianAnalysis.probability.efron_stein_omission: efron_stein_omission
GaussianAnalysis.convex.barrier_lindeberg: barrier_lindeberg_variance

theorem efron_stein_integrable source, line 614

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [F : n.-tuple T -> R],
(tuple_prod mu n).-integrable [set: n.-tuple T] (EFin \o F) ->
('V_(tuple_prod mu n)[F] <=
 (\sum_(i < n) (\int[tuple_prod mu n]_x 'V_(mu i)[(fun t : T => F (tuple_set x i t))])%E)%R)%E

The Efron-Stein inequality: the variance of an integrable function of independent coordinates is at most the sum over i of the mean of its variance in the coordinate i, the others being fixed. The variances are in [0, +oo].

Statement as written in the source

Theorem efron_stein_integrable (mu : nat -> probability T R) n
    (F : n.-tuple T -> R) :
  (tuple_prod mu n).-integrable setT (EFin \o F) ->
  'V_(tuple_prod mu n)[F] <=
    \sum_(i < n) \int[tuple_prod mu n]_x
      'V_(mu i)[fun t => F (tuple_set x i t)].

Used by 4 declarations in 3 files

this file: efron_stein, efron_stein_resample
GaussianAnalysis.probability.efron_stein_omission: efron_stein_omission
GaussianAnalysis.convex.barrier_lindeberg: barrier_lindeberg_variance

theorem efron_stein main result source, line 690

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [F : n.-tuple T -> R],
F \in Lfun (tuple_prod mu n) 2 ->
('V_(tuple_prod mu n)[F] <=
 (\sum_(i < n) (\int[tuple_prod mu n]_x 'V_(mu i)[(fun t : T => F (tuple_set x i t))])%E)%R)%E

The Efron-Stein inequality for a square integrable F.

Main result, as the README states it

The Efron-Stein inequality: Var F <= sum_i E Var_(x_i) F = 1/2 sum_i E (F (x) - F (x^(i)))^2 for F square integrable under tuple_prod mu n, x^(i) being x with coordinate i resampled; E (X - X')^2 = 2 Var X for an independent copy; (int |f g|)^2 <= int f^2 int g^2.

Statement as written in the source

Theorem efron_stein (mu : nat -> probability T R) n (F : n.-tuple T -> R) :
  F \in Lfun (tuple_prod mu n) 2%:E ->
  'V_(tuple_prod mu n)[F] <=
    \sum_(i < n) \int[tuple_prod mu n]_x
      'V_(mu i)[fun t => F (tuple_set x i t)].

lemma integral_resample_tuple_set source, line 703

forall [d : measure_display] [T : measurableType d] [R : realType]
  (mu : nat -> probability T R) [n : nat] (i : 'I_n) [F : n.-tuple T -> R],
measurable_fun [set: n.-tuple _] F ->
(\int[tuple_prod mu n]_x \int[mu i]_t ((F x - F (tuple_set x i t)) ^+ 2)%:E)%E =
(\int[tuple_prod mu n]_x 'V_(mu i)[(fun t : T => F (tuple_set x i t))] *+ 2)%E

Resampling the coordinate i: for x' equal to x with its coordinate i replaced by an independent copy, E (F x - F x')^2 is twice the mean of the variance in the coordinate i.

Statement as written in the source

Lemma integral_resample_tuple_set (mu : nat -> probability T R) n (i : 'I_n)
    (F : n.-tuple T -> R) : measurable_fun setT F ->
  \int[tuple_prod mu n]_x \int[mu i]_t ((F x - F (tuple_set x i t)) ^+ 2)%:E =
  (\int[tuple_prod mu n]_x 'V_(mu i)[fun t => F (tuple_set x i t)]) *+ 2.

Used by 1 declaration in 1 file

this file: efron_stein_resample

theorem efron_stein_resample main result source, line 730

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [F : n.-tuple T -> R],
(tuple_prod mu n).-integrable [set: n.-tuple T] (EFin \o F) ->
('V_(tuple_prod mu n)[F] <=
 (2^-1)%:E *
 (\sum_(i < n)
     (\int[tuple_prod mu n]_x \int[mu i]_t ((F x - F (tuple_set x i t)) ^+ 2)%:E)%E)%R)%E

The Efron-Stein inequality with resampled coordinates: Var F <= 1/2 sum_i E (F x - F x^(i))^2.

Main result

Stated in the README together with efron_stein.

Statement as written in the source

Theorem efron_stein_resample (mu : nat -> probability T R) n
    (F : n.-tuple T -> R) :
  (tuple_prod mu n).-integrable setT (EFin \o F) ->
  'V_(tuple_prod mu n)[F] <= 2^-1%:E * \sum_(i < n)
    \int[tuple_prod mu n]_x \int[mu i]_t ((F x - F (tuple_set x i t)) ^+ 2)%:E.

Used by 1 declaration in 1 file

this file: efron_stein_fourth

lemma resample_sqr_le source, line 749

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [i : 'I_n] [F : n.-tuple T -> R] 
  [Di : R],
measurable_fun [set: n.-tuple _] F ->
0 <= Di ->
(\int[tuple_prod mu n]_x \int[mu i]_t ((F x - F (tuple_set x i t)) ^+ 4)%:E <= (Di ^+ 2)%:E)%E ->
(\int[tuple_prod mu n]_x \int[mu i]_t ((F x - F (tuple_set x i t)) ^+ 2)%:E <= Di%:E)%E

The two estimates of one resampled coordinate that the fourth moment bound uses, for F with E F^4 < +oo and m = E F.

Statement as written in the source

Lemma resample_sqr_le (mu : nat -> probability T R) n (i : 'I_n)
    (F : n.-tuple T -> R) (Di : R) :
  measurable_fun setT F -> (0 <= Di)%R ->
  \int[tuple_prod mu n]_x \int[mu i]_t
    ((F x - F (tuple_set x i t)) ^+ 4)%:E <= (Di ^+ 2)%:E ->
  \int[tuple_prod mu n]_x \int[mu i]_t
    ((F x - F (tuple_set x i t)) ^+ 2)%:E <= Di%:E.

Used by 1 declaration in 1 file

this file: efron_stein_fourth

lemma resample_sqr_sqr_le source, line 793

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [i : 'I_n] [F : n.-tuple T -> R] 
  [m Di : R],
measurable_fun [set: n.-tuple _] F ->
0 <= Di ->
(\int[tuple_prod mu n]_x ((F x - m) ^+ 4)%:E < +oo)%E ->
(\int[tuple_prod mu n]_x \int[mu i]_t ((F x - F (tuple_set x i t)) ^+ 4)%:E <= (Di ^+ 2)%:E)%E ->
(\int[tuple_prod mu n]_x
    \int[mu i]_t (((F x - m) ^+ 2 - (F (tuple_set x i t) - m) ^+ 2) ^+ 2)%:E <=
 (4 * Di * Num.ExtraDef.sqrtr (fine (\int[tuple_prod mu n]_x ((F x - m) ^+ 4)%:E)))%:E)%E

Statement as written in the source

Lemma resample_sqr_sqr_le (mu : nat -> probability T R) n (i : 'I_n)
    (F : n.-tuple T -> R) (m Di : R) :
  measurable_fun setT F -> (0 <= Di)%R ->
  \int[tuple_prod mu n]_x ((F x - m) ^+ 4)%:E < +oo ->
  \int[tuple_prod mu n]_x \int[mu i]_t
    ((F x - F (tuple_set x i t)) ^+ 4)%:E <= (Di ^+ 2)%:E ->
  \int[tuple_prod mu n]_x \int[mu i]_t
    (((F x - m) ^+ 2 - (F (tuple_set x i t) - m) ^+ 2) ^+ 2)%:E <=
  (4 * Di * Num.sqrt (fine (\int[tuple_prod mu n]_x ((F x - m) ^+ 4)%:E)))%:E.

Used by 1 declaration in 1 file

this file: efron_stein_fourth

theorem efron_stein_fourth main result source, line 897

forall [d : measure_display] [T : measurableType d] [R : realType]
  [mu : nat -> probability T R] [n : nat] [F : n.-tuple T -> R] 
  [D : nat -> R],
measurable_fun [set: n.-tuple _] F ->
(\int[tuple_prod mu n]_x (F x ^+ 4)%:E < +oo)%E ->
(forall i : nat, 0 <= D i) ->
(forall i : 'I_n,
 (\int[tuple_prod mu n]_x \int[mu i]_t ((F x - F (tuple_set x i t)) ^+ 4)%:E <=
  (D i ^+ 2)%:E)%E) ->
(\int[tuple_prod mu n]_x ((F x - fine (\int[tuple_prod mu n]_y (F y)%:E)) ^+ 4)%:E <=
 (9 / 2 * (\sum_(i < n) D i) ^+ 2)%:E)%E

Moments from Efron-Stein: if E (F (x) - F (x^(i)))^4 <= D_i^2 for every i, then E (F - E F)^4 <= 9/2 (sum_i D_i)^2.

Main result, as the README states it

The L^4 step of the moment recursion of Koehler and Sohn (proof of their Proposition 2.6): if E (F (x) - F (x^(i)))^4 <= D_i^2 for every i, then E (F - E F)^4 <= 9/2 (sum_i D_i)^2.

Statement as written in the source

Theorem efron_stein_fourth (mu : nat -> probability T R) n
    (F : n.-tuple T -> R) (D : nat -> R) :
  measurable_fun setT F ->
  \int[tuple_prod mu n]_x ((F x) ^+ 4)%:E < +oo ->
  (forall i, 0 <= D i)%R ->
  (forall i : 'I_n, \int[tuple_prod mu n]_x \int[mu i]_t
    ((F x - F (tuple_set x i t)) ^+ 4)%:E <= ((D i) ^+ 2)%:E) ->
  \int[tuple_prod mu n]_x
    ((F x - fine (\int[tuple_prod mu n]_y (F y)%:E)) ^+ 4)%:E <=
  (9 / 2 * (\sum_(i < n) D i) ^+ 2)%: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.