On this page
The omission form of the Efron-Stein inequality
Imports 2 library modules and 18 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.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
Let x have law tuple_prod mu n (lindeberg.v): its coordinates are independent, of laws mu 0, ..., mu (n - 1). Let F be an integrable real function of x, and for each i let G i be a measurable function of x that does not depend on the coordinate i: G i (tuple_set x i t) = G i x for all x and t. Then Var F <= \sum_i E (G i - F)^2 (efron_stein_omission), with the variance and the expectations in [0, +oo] as in efron_stein.v. For a statistic F of independent data, G i is typically the same statistic computed without the datum i; this is the form of Steele, written by Boucheron, Bousquet, Lugosi and Massart (Concentration inequalities, Section 3.2, equation (3.6)). efron_stein_omission_bounded is the case of a bounded measurable F.
The proof bounds the variance in the coordinate i, the others being fixed, by the second moment about the value G i x, which does not depend on that coordinate (variance_le_sqr_dev). The Efron-Stein inequality (efron_stein_integrable) sums these bounds, and Fubini at one coordinate (ge0_integral_tuple_prod_set) integrates the coordinate i back.
This file is a Rocq formalization, in general form, of the lemma 'Deletion variance bound' of 'A limiting satisfiability threshold for every fixed clause size' (family 235 of the OpenAI math collection, revision 1581d4cbd, source/sections/concentration.tex), where F is a statistic of independent data and G i the same statistic with the datum i omitted, its position left blank. The manuscript proves the lemma with the martingale differences of the data revealed one at a time; the proof here goes through the Efron-Stein inequality instead. The file follows no Lean module. The Lean development of the collection bounds the variance by a recursion over the data instead, and the proof of target T7 of phase 12 follows that recursion and does not use this file.
Main results
| Results | Statement |
|---|---|
The omission form of the Efron-Stein inequality (Steele): for x of law tuple_prod mu n, F integrable (or measurable and bounded) and G i measurable with G i (tuple_set x i t) = G i x for all x and t (G i does not depend on the coordinate i), Var F <= sum_i E (G i - F)^2, in [0, +oo]. The lemma 'Deletion variance bound' of family 235 of the OpenAI math collection, in general form. |
Declarations2 exported
Context d (T : measurableType d) (R : realType). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType] [mu : nat -> probability T R] [n : nat] [F : n.-tuple T -> R] [G : 'I_n -> n.-tuple T -> R], (tuple_prod mu n).-integrable [set: n.-tuple T] (EFin \o F) -> (forall i : 'I_n, measurable_fun [set: n.-tuple _] (G i)) -> (forall (i : 'I_n) (x : n.-tuple T) (t : T), G i (tuple_set x i t) = G i x) -> ('V_(tuple_prod mu n)[F] <= (\sum_(i < n) (\int[tuple_prod mu n]_x ((G i x - F x) ^+ 2)%:E)%E)%R)%E
The omission form of the Efron-Stein inequality: for F integrable and G i measurable and independent of the coordinate i, Var F <= \sum_i E (G i - F)^2.
The omission form of the Efron-Stein inequality (Steele): for x of law tuple_prod mu n, F integrable (or measurable and bounded) and G i measurable with G i (tuple_set x i t) = G i x for all x and t (G i does not depend on the coordinate i), Var F <= sum_i E (G i - F)^2, in [0, +oo]. The lemma 'Deletion variance bound' of family 235 of the OpenAI math collection, in general form.
Statement as written in the source
Theorem efron_stein_omission (mu : nat -> probability T R) n (F : n.-tuple T -> R) (G : 'I_n -> n.-tuple T -> R) : (tuple_prod mu n).-integrable setT (EFin \o F) -> (forall i, measurable_fun setT (G i)) -> (forall i x t, G i (tuple_set x i t) = G i x) -> 'V_(tuple_prod mu n)[F] <= \sum_(i < n) \int[tuple_prod mu n]_x ((G i x - F x) ^+ 2)%:E.
Used by 1 declaration in 1 file
- this file: efron_stein_omission_bounded
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) [n : nat] [F : n.-tuple T -> R] [G : 'I_n -> n.-tuple T -> R] [C : R], measurable_fun [set: n.-tuple _] F -> (forall x : n.-tuple T, `|F x| <= C) -> (forall i : 'I_n, measurable_fun [set: n.-tuple _] (G i)) -> (forall (i : 'I_n) (x : n.-tuple T) (t : T), G i (tuple_set x i t) = G i x) -> ('V_(tuple_prod mu n)[F] <= (\sum_(i < n) (\int[tuple_prod mu n]_x ((G i x - F x) ^+ 2)%:E)%E)%R)%E
The same for a bounded measurable F.
Stated in the README together with efron_stein_omission.
Statement as written in the source
Corollary efron_stein_omission_bounded (mu : nat -> probability T R) n (F : n.-tuple T -> R) (G : 'I_n -> n.-tuple T -> R) (C : R) : measurable_fun setT F -> (forall x, `|F x| <= C)%R -> (forall i, measurable_fun setT (G i)) -> (forall i x t, G i (tuple_set x i t) = G i x) -> 'V_(tuple_prod mu n)[F] <= \sum_(i < n) \int[tuple_prod mu n]_x ((G i x - F x) ^+ 2)%:E.