On this page
Rademacher averages, contraction and symmetrization
Imports 3 library modules and 22 external
- GaussianAnalysis.probability.lindeberg
- GaussianAnalysis.probability.tuple_rows
- GaussianAnalysis.probability.efron_stein
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_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.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.probability_theory.probability
Required by 1 files of the paper proofs
Rademacher signs are written as a finite average over the 2^n sign vectors, not as a measure. For independent random elements X_1, ..., X_n (tuple_prod) and a finite class of functions f_j, the tools of empirical process theory that the small-ball method needs, for expectations only: no concentration inequality is used.
Main results:
- rademacher_mean_cst, rademacher_meanD, rademacher_meanZ, ler_rademacher_mean, rademacher_mean_flip, rademacher_mean_neg: the average over signs is linear, monotone, and invariant under changing one sign or all of them; rademacher_mean_prod: E eps_k eps_l = [k == l]; rademacher_mean_sqr_sum, rademacher_mean_abs_sum: E (sum_k a_k eps_k)^2 = sum_k a_k^2, hence E |sum_k a_k eps_k| <= (sum_k a_k^2)^(1/2).
- Contraction (Ledoux-Talagrand), contraction: for a finite class of vectors t_j of R^n and L-Lipschitz phi_k with phi_k(0) = 0,
rademacher_mean (max_j |sum_k eps_k phi_k(t_jk)|) <= 2 L rademacher_mean (max_j |sum_k eps_k t_jk|);
contraction_bigmax0: the same without absolute values and without the factor 2, over the class and the zero vector, proved one coordinate at a time (bigmax0_contraction1).
- Symmetrization (Gine-Zinn), symmetrization: for x of law tuple_prod mu n and measurable f_j integrable for every mu_k,
E max_j |sum_k (f_j(x_k) - E f_j(x_k))| <= 2 E rademacher_mean (max_j |sum_k eps_k f_j(x_k)|),
as integrals in [0, +oo]. Proof: an independent copy as the second block of n + n coordinates of law doubled_law mu n (ge0_integral_tuple_left, ge0_integral_tuple_right); Jensen's inequality for max_norm (jensen_max_norm), one coordinate of the copy at a time, and the exchange of x_k and its copy (ge0_integral_swap), both by Fubini at one coordinate (ge0_integral_tuple_prod_set of efron_stein.v).
- Tools: max_normD, max_normN (max_norm is a norm), measurable_bigmax0, measurable_max_norm, ge0_integral_rademacher_mean, measurable_rademacher_mean.
rademacher b | the sign 1 if b, -1 otherwise |
rademacher_ | 2^-n sum_{s : n.-tuple bool} F s, the expectation of F over n independent signs |
sign_ | s with its sign i changed |
sign_ | s with every sign changed |
max_ | max_j |v j| for v : 'I_m -> R (0 if m = 0) |
doubled_ | the laws of n + n coordinates whose two blocks are independent copies of tuple_prod mu n |
tuple_ | the two blocks of z : (n + n).-tuple T |
Main results
| Results | Statement |
|---|---|
Rademacher averages are averages over the 2^n sign vectors. Ledoux-Talagrand contraction: for L-Lipschitz phi_k with phi_k(0) = 0 and a finite class of vectors t_j, E max_j |sum_k eps_k phi_k(t_jk)| <= 2 L E max_j |sum_k eps_k t_jk|; and E |sum_k a_k eps_k| <= (sum_k a_k^2)^(1/2). | |
Gine-Zinn symmetrization: for x of law tuple_prod mu n and a finite class of measurable f_j integrable for every mu k, E max_j |sum_k (f_j(x_k) - E f_j(x_k))| <= 2 E rademacher_mean (max_j |sum_k eps_k f_j(x_k)|), as integrals in [0, +oo]. |
Declarations50 exported, 12 local
sectionrademacher
Context {R : realType}.
Type
forall {R : realType}, bool -> R
Definition
Definition rademacher (b : bool) : R := if b then 1 else -1.
Used by 14 declarations in 2 files
- this file: rademacherN, rademacher_sqr, normr_rademacher, sum_rademacher_flip, contraction_bigmax0, sum_rademacher_neg, contraction, rademacher_mean_prod, rademacher_mean_sqr_sum, rademacher_mean_abs_sum, B, symmetrization
- GaussianAnalysis.probability.small_ball_method: small_ball_method, small_ball_linear
Type
forall {R : realType} [n : nat], (n.-tuple bool -> R) -> R
Definition
Definition rademacher_mean n (F : n.-tuple bool -> R) : R := (2 ^+ n)^-1 * \sum_(s : n.-tuple bool) F s.
Used by 19 declarations in 2 files
- this file: rademacher_mean_cst, rademacher_meanD, rademacher_meanZ, ler_rademacher_mean, rademacher_mean_ge0, rademacher_mean_flip, rademacher_mean_neg, rademacher_mean_pair, contraction_bigmax0, contraction, rademacher_mean_sum, rademacher_mean_prod, rademacher_mean_sqr_sum, rademacher_mean_abs_sum, ge0_integral_rademacher_mean, measurable_rademacher_mean, symmetrization
- GaussianAnalysis.probability.small_ball_method: small_ball_method, small_ball_linear
sectionrademacher_theory
Context {R : realType}. Local Notation rm := (@rademacher_mean R).
forall {R : realType} (b : bool), rademacher (~~ b) = - rademacher b
Statement as written in the source
Lemma rademacherN b : rademacher (~~ b) = - rademacher b :> R.
Used by 4 declarations in 1 file
- this file: sum_rademacher_flip, sum_rademacher_neg, rademacher_mean_prod, B_set
forall {R : realType} (b : bool), rademacher b ^+ 2 = 1
Statement as written in the source
Lemma rademacher_sqr b : rademacher b ^+ 2 = 1 :> R.
Used by 1 declaration in 1 file
- this file: rademacher_mean_prod
forall {R : realType} (b : bool), `|rademacher b| = 1
Statement as written in the source
Lemma normr_rademacher b : `|rademacher b| = 1 :> R.
forall {R : realType} (n : nat) (c : R), rademacher_mean (fun=> c) = c
Statement as written in the source
Lemma rademacher_mean_cst n (c : R) : rm (fun _ : n.-tuple bool => c) = c.
Used by 3 declarations in 1 file
forall {R : realType} [n : nat] (F G : n.-tuple bool -> R), rademacher_mean (fun s : n.-tuple bool => F s + G s) = rademacher_mean F + rademacher_mean G
Statement as written in the source
Lemma rademacher_meanD n (F G : n.-tuple bool -> R) : rm (fun s => F s + G s) = rm F + rm G.
Used by 4 declarations in 1 file
- this file: rademacher_mean_pair, contraction, rademacher_mean_abs_sum, symmetrization
forall {R : realType} [n : nat] (c : R) (F : n.-tuple bool -> R), rademacher_mean (fun s : n.-tuple bool => c * F s) = c * rademacher_mean F
Statement as written in the source
Lemma rademacher_meanZ n (c : R) (F : n.-tuple bool -> R) : rm (fun s => c * F s) = c * rm F.
Used by 5 declarations in 2 files
- this file: rademacher_mean_pair, contraction_bigmax0, rademacher_mean_sqr_sum, rademacher_mean_abs_sum
- GaussianAnalysis.probability.small_ball_method: small_ball_method
forall {R : realType} [n : nat] [F G : n.-tuple bool -> R], (forall s : n.-tuple bool, F s <= G s) -> rademacher_mean F <= rademacher_mean G
Statement as written in the source
Lemma ler_rademacher_mean n (F G : n.-tuple bool -> R) : (forall s, F s <= G s) -> rm F <= rm G.
Used by 5 declarations in 2 files
- this file: rademacher_mean_ge0, contraction_bigmax0, contraction, symmetrization
- GaussianAnalysis.probability.small_ball_method: small_ball_linear
forall {R : realType} [n : nat] [F : n.-tuple bool -> R], (forall s : n.-tuple bool, 0 <= F s) -> 0 <= rademacher_mean F
Statement as written in the source
Lemma rademacher_mean_ge0 n (F : n.-tuple bool -> R) : (forall s, 0 <= F s) -> 0 <= rm F.
Used by 4 declarations in 2 files
- this file: rademacher_mean_abs_sum, symmetrization
- GaussianAnalysis.probability.small_ball_method: small_ball_method, small_ball_linear
Type
forall [n : nat], 'I_n -> n.-tuple bool -> n.-tuple bool
Definition
Definition sign_flip n (i : 'I_n) (s : n.-tuple bool) : n.-tuple bool := [tuple if j == i then ~~ tnth s j else tnth s j | j < n].
Changing the sign of coordinate i, and of every coordinate.
Used by 10 declarations in 1 file
Type
forall [n : nat], n.-tuple bool -> n.-tuple bool
Definition
Definition sign_neg n (s : n.-tuple bool) : n.-tuple bool := [tuple ~~ tnth s j | j < n].
Used by 4 declarations in 1 file
- this file: sign_negK, rademacher_mean_neg, sum_rademacher_neg, contraction
forall [n : nat] (i j : 'I_n) (s : n.-tuple bool), tnth (sign_flip i s) j = (if j == i then ~~ tnth s j else tnth s j)
Statement as written in the source
Lemma tnth_sign_flip n (i j : 'I_n) s : tnth (sign_flip i s) j = if j == i then ~~ tnth s j else tnth s j.
Used by 5 declarations in 1 file
- this file: sign_flipK, sum_rademacher_flip, rademacher_mean_prod, B_set, symmetrization
forall [n : nat] (i : 'I_n), involutive (sign_flip i)
Statement as written in the source
Lemma sign_flipK n (i : 'I_n) : involutive (sign_flip i).
Used by 1 declaration in 1 file
- this file: rademacher_mean_flip
forall [n : nat], involutive (sign_neg (n:=n))
Statement as written in the source
Lemma sign_negK n : involutive (@sign_neg n).
Used by 1 declaration in 1 file
- this file: rademacher_mean_neg
forall {R : realType} [n : nat] (i : 'I_n) (F : n.-tuple bool -> R), rademacher_mean (fun s : n.-tuple bool => F (sign_flip i s)) = rademacher_mean F
Statement as written in the source
Lemma rademacher_mean_flip n (i : 'I_n) (F : n.-tuple bool -> R) : rm (fun s => F (sign_flip i s)) = rm F.
Used by 2 declarations in 1 file
- this file: rademacher_mean_pair, rademacher_mean_prod
forall {R : realType} [n : nat] (F : n.-tuple bool -> R), rademacher_mean (fun s : n.-tuple bool => F (sign_neg s)) = rademacher_mean F
Statement as written in the source
Lemma rademacher_mean_neg n (F : n.-tuple bool -> R) : rm (fun s => F (sign_neg s)) = rm F.
Used by 1 declaration in 1 file
- this file: contraction
forall {R : realType} [n : nat] (i : 'I_n) (F : n.-tuple bool -> R), rademacher_mean F = rademacher_mean (fun s : n.-tuple bool => 2^-1 * (F s + F (sign_flip i s)))
The average over the sign of coordinate i.
Statement as written in the source
Lemma rademacher_mean_pair n (i : 'I_n) (F : n.-tuple bool -> R) : rm F = rm (fun s => 2^-1 * (F s + F (sign_flip i s))).
Used by 1 declaration in 1 file
- this file: contraction_bigmax0
forall {R : realType} [m : nat] (F : 'I_m -> R), 0 <= \big[maxr/0]_(j < m) F jA maximum \big[Num.max/0] over a class is the maximum over the class and the zero vector.
Statement as written in the source
Lemma bigmax0_ge0 m (F : 'I_m -> R) : 0 <= \big[Num.max/0]_(j < m) F j.
Used by 3 declarations in 1 file
- this file: bigmax0_contraction1, contraction, max_norm_ge0
forall {R : realType} [m : nat] (a t : 'I_m -> R) [phi : R -> R] [L : R], (forall x y : R, `|phi x - phi y| <= L * `|x - y|) -> phi 0 = 0 -> \big[maxr/0]_(j < m) (a j + phi (t j)) + \big[maxr/0]_(j < m) (a j - phi (t j)) <= \big[maxr/0]_(j < m) (a j + L * t j) + \big[maxr/0]_(j < m) (a j - L * t j)
Contraction at one coordinate.
Statement as written in the source
Lemma bigmax0_contraction1 m (a t : 'I_m -> R) (phi : R -> R) (L : R) : (forall x y, `|phi x - phi y| <= L * `|x - y|) -> phi 0 = 0 -> \big[Num.max/0]_(j < m) (a j + phi (t j)) + \big[Num.max/0]_(j < m) (a j - phi (t j)) <= \big[Num.max/0]_(j < m) (a j + L * t j) + \big[Num.max/0]_(j < m) (a j - L * t j).
Used by 1 declaration in 1 file
- this file: contraction_bigmax0
forall {R : realType} [m : nat] [c : R] (F : 'I_m -> R),
0 <= c -> \big[maxr/0]_(j < m) (c * F j) = c * \big[maxr/0]_(j < m) F jStatement as written in the source
Lemma bigmax0_pM m (c : R) (F : 'I_m -> R) : 0 <= c -> \big[Num.max/0]_(j < m) (c * F j) = c * \big[Num.max/0]_(j < m) F j.
Used by 2 declarations in 2 files
- this file: contraction_bigmax0
- GaussianAnalysis.probability.small_ball_method: small_ball_method
forall {R : realType} [n : nat] (i : 'I_n) (s : n.-tuple bool) (g : 'I_n -> R), \sum_(k < n) rademacher (tnth (sign_flip i s) k) * g k = \sum_(k < n | k != i) rademacher (tnth s k) * g k - rademacher (tnth s i) * g i
Statement as written in the source
Lemma sum_rademacher_flip n (i : 'I_n) (s : n.-tuple bool) (g : 'I_n -> R) : \sum_(k < n) rademacher (tnth (sign_flip i s) k) * g k = \sum_(k < n | k != i) rademacher (tnth s k) * g k - rademacher (tnth s i) * g i.
Used by 1 declaration in 1 file
- this file: contraction_bigmax0
forall {R : realType} [n m : nat] (t : 'I_m -> 'I_n -> R) [phi : 'I_n -> R -> R] [L : R], 0 <= L -> (forall (k : 'I_n) (x y : R), `|phi k x - phi k y| <= L * `|x - y|) -> (forall k : 'I_n, phi k 0 = 0) -> rademacher_mean (fun s : n.-tuple bool => \big[maxr/0]_(j < m) \sum_(k < n) rademacher (tnth s k) * phi k (t j k)) <= L * rademacher_mean (fun s : n.-tuple bool => \big[maxr/0]_(j < m) \sum_(k < n) rademacher (tnth s k) * t j k)
Contraction (Ledoux-Talagrand) without absolute values, over a class that contains the zero vector.
Main result
Stated in the README together with contraction.
Statement as written in the source
Lemma contraction_bigmax0 n m (t : 'I_m -> 'I_n -> R) (phi : 'I_n -> R -> R) (L : R) : 0 <= L -> (forall k x y, `|phi k x - phi k y| <= L * `|x - y|) -> (forall k, phi k 0 = 0) -> rm (fun s : n.-tuple bool => \big[Num.max/0]_(j < m) \sum_(k < n) rademacher (tnth s k) * phi k (t j k)) <= L * rm (fun s : n.-tuple bool => \big[Num.max/0]_(j < m) \sum_(k < n) rademacher (tnth s k) * t j k).
Used by 1 declaration in 1 file
- this file: contraction
forall {R : realType} [n : nat] (s : n.-tuple bool) (g : 'I_n -> R), \sum_(k < n) rademacher (tnth (sign_neg s) k) * g k = - \sum_(k < n) rademacher (tnth s k) * g k
Statement as written in the source
Lemma sum_rademacher_neg n (s : n.-tuple bool) (g : 'I_n -> R) : \sum_(k < n) rademacher (tnth (sign_neg s) k) * g k = - \sum_(k < n) rademacher (tnth s k) * g k.
Used by 1 declaration in 1 file
- this file: contraction
forall {R : realType} [n m : nat] (t : 'I_m -> 'I_n -> R) [phi : 'I_n -> R -> R] [L : R], 0 <= L -> (forall (k : 'I_n) (x y : R), `|phi k x - phi k y| <= L * `|x - y|) -> (forall k : 'I_n, phi k 0 = 0) -> rademacher_mean (fun s : n.-tuple bool => \big[maxr/0]_(j < m) `|\sum_(k < n) rademacher (tnth s k) * phi k (t j k)|) <= 2 * L * rademacher_mean (fun s : n.-tuple bool => \big[maxr/0]_(j < m) `|\sum_(k < n) rademacher (tnth s k) * t j k|)
Contraction (Ledoux-Talagrand).
Main result, as the README states it
Rademacher averages are averages over the 2^n sign vectors. Ledoux-Talagrand contraction: for L-Lipschitz phi_k with phi_k(0) = 0 and a finite class of vectors t_j, E max_j |sum_k eps_k phi_k(t_jk)| <= 2 L E max_j |sum_k eps_k t_jk|; and E |sum_k a_k eps_k| <= (sum_k a_k^2)^(1/2).
Statement as written in the source
Lemma contraction n m (t : 'I_m -> 'I_n -> R) (phi : 'I_n -> R -> R) (L : R) : 0 <= L -> (forall k x y, `|phi k x - phi k y| <= L * `|x - y|) -> (forall k, phi k 0 = 0) -> rm (fun s : n.-tuple bool => \big[Num.max/0]_(j < m) `|\sum_(k < n) rademacher (tnth s k) * phi k (t j k)|) <= 2 * L * rm (fun s : n.-tuple bool => \big[Num.max/0]_(j < m) `|\sum_(k < n) rademacher (tnth s k) * t j k|).
Used by 1 declaration in 1 file
- GaussianAnalysis.probability.small_ball_method: small_ball_method
forall {R : realType} [n : nat] [I : finType] (F : I -> n.-tuple bool -> R), rademacher_mean (fun s : n.-tuple bool => \sum_i F i s) = \sum_i rademacher_mean (F i)
Statement as written in the source
Lemma rademacher_mean_sum n (I : finType) (F : I -> n.-tuple bool -> R) : rm (fun s => \sum_(i : I) F i s) = \sum_(i : I) rm (F i).
Used by 1 declaration in 1 file
- this file: rademacher_mean_sqr_sum
forall {R : realType} [n : nat] (k l : 'I_n), rademacher_mean (fun s : n.-tuple bool => rademacher (tnth s k) * rademacher (tnth s l)) = (k == l)%:R
Statement as written in the source
Lemma rademacher_mean_prod n (k l : 'I_n) : rm (fun s : n.-tuple bool => rademacher (tnth s k) * rademacher (tnth s l)) = (k == l)%:R.
Used by 1 declaration in 1 file
- this file: rademacher_mean_sqr_sum
forall {R : realType} [n : nat] (a : 'I_n -> R), rademacher_mean (fun s : n.-tuple bool => (\sum_(k < n) a k * rademacher (tnth s k)) ^+ 2) = \sum_(k < n) a k ^+ 2
Statement as written in the source
Lemma rademacher_mean_sqr_sum n (a : 'I_n -> R) : rm (fun s : n.-tuple bool => (\sum_(k < n) a k * rademacher (tnth s k)) ^+ 2) = \sum_(k < n) a k ^+ 2.
Used by 1 declaration in 1 file
- this file: rademacher_mean_abs_sum
forall {R : realType} [n : nat] (a : 'I_n -> R), rademacher_mean (fun s : n.-tuple bool => `|\sum_(k < n) a k * rademacher (tnth s k)|) <= Num.ExtraDef.sqrtr (\sum_(k < n) a k ^+ 2)
Main result
Stated in the README together with contraction.
Statement as written in the source
Lemma rademacher_mean_abs_sum n (a : 'I_n -> R) : rm (fun s : n.-tuple bool => `|\sum_(k < n) a k * rademacher (tnth s k)|) <= Num.sqrt (\sum_(k < n) a k ^+ 2).
sectionmax_norm
Context {R : realType}.
Type
forall {R : realType} [m : nat], ('I_m -> R) -> RDefinition
Definition max_norm m (v : 'I_m -> R) : R := \big[Num.max/0]_(j < m) `|v j|.
The norm max_j |v_j| of 'I_m -> R.
Used by 13 declarations in 2 files
- this file: max_norm_ge0, ler_max_norm, max_normD, max_normN, measurable_max_norm, jensen_max_norm, mA, jensen_step, mB, swap_step, symmetrization
- GaussianAnalysis.probability.small_ball_method: small_ball_method, small_ball_linear
forall {R : realType} [m : nat] (v : 'I_m -> R), 0 <= max_norm v
Statement as written in the source
Lemma max_norm_ge0 m (v : 'I_m -> R) : 0 <= max_norm v.
Used by 7 declarations in 2 files
- this file: max_normD, jensen_max_norm, jensen_step, swap_step, symmetrization
- GaussianAnalysis.probability.small_ball_method: small_ball_method, small_ball_linear
forall {R : realType} [m : nat] (v : 'I_m -> R) (j : 'I_m), `|v j| <= max_norm v
Statement as written in the source
Lemma ler_max_norm m (v : 'I_m -> R) j : `|v j| <= max_norm v.
Used by 3 declarations in 2 files
- this file: max_normD, jensen_max_norm
- GaussianAnalysis.probability.small_ball_method: small_ball_method
forall {R : realType} [m : nat] (u v : 'I_m -> R), max_norm (fun j : 'I_m => u j + v j) <= max_norm u + max_norm v
Statement as written in the source
Used by 1 declaration in 1 file
- this file: symmetrization
Statement as written in the source
Used by 1 declaration in 1 file
- this file: symmetrization
sectionmeasurable_max_norm
Context d (U : measurableType d) (R : realType).
forall [d : measure_display] [U : measurableType d] [R : realType] [m : nat] [F : 'I_m -> U -> R], (forall j : 'I_m, measurable_fun [set: U] (F j)) -> measurable_fun [set: U] (fun x : U => \big[maxr/0]_(j < m) F j x)
Statement as written in the source
Lemma measurable_bigmax0 m (F : 'I_m -> U -> R) : (forall j, measurable_fun [set: U] (F j)) -> measurable_fun [set: U] (fun x => \big[Num.max/0]_(j < m) F j x).
Used by 1 declaration in 1 file
- this file: measurable_max_norm
forall [d : measure_display] [U : measurableType d] [R : realType] [m : nat] [F : 'I_m -> U -> R], (forall j : 'I_m, measurable_fun [set: U] (F j)) -> measurable_fun [set: U] (fun x : U => max_norm (F^~ x))
Statement as written in the source
Lemma measurable_max_norm m (F : 'I_m -> U -> R) : (forall j, measurable_fun [set: U] (F j)) -> measurable_fun [set: U] (fun x => max_norm (fun j => F j x)).
Used by 6 declarations in 2 files
- this file: jensen_max_norm, mA, mB, symmetrization
- GaussianAnalysis.probability.small_ball_method: small_ball_method, small_ball_linear
forall [d : measure_display] [U : measurableType d] [R : realType] [P : probability U R] [m : nat] (a : 'I_m -> R) [g : 'I_m -> U -> R], (forall j : 'I_m, P.-integrable [set: U] (EFin \o g j)) -> (forall j : 'I_m, \int[P]_t g j t = 0) -> ((max_norm a)%:E <= \int[P]_t (max_norm (fun j : 'I_m => a j + g j t))%:E)%E
Jensen's inequality for the norm max_j |.|.
Statement as written in the source
Used by 1 declaration in 1 file
- this file: jensen_step
sectionswap_integral
Context d (T : measurableType d) (R : realType). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType] (P : probability T R) [H : T * T -> \bar R], measurable_fun [set: T * T] H -> (forall p : T * T, (0%R <= H p)%E) -> (\int[P]_u \int[P]_t H (t, u))%E = (\int[P]_u \int[P]_t H (u, t))%E
Exchanging two independent variables of the same law.
Statement as written in the source
Lemma ge0_integral_swap (P : probability T R) (H : T * T -> \bar R) : measurable_fun [set: T * T] H -> (forall p, 0 <= H p) -> \int[P]_u \int[P]_t H (t, u) = \int[P]_u \int[P]_t H (u, t).
Used by 1 declaration in 1 file
- this file: swap_step
forall [d : measure_display] [T : measurableType d] [R : realType] (P : measure T R) [n : nat] [F : n.-tuple bool -> T -> R], (forall s : n.-tuple bool, measurable_fun [set: T] (F s)) -> (forall (s : n.-tuple bool) (x : T), 0 <= F s x) -> (\int[P]_x (rademacher_mean (F^~ x))%:E)%E = ((2 ^- n)%:E * (\sum_s (\int[P]_x (F s x)%:E)%E)%R)%E
Statement as written in the source
Lemma ge0_integral_rademacher_mean (P : {measure set T -> \bar R}) n (F : n.-tuple bool -> T -> R) : (forall s, measurable_fun [set: T] (F s)) -> (forall s x, (0 <= F s x)%R) -> \int[P]_x (rademacher_mean (fun s => F s x))%:E = ((2 ^+ n)^-1)%:E * \sum_(s : n.-tuple bool) \int[P]_x (F s x)%:E.
Used by 1 declaration in 1 file
- this file: symmetrization
forall [d : measure_display] [T : measurableType d] [R : realType] [n : nat] [F : n.-tuple bool -> T -> R], (forall s : n.-tuple bool, measurable_fun [set: T] (F s)) -> measurable_fun [set: T] (fun x : T => rademacher_mean (F^~ x))
Statement as written in the source
Lemma measurable_rademacher_mean n (F : n.-tuple bool -> T -> R) : (forall s, measurable_fun [set: T] (F s)) -> measurable_fun [set: T] (fun x => rademacher_mean (fun s => F s x)).
Used by 3 declarations in 2 files
- this file: symmetrization
- GaussianAnalysis.probability.small_ball_method: small_ball_method, small_ball_linear
sectiondoubled_tuple
Context d (T : measurableType d) (R : realType). Local Open Scope ereal_scope. Variables (mu : nat -> probability T R) (n : nat).
Type
forall [d : measure_display] [T : measurableType d] [R : realType], (nat -> probability T R) -> nat -> nat -> probability T R
Definition
Definition doubled_law (i : nat) : probability T R := if (i < n)%N then mu i else mu (i - n).
Two independent copies X, X' of x of law tuple_prod mu n, as the two blocks of a tuple of n + n coordinates.
Used by 10 declarations in 1 file
Type
forall [d : measure_display] [T : measurableType d] [n : nat],
(n + n).-tuple T -> n.-tuple TDefinition
Definition tuple_left (z : (n + n).-tuple T) : n.-tuple T := [tuple tnth z (lshift n k) | k < n].
Used by 3 declarations in 1 file
- this file: measurable_tuple_left, ge0_integral_tuple_left, symmetrization
Type
forall [d : measure_display] [T : measurableType d] [n : nat],
(n + n).-tuple T -> n.-tuple TDefinition
Definition tuple_right (z : (n + n).-tuple T) : n.-tuple T := [tuple tnth z (rshift n k) | k < n].
Used by 3 declarations in 1 file
- this file: measurable_tuple_right, ge0_integral_tuple_right, symmetrization
forall [d : measure_display] [T : measurableType d] [n : nat], measurable_fun [set: (n + n).-tuple T] (tuple_left (n:=n))
Statement as written in the source
Lemma measurable_tuple_left : measurable_fun [set: (n + n).-tuple T] tuple_left.
Used by 2 declarations in 1 file
- this file: ge0_integral_tuple_left, symmetrization
forall [d : measure_display] [T : measurableType d] [n : nat], measurable_fun [set: (n + n).-tuple T] (tuple_right (n:=n))
Statement as written in the source
Lemma measurable_tuple_right : measurable_fun [set: (n + n).-tuple T] tuple_right.
Used by 2 declarations in 1 file
- this file: ge0_integral_tuple_right, symmetrization
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) (n : nat), tuple_prod (doubled_law mu n) n = tuple_prod mu n
Statement as written in the source
Lemma doubled_law_left : tuple_prod doubled_law n = tuple_prod mu n.
Used by 1 declaration in 1 file
- this file: ge0_integral_tuple_left
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) (n : nat), tuple_prod (fun i : nat => doubled_law mu n (n + i)) n = tuple_prod mu n
Statement as written in the source
Lemma doubled_law_right : tuple_prod (fun i => doubled_law (n + i)) n = tuple_prod mu n.
Used by 1 declaration in 1 file
- this file: ge0_integral_tuple_right
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) [n : nat] [G : n.-tuple T -> \bar R], measurable_fun [set: n.-tuple T] G -> (forall x : n.-tuple T, (0%R <= G x)%E) -> (\int[tuple_prod (doubled_law mu n) (n + n)]_z G (tuple_left z))%E = (\int[tuple_prod mu n]_x G x)%E
Statement as written in the source
Lemma ge0_integral_tuple_left (G : n.-tuple T -> \bar R) : measurable_fun [set: n.-tuple T] G -> (forall x, 0 <= G x) -> \int[tuple_prod doubled_law (n + n)]_z G (tuple_left z) = \int[tuple_prod mu n]_x G x.
Used by 1 declaration in 1 file
- this file: symmetrization
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) [n : nat] [G : n.-tuple T -> \bar R], measurable_fun [set: n.-tuple T] G -> (forall x : n.-tuple T, (0%R <= G x)%E) -> (\int[tuple_prod (doubled_law mu n) (n + n)]_z G (tuple_right z))%E = (\int[tuple_prod mu n]_x G x)%E
Statement as written in the source
Lemma ge0_integral_tuple_right (G : n.-tuple T -> \bar R) : measurable_fun [set: n.-tuple T] G -> (forall x, 0 <= G x) -> \int[tuple_prod doubled_law (n + n)]_z G (tuple_right z) = \int[tuple_prod mu n]_x G x.
Used by 1 declaration in 1 file
- this file: symmetrization
sectionsymmetrization
Context d (T : measurableType d) (R : realType). Local Open Scope ereal_scope. Variables (mu : nat -> probability T R) (n m : nat) (f : 'I_m -> T -> R). Hypothesis mf : forall j, measurable_fun [set: T] (f j). Hypothesis fi : forall j k, (mu k).-integrable [set: T] (EFin \o f j).
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) [n : nat] (k : 'I_n), doubled_law mu n (lshift n k) = mu k
Statement as written in the source
Local Lemma nu_left (k : 'I_n) : doubled_law mu n (lshift n k) = mu k.
Used by 1 declaration in 1 file
- this file: fubini_pair
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) [n : nat] (k : 'I_n), doubled_law mu n (rshift n k) = mu k
Statement as written in the source
Local Lemma nu_right (k : 'I_n) : doubled_law mu n (rshift n k) = mu k.
Used by 2 declarations in 1 file
- this file: jensen_step, fubini_pair
forall [d : measure_display] [T : measurableType d] [R : realType] [n m : nat] [f : 'I_m -> T -> R], (forall j : 'I_m, measurable_fun [set: T] (f j)) -> forall (j : 'I_m) (i : 'I_(n + n)), measurable_fun [set: (n + n).-tuple T] (fun z : (n + n).-tuple _ => f j (tnth z i))
Statement as written in the source
Local Lemma mft j (i : 'I_(n + n)) : measurable_fun [set: (n + n).-tuple T] (fun z => f j (tnth z i)).
Used by 3 declarations in 1 file
- this file: mA, mB, symmetrization
Type
forall [d : measure_display] [T : measurableType d] [R : realType], (nat -> probability T R) -> forall [n m : nat], ('I_m -> T -> R) -> nat -> (n + n).-tuple T -> 'I_m -> R
Definition
Local Definition A (p : nat) (z : (n + n).-tuple T) (j : 'I_m) : R := (\sum_(k < n) (f j (tnth z (lshift n k)) - (if (k < p)%N then f j (tnth z (rshift n k)) else \int[mu k]_t f j t)))%R.
The sums with the coordinates k < p of the first block centered by the second block, the others by their means.
Used by 4 declarations in 1 file
- this file: mA, A_set, jensen_step, symmetrization
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) [n m : nat] [f : 'I_m -> T -> R], (forall j : 'I_m, measurable_fun [set: T] (f j)) -> forall p : nat, measurable_fun [set: (n + n).-tuple T] (fun z : (n + n).-tuple _ => (max_norm (symmetrization.A mu f p z))%:E)
Statement as written in the source
Used by 1 declaration in 1 file
- this file: jensen_step
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) [n m : nat] (f : 'I_m -> T -> R) (p : 'I_n) (z : (n + n).-tuple T) (t : T) (j : 'I_m), symmetrization.A mu f p.+1 (tuple_set z (rshift n p) t) j = symmetrization.A mu f p z j + (\int[mu p]_t0 f j t0 - f j t)
Statement as written in the source
Used by 1 declaration in 1 file
- this file: jensen_step
forall [d : measure_display] [T : measurableType d] [R : realType] [mu : nat -> probability T R] [n m : nat] [f : 'I_m -> T -> R], (forall j : 'I_m, measurable_fun [set: T] (f j)) -> (forall (j : 'I_m) (k : nat), (mu k).-integrable [set: T] (EFin \o f j)) -> forall p : 'I_n, (\int[tuple_prod (doubled_law mu n) (n + n)]_z (max_norm (symmetrization.A mu f p z))%:E <= \int[tuple_prod (doubled_law mu n) (n + n)]_z (max_norm (symmetrization.A mu f p.+1 z))%:E)%E
Statement as written in the source
Local Lemma jensen_step (p : 'I_n) : \int[tuple_prod (doubled_law mu n) (n + n)]_z (max_norm (A p z))%:E <= \int[tuple_prod (doubled_law mu n) (n + n)]_z (max_norm (A p.+1 z))%:E.
Used by 1 declaration in 1 file
- this file: symmetrization
Type
forall [d : measure_display] [T : measurableType d] [R : realType] [n m : nat], ('I_m -> T -> R) -> n.-tuple bool -> (n + n).-tuple T -> 'I_m -> R
Definition
Local Definition B (s : n.-tuple bool) (z : (n + n).-tuple T) (j : 'I_m) : R := (\sum_(k < n) rademacher (tnth s k) * (f j (tnth z (lshift n k)) - f j (tnth z (rshift n k))))%R.
The sums of the differences with signs.
Used by 4 declarations in 1 file
- this file: mB, B_set, swap_step, symmetrization
forall [d : measure_display] [T : measurableType d] [R : realType] [n m : nat] [f : 'I_m -> T -> R], (forall j : 'I_m, measurable_fun [set: T] (f j)) -> forall s : n.-tuple bool, measurable_fun [set: (n + n).-tuple T] (fun z : (n + n).-tuple _ => (max_norm (symmetrization.B f s z))%:E)
Statement as written in the source
Used by 1 declaration in 1 file
- this file: swap_step
forall [d : measure_display] [T : measurableType d] [R : realType] [n m : nat] (f : 'I_m -> T -> R) (s : n.-tuple bool) (q : 'I_n) (z : (n + n).-tuple T) (t u : T) (j : 'I_m), symmetrization.B f (sign_flip q s) (tuple_set (tuple_set z (rshift n q) u) (lshift n q) t) j = symmetrization.B f s (tuple_set (tuple_set z (rshift n q) t) (lshift n q) u) j
Statement as written in the source
Used by 1 declaration in 1 file
- this file: swap_step
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) [n : nat] (q : 'I_n) [F : (n + n).-tuple T -> \bar R], measurable_fun [set: (n + n).-tuple T] F -> (forall z : (n + n).-tuple T, (0%R <= F z)%E) -> (\int[tuple_prod (doubled_law mu n) (n + n)]_z F z)%E = (\int[tuple_prod (doubled_law mu n) (n + n)]_z \int[mu q]_u \int[mu q]_t F (tuple_set (tuple_set z (rshift n q) u) (lshift n q) t))%E
Statement as written in the source
Local Lemma fubini_pair (q : 'I_n) (F : (n + n).-tuple T -> \bar R) : measurable_fun [set: (n + n).-tuple T] F -> (forall z, 0 <= F z) -> \int[tuple_prod (doubled_law mu n) (n + n)]_z F z = \int[tuple_prod (doubled_law mu n) (n + n)]_z \int[mu q]_u \int[mu q]_t F (tuple_set (tuple_set z (rshift n q) u) (lshift n q) t).
Used by 1 declaration in 1 file
- this file: swap_step
forall [d : measure_display] [T : measurableType d] [R : realType] (mu : nat -> probability T R) [n m : nat] [f : 'I_m -> T -> R], (forall j : 'I_m, measurable_fun [set: T] (f j)) -> forall (s : n.-tuple bool) (q : 'I_n), (\int[tuple_prod (doubled_law mu n) (n + n)]_z (max_norm (symmetrization.B f (sign_flip q s) z))%:E)%E = (\int[tuple_prod (doubled_law mu n) (n + n)]_z (max_norm (symmetrization.B f s z))%:E)%E
Statement as written in the source
Local Lemma swap_step s (q : 'I_n) : \int[tuple_prod (doubled_law mu n) (n + n)]_z (max_norm (B (sign_flip q s) z))%:E = \int[tuple_prod (doubled_law mu n) (n + n)]_z (max_norm (B s z))%:E.
Used by 1 declaration in 1 file
- this file: symmetrization
forall [d : measure_display] [T : measurableType d] [R : realType] [mu : nat -> probability T R] (n : nat) [m : nat] [f : 'I_m -> T -> R], (forall j : 'I_m, measurable_fun [set: T] (f j)) -> (forall (j : 'I_m) (k : nat), (mu k).-integrable [set: T] (EFin \o f j)) -> (\int[tuple_prod mu n]_x (max_norm (fun j : 'I_m => \sum_(k < n) (f j (tnth x k) - \int[mu k]_t f j t)))%:E <= 2 * \int[tuple_prod mu n]_x (rademacher_mean (fun s : n.-tuple bool => max_norm (fun j : 'I_m => \sum_(k < n) rademacher (tnth s k) * f j (tnth x k))))%:E)%E
Main result, as the README states it
Gine-Zinn symmetrization: for x of law tuple_prod mu n and a finite class of measurable f_j integrable for every mu k, E max_j |sum_k (f_j(x_k) - E f_j(x_k))| <= 2 E rademacher_mean (max_j |sum_k eps_k f_j(x_k)|), as integrals in [0, +oo].
Statement as written in the source
Theorem symmetrization : \int[tuple_prod mu n]_x (max_norm (fun j => \sum_(k < n) (f j (tnth x k) - \int[mu k]_t f j t)))%:E <= 2%:E * \int[tuple_prod mu n]_x (rademacher_mean (fun s : n.-tuple bool => max_norm (fun j => \sum_(k < n) rademacher (tnth s k) * f j (tnth x k))))%:E.
Used by 1 declaration in 1 file
- GaussianAnalysis.probability.small_ball_method: small_ball_method