GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisfourieresseen

Esseen's inequality and the concentration of sums

GaussianAnalysis.fourier.esseenlibrary/fourier/esseen.v1,097 lines30 lemmas and theorems, 2 definitionssource
Imports 3 library modules and 31 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.archimedean, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_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.derive, mathcomp.analysis.realfun, mathcomp.analysis.convex, mathcomp.analysis.exp, mathcomp.analysis.trigo, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.numfun, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.ftc, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.gauss_integral

Imported by 3
Required by 2 files of the paper proofs

The Levy concentration function Q(mu, L) = sup_a mu [a, a + L] of a law mu on the real line (conc_fun) is at most one, nondecreasing in L, satisfies Q(mu, L) <= (L / L' + 1) Q(mu, L') (conc_fun_cover), and does not increase when an independent variable is added (conc_fun_add).

Esseen's inequality bounds it by the characteristic function:

Q(mu, 2 pi / T) <= pi^2 / (4 T) \int_{-T}^T |cf mu t| dt    (esseen)
                 = pi^2 / (2 T) \int_0^T |cf mu t| dt       (esseen0),

through the Fejer kernel 2 \int_0^T (1 - t / T) cos (t z) dt = 2 (1 - cos (T z)) / (T z^2) (fejerE), which is at least 4 T / pi^2 for |z| <= pi / T by Jordan's inequality (jordan_sin, jordan_cos).

For independent X_1, ..., X_n of laws mu_k with E[X_k^2] <= v and Q(mu_k, lambda) <= 1 - eps, the law of S = X_1 + ... + X_n satisfies

Q(S, L) <= 2 pi^2 sqrt pi (L + sqrt (v / eps)) / (lambda sqrt (eps n))

(conc_fun_sum). The proof goes through the symmetrization X - X', for which P(|X - X'| < lambda / 2) <= Q(mu, lambda) (sym_small_ball) and 1 - |cf mu t|^2 >= lambda^2 eps t^2 / (4 pi^2) for small |t| (sym_cf_bound).

Laws on the line are probabilities on measurableTypeR R, as in charfun.v.

conc_fun mu Lsup_a mu [a, a + L], the Levy concentration function
fejer T z\int_0^T (1 - t / T) cos (t z) dt, half the Fejer kernel

Main results

ResultsStatement
conc_funconc_fun_ge0conc_fun_le1le_conc_funconc_fun_ubconc_fun_leconc_fun_cover
The Levy concentration function Q(mu, L) = sup_a mu [a, a + L] of a law on the line: between 0 and 1, nondecreasing in L, and Q(mu, L) <= (L / L' + 1) Q(mu, L') for 0 <= L and 0 < L'.
conc_fun_add
Adding an independent variable does not increase the concentration function: if nu is the law of g X + e Y for X of law P independent of Y of law mu and e != 0, then Q(nu, |e| L) <= Q(mu, L).
jordan_sinjordan_cos
Jordan's inequality 2 x / pi <= sin x on [0, pi / 2], hence 1 - cos u >= 2 u^2 / pi^2 for |u| <= pi.
fejerfejerEfejer0fejer_ge0fejer_ge
The integral of the triangle kernel: \int_0^T (1 - t / T) cos (t z) dt = (1 - cos (T z)) / (T z^2) (T / 2 at z = 0); it is nonnegative, and at least 2 T / pi^2 for |z| <= pi / T.
esseenesseen0
Esseen's inequality: for every law mu on the line and T > 0, Q(mu, 2 pi / T) <= pi^2 / (4 T) \int_{-T}^T |cf mu t| dt = pi^2 / (2 T) \int_0^T |cf mu t| dt.
conc_fun_sum
Concentration of sums: for independent X_1, ..., X_n (n >= 1, laws mu_k, tuple_prod) with E[X_k^2] <= v and Q(mu_k, lambda) <= 1 - eps, the law of X_1 + ... + X_n satisfies Q(S, L) <= 2 pi^2 sqrt pi (L + sqrt (v / eps)) / (lambda sqrt (eps n)) for L >= 0.
sym_small_ballsym_second_momentsym_second_moment_centersym_tailcf_norm_sqr_symsym_cf_boundsym_cf_bound_expR
Symmetrization, for X, X' independent of law mu (on mu \x mu): P(|X - X'| < lambda / 2) <= Q(mu, lambda), E[(X - X')^2] <= 4 E[(X - a)^2] for every a, Markov's tail bound, |cf mu t|^2 = E[cos (t (X - X'))], and, if Q(mu, lambda) <= 1 - eps, E[X^2] <= v and 8 v <= eps r^2, then |cf mu t|^2 <= 1 - lambda^2 eps t^2 / (4 pi^2) for |t| <= pi / r.
Rintegral_fubinimeasurable_Rintegral1measurable_Rintegral2
Fubini for real integrals against a probability and a sigma-finite measure, for a measurable function dominated by an integrable function of the second variable; both partial integrals are measurable.
Rintegral_FTCRintegral_evenintegral_gauss_half_le
The fundamental theorem of calculus for an antiderivative on the whole line; \int_{-T}^T f = 2 \int_0^T f for f even and continuous; \int_0^T exp (- (c t)^2) dt <= sqrt pi / (2 c).

Declarations32 exported, 13 local

lemma, theoremdefinitioninstancelocal
sectionjordan
Context {R : realType}.
lemma jordan_sin main result source, line 58 
forall {R : realType} [x : R], 0 <= x <= pi / 2 -> 2 / pi * x <= sin x

Jordan's inequality: sin is above its chord on [0, pi / 2].

Main result, as the README states it

Jordan's inequality 2 x / pi <= sin x on [0, pi / 2], hence 1 - cos u >= 2 u^2 / pi^2 for |u| <= pi.

Statement as written in the source
Lemma jordan_sin (x : R) : 0 <= x <= pi / 2 -> 2 / pi * x <= sin x.
Used by 1 declaration in 1 file
lemma jordan_cos main result source, line 93 
forall {R : realType} [u : R], `|u| <= pi -> 2 / pi ^+ 2 * u ^+ 2 <= 1 - cos u

Hence 1 - cos u >= 2 u^2 / pi^2 for |u| <= pi.

Main result

Stated in the README together with jordan_sin.

Statement as written in the source
Lemma jordan_cos (u : R) : `|u| <= pi -> 2 / pi ^+ 2 * u ^+ 2 <= 1 - cos u.
Used by 2 declarations in 1 file
sectionfejer
Context {R : realType}.
Local Notation mu := (@lebesgue_measure R).
lemma Rintegral_FTC main result source, line 123 
forall {R : realType} [f F : R -> R] [a b : R],
a < b ->
continuous f ->
(forall x : R, is_derive x 1 F (f x)) ->
\int[lebesgue_measure]_(x in `[a, b]) f x = F b - F a

The fundamental theorem of calculus, for an antiderivative on R.

Main result, as the README states it

The fundamental theorem of calculus for an antiderivative on the whole line; \int_{-T}^T f = 2 \int_0^T f for f even and continuous; \int_0^T exp (- (c t)^2) dt <= sqrt pi / (2 c).

Statement as written in the source
Lemma Rintegral_FTC (f F : R -> R) (a b : R) : a < b -> continuous f ->
  (forall x : R, is_derive x 1 F (f x)) ->
  \int[mu]_(x in `[a, b]) f x = F b - F a.
Used by 2 declarations in 1 file
definition fejer main result source, line 145
Type
forall {R : realType}, R -> R -> R
Definition
Definition fejer (T z : R) : R :=
  \int[mu]_(t in `[0, T]) ((1 - t / T) * cos (t * z)).

The Fejer kernel, without its factor 2: the integral over [0, T] of the triangle function 1 - t / T against cos (t z).

Main result, as the README states it

The integral of the triangle kernel: \int_0^T (1 - t / T) cos (t z) dt = (1 - cos (T z)) / (T z^2) (T / 2 at z = 0); it is nonnegative, and at least 2 T / pi^2 for |z| <= pi / T.

Used by 5 declarations in 1 file
let is_derive_triangle section-local source, line 148 
Let is_derive_triangle (T t : R) :
  is_derive t 1 (fun s : R => 1 - s / T) (- T^-1).
Used by 2 declarations in 1 file
let continuous_fejer_integrand section-local source, line 155 
Let continuous_fejer_integrand (T z : R) :
  continuous (fun t : R => (1 - t / T) * cos (t * z)).
Used by 2 declarations in 1 file
lemma fejerE main result source, line 163 
forall {R : realType} [T z : R],
0 < T -> z != 0 -> fejer T z = (1 - cos (T * z)) / (T * z ^+ 2)
Main result

Stated in the README together with fejer.

Statement as written in the source
Lemma fejerE (T z : R) : 0 < T -> z != 0 ->
  fejer T z = (1 - cos (T * z)) / (T * z ^+ 2).
Used by 2 declarations in 1 file
lemma fejer0 main result source, line 185 
forall {R : realType} [T : R], 0 < T -> fejer T 0 = T / 2
Main result

Stated in the README together with fejer.

Statement as written in the source
Lemma fejer0 (T : R) : 0 < T -> fejer T 0 = T / 2.
Used by 2 declarations in 1 file
sectionfejer_bounds
Context {R : realType}.
lemma fejer_ge0 main result source, line 204 
forall {R : realType} [T : R] (z : R), 0 < T -> 0 <= fejer T z
Main result

Stated in the README together with fejer.

Statement as written in the source
Lemma fejer_ge0 (T z : R) : 0 < T -> 0 <= fejer T z.
Used by 1 declaration in 1 file
lemma fejer_ge main result source, line 211 
forall {R : realType} [T z : R], 0 < T -> `|z| <= pi / T -> 2 * T / pi ^+ 2 <= fejer T z
Main result

Stated in the README together with fejer.

Statement as written in the source
Lemma fejer_ge (T z : R) : 0 < T -> `|z| <= pi / T ->
  2 * T / pi ^+ 2 <= fejer T z.
Used by 1 declaration in 1 file
sectionconc_fun
Context {R : realType}.
Implicit Types (mu nu : probability (measurableTypeR R) R) (L a : R).
definition conc_fun main result source, line 238
Type
forall {R : realType}, probability (measurableTypeR R) R -> R -> R
Definition
Definition conc_fun mu L : R :=
  sup [set fine (mu `[a, a + L]%classic) | a in [set: R]].
Main result, as the README states it

The Levy concentration function Q(mu, L) = sup_a mu [a, a + L] of a law on the line: between 0 and 1, nondecreasing in L, and Q(mu, L) <= (L / L' + 1) Q(mu, L') for 0 <= L and 0 < L'.

Used by 27 declarations in 3 files
let prob_fin section-local source, line 241 
Let prob_fin mu (A : set (measurableTypeR R)) :
  measurable A -> mu A \is a fin_num.
Used by 3 declarations in 1 file
let has_sup_conc section-local source, line 248 
Let has_sup_conc mu L :
  has_sup [set fine (mu `[a, a + L]%classic) | a in [set: R]].
Used by 1 declaration in 1 file
lemma conc_fun_ub main result source, line 256 
forall {R : realType} (mu : probability (measurableTypeR R) R) (L a : R),
fine (mu `[a, a + L]%classic) <= conc_fun mu L
Main result

Stated in the README together with conc_fun.

Statement as written in the source
Lemma conc_fun_ub mu L a : fine (mu `[a, a + L]%classic) <= conc_fun mu L.
Used by 3 declarations in 2 files
lemma conc_fun_ubE source, line 259 
forall {R : realType} (mu : probability (measurableTypeR R) R) (L a : R),
(mu `[a, (a + L)%R]%classic <= (conc_fun mu L)%:E)%E
Statement as written in the source
Lemma conc_fun_ubE mu L a :
  (mu `[a, (a + L)%R]%classic <= (conc_fun mu L)%:E)%E.
Used by 4 declarations in 1 file
lemma conc_fun_le main result source, line 265 
forall {R : realType} [mu : probability (measurableTypeR R) R] [L c : R],
(forall a : R, (mu `[a, (a + L)%R]%classic <= c%:E)%E) -> conc_fun mu L <= c
Main result

Stated in the README together with conc_fun.

Statement as written in the source
Lemma conc_fun_le mu L c :
  (forall a, mu `[a, (a + L)%R]%classic <= c%:E)%E -> conc_fun mu L <= c.
Used by 6 declarations in 2 files
lemma conc_fun_ge0 main result source, line 272 
forall {R : realType} (mu : probability (measurableTypeR R) R) (L : R), 0 <= conc_fun mu L
Main result

Stated in the README together with conc_fun.

Statement as written in the source
Lemma conc_fun_ge0 mu L : 0 <= conc_fun mu L.
Used by 1 declaration in 1 file
lemma conc_fun_le1 main result source, line 275 
forall {R : realType} (mu : probability (measurableTypeR R) R) (L : R), conc_fun mu L <= 1
Main result

Stated in the README together with conc_fun.

Statement as written in the source
Lemma conc_fun_le1 mu L : conc_fun mu L <= 1.
lemma le_conc_fun main result source, line 278 
forall {R : realType} (mu : probability (measurableTypeR R) R) [L1 L2 : R],
L1 <= L2 -> conc_fun mu L1 <= conc_fun mu L2
Main result

Stated in the README together with conc_fun.

Statement as written in the source
Lemma le_conc_fun mu L1 L2 : L1 <= L2 -> conc_fun mu L1 <= conc_fun mu L2.
lemma conc_fun_cover main result source, line 286 
forall {R : realType} (mu : probability (measurableTypeR R) R) [L L' : R],
0 <= L -> 0 < L' -> conc_fun mu L <= (L / L' + 1) * conc_fun mu L'

An interval of length L is covered by L / L' + 1 intervals of length L'.

Main result

Stated in the README together with conc_fun.

Statement as written in the source
Lemma conc_fun_cover mu L L' : 0 <= L -> 0 < L' ->
  conc_fun mu L <= (L / L' + 1) * conc_fun mu L'.
Used by 1 declaration in 1 file
lemma conc_fun_add main result source, line 321 
forall {R : realType} [d : measure_display] [T : measurableType d] 
  [P : probability T R] [g : T -> R] [mu nu : probability (measurableTypeR R) R] 
  [e : R] (L : R),
measurable_fun [set: T] g ->
e != 0 ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 (P \x mu)%E ((fun p : T * R => g p.1 + e * p.2) @^-1` A) = nu A) ->
conc_fun nu (`|e| * L) <= conc_fun mu L

Adding an independent variable does not increase the concentration function: if nu is the law of g X + e Y for X of law P independent of Y of law mu, then Q(nu, |e| L) <= Q(mu, L).

Main result, as the README states it

Adding an independent variable does not increase the concentration function: if nu is the law of g X + e Y for X of law P independent of Y of law mu and e != 0, then Q(nu, |e| L) <= Q(mu, L).

Statement as written in the source
Lemma conc_fun_add d (T : measurableType d) (P : probability T R)
    (g : T -> R) mu nu (e L : R) :
  measurable_fun [set: T] g -> e != 0 ->
  (forall A : set (measurableTypeR R), measurable A ->
     (P \x mu)%E ((fun p => g p.1 + e * p.2) @^-1` A) = nu A) ->
  conc_fun nu (`|e| * L) <= conc_fun mu L.
Used by 1 declaration in 1 file

Fubini's theorem for real integrals against a probability and a sigma-finite measure, for a measurable function dominated by an integrable function of the second variable.

sectionfubini_dominated
Context {R : realType} d1 d2 (T1 : measurableType d1) (T2 : measurableType d2).
Variables (P : probability T1 R) (m : {sigma_finite_measure set T2 -> \bar R}).
Variables (F : T1 * T2 -> R) (g : T2 -> R).
Hypotheses (mF : measurable_fun [set: T1 * T2] F)
  (ig : m.-integrable [set: T2] (EFin \o g))
  (Fg : forall x y, `|F (x, y)| <= g y).
let mFx section-local source, line 370 
Let mFx x : measurable_fun [set: T2] (fun y => F (x, y)).
let mFy section-local source, line 373 
Let mFy y : measurable_fun [set: T1] (fun x => F (x, y)).
Used by 1 declaration in 1 file
  • this file: iFy
let iFx section-local source, line 376 
Let iFx x : m.-integrable [set: T2] (EFin \o (fun y => F (x, y))).
Used by 1 declaration in 1 file
let iFy section-local source, line 382 
Let iFy y : P.-integrable [set: T1] (EFin \o (fun x => F (x, y))).
Used by 1 declaration in 1 file
let iF section-local source, line 385 
Let iF : (P \x m)%E.-integrable [set: T1 * T2] (EFin \o F).
Used by 3 declarations in 1 file
lemma Rintegral_fubini main result source, line 402 
forall {R : realType} [d1 d2 : measure_display] [T1 : measurableType d1]
  [T2 : measurableType d2] (P : probability T1 R)
  [m : {sigma_finite_measure set T2 -> \bar R}] [F : T1 * T2 -> R] 
  [g : T2 -> R],
measurable_fun [set: T1 * T2] F ->
m.-integrable [set: T2] (EFin \o g) ->
(forall (x : T1) (y : T2), `|F (x, y)| <= g y) ->
\int[P]_x \int[m]_y F (x, y) = \int[m]_y \int[P]_x F (x, y)
Main result, as the README states it

Fubini for real integrals against a probability and a sigma-finite measure, for a measurable function dominated by an integrable function of the second variable; both partial integrals are measurable.

Statement as written in the source
Lemma Rintegral_fubini :
  \int[P]_x \int[m]_y F (x, y) = \int[m]_y \int[P]_x F (x, y).
Used by 4 declarations in 3 files
lemma measurable_Rintegral1 main result source, line 413 
forall {R : realType} [d1 d2 : measure_display] [T1 : measurableType d1]
  [T2 : measurableType d2],
probability T1 R ->
forall [m : {sigma_finite_measure set T2 -> \bar R}] [F : T1 * T2 -> R] [g : T2 -> R],
measurable_fun [set: T1 * T2] F ->
m.-integrable [set: T2] (EFin \o g) ->
(forall (x : T1) (y : T2), `|F (x, y)| <= g y) ->
measurable_fun [set: T1] (fun x : T1 => \int[m]_y F (x, y))
Main result

Stated in the README together with Rintegral_fubini.

Statement as written in the source
Lemma measurable_Rintegral1 :
  measurable_fun [set: T1] (fun x => \int[m]_y F (x, y)).
Used by 5 declarations in 3 files
lemma measurable_Rintegral2 main result source, line 420 
forall {R : realType} [d1 d2 : measure_display] [T1 : measurableType d1]
  [T2 : measurableType d2] (P : probability T1 R)
  [m : {sigma_finite_measure set T2 -> \bar R}] [F : T1 * T2 -> R] 
  [g : T2 -> R],
measurable_fun [set: T1 * T2] F ->
m.-integrable [set: T2] (EFin \o g) ->
(forall (x : T1) (y : T2), `|F (x, y)| <= g y) ->
measurable_fun [set: T2] (fun y : T2 => \int[P]_x F (x, y))
Main result

Stated in the README together with Rintegral_fubini.

Statement as written in the source
Lemma measurable_Rintegral2 :
  measurable_fun [set: T2] (fun y => \int[P]_x F (x, y)).
Used by 2 declarations in 2 files
sectionesseen
Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
Implicit Types (mu : probability (measurableTypeR R) R).
theorem esseen0 main result source, line 435 
forall {R : realType} (mu : probability (measurableTypeR R) R) [T : R],
0 < T ->
conc_fun mu (2 * pi / T) <=
pi ^+ 2 / (2 * T) * \int[lebesgue_measure]_(t in `[0, T]) cf_norm mu t

Esseen's inequality, with the integral over [0, T].

Main result

Stated in the README together with esseen.

Statement as written in the source
Theorem esseen0 mu (T : R) : 0 < T ->
  conc_fun mu (2 * pi / T) <=
  pi ^+ 2 / (2 * T) * \int[leb]_(t in `[0, T]) cf_norm mu t.
Used by 2 declarations in 1 file
lemma Rintegral_even main result source, line 582 
forall {R : realType} [f : R -> R] [T : R],
0 < T ->
continuous f ->
(forall t : R, f (- t) = f t) ->
\int[lebesgue_measure]_(t in `[- T, T]) f t = 2 * \int[lebesgue_measure]_(t in `[0, T]) f t

The integral over [- T, T] of an even continuous function.

Main result

Stated in the README together with Rintegral_FTC.

Statement as written in the source
Lemma Rintegral_even (f : R -> R) (T : R) : 0 < T -> continuous f ->
  (forall t, f (- t) = f t) ->
  \int[leb]_(t in `[- T, T]) f t = 2 * \int[leb]_(t in `[0, T]) f t.
Used by 1 declaration in 1 file
theorem esseen main result source, line 612 
forall {R : realType} (mu : probability (measurableTypeR R) R) [T : R],
0 < T ->
conc_fun mu (2 * pi / T) <=
pi ^+ 2 / (4 * T) * \int[lebesgue_measure]_(t in `[- T, T]) cf_norm mu t

Esseen's inequality: for every law mu and T > 0, Q(mu, 2 pi / T) <= pi^2 / (4 T) \int_{-T}^{T} |cf mu t| dt.

Main result, as the README states it

Esseen's inequality: for every law mu on the line and T > 0, Q(mu, 2 pi / T) <= pi^2 / (4 T) \int_{-T}^T |cf mu t| dt = pi^2 / (2 T) \int_0^T |cf mu t| dt.

Statement as written in the source
Theorem esseen mu (T : R) : 0 < T ->
  conc_fun mu (2 * pi / T) <=
  pi ^+ 2 / (4 * T) * \int[leb]_(t in `[- T, T]) cf_norm mu t.

The symmetrization X - X' of a law mu, on the product space mu \x mu.

sectionsymmetrization
Context {R : realType} (mu : probability (measurableTypeR R) R).
Local Notation PP := (mu \x mu)%E.
let mdiff section-local source, line 630 
Let mdiff : measurable_fun [set: measurableTypeR R * measurableTypeR R]
    (fun p => p.1 - p.2 : R).
Used by 6 declarations in 1 file
lemma sym_small_ball main result source, line 639 
forall {R : realType} (mu : probability (measurableTypeR R) R) (lambda : R),
((mu \x mu) [set p | (`|p.1 - p.2| < lambda / 2)%R] <= (conc_fun mu lambda)%:E)%E

P(|X - X'| < lambda / 2) <= Q(mu, lambda).

Main result, as the README states it

Symmetrization, for X, X' independent of law mu (on mu \x mu): P(|X - X'| < lambda / 2) <= Q(mu, lambda), E[(X - X')^2] <= 4 E[(X - a)^2] for every a, Markov's tail bound, |cf mu t|^2 = E[cos (t (X - X'))], and, if Q(mu, lambda) <= 1 - eps, E[X^2] <= v and 8 v <= eps r^2, then |cf mu t|^2 <= 1 - lambda^2 eps t^2 / (4 pi^2) for |t| <= pi / r.

Statement as written in the source
Lemma sym_small_ball (lambda : R) :
  (PP [set p | (`|p.1 - p.2| < lambda / 2)%R] <= (conc_fun mu lambda)%:E)%E.
Used by 1 declaration in 1 file
lemma sym_second_moment_center main result source, line 664 
forall {R : realType} [mu : probability (measurableTypeR R) R] [a v : R],
(\int[mu]_x (((x : R) - a) ^+ 2)%:E <= v%:E)%E ->
(\int[mu \x mu]_p ((p.1 - p.2) ^+ 2)%:E <= (4 * v)%:E)%E

The second moment of X - X' is at most 4 v.

E[(X - X')^2] <= 4 E[(X - a)^2] for every a.

Main result

Stated in the README together with sym_small_ball.

Statement as written in the source
Lemma sym_second_moment_center (a v : R) :
  (\int[mu]_x ((((x : R) - a) ^+ 2)%R)%:E <= v%:E)%E ->
  (\int[PP]_p (((p.1 - p.2) ^+ 2)%R)%:E <= (4 * v)%:E)%E.
Used by 2 declarations in 2 files
lemma sym_second_moment main result source, line 715 
forall {R : realType} [mu : probability (measurableTypeR R) R] [v : R],
(\int[mu]_x (x ^+ 2)%:E <= v%:E)%E ->
(\int[mu \x mu]_p ((p.1 - p.2) ^+ 2)%:E <= (4 * v)%:E)%E
Main result

Stated in the README together with sym_small_ball.

Statement as written in the source
Lemma sym_second_moment (v : R) :
  (\int[mu]_x ((x ^+ 2)%R)%:E <= v%:E)%E ->
  (\int[PP]_p (((p.1 - p.2) ^+ 2)%R)%:E <= (4 * v)%:E)%E.
Used by 2 declarations in 2 files
lemma sym_tail main result source, line 724 
forall {R : realType} [mu : probability (measurableTypeR R) R] [v r : R],
0 < r ->
(\int[mu]_x (x ^+ 2)%:E <= v%:E)%E ->
((mu \x mu) [set p | (r < `|p.1 - p.2|)%R] <= (4 * v / r ^+ 2)%:E)%E

Markov's inequality for X - X'.

Main result

Stated in the README together with sym_small_ball.

Statement as written in the source
Lemma sym_tail (v r : R) : 0 < r ->
  (\int[mu]_x ((x ^+ 2)%R)%:E <= v%:E)%E ->
  (PP [set p | (r < `|p.1 - p.2|)%R] <= (4 * v / r ^+ 2)%:E)%E.
Used by 1 declaration in 1 file
let msmall section-local source, line 761 
Let msmall (a : R) :
  measurable [set p : measurableTypeR R * measurableTypeR R |
    (`|p.1 - p.2| < a)%R].
Used by 1 declaration in 1 file
let mlarge section-local source, line 771 
Let mlarge (a : R) :
  measurable [set p : measurableTypeR R * measurableTypeR R |
    (a < `|p.1 - p.2|)%R].
Used by 1 declaration in 1 file
let PPfin section-local source, line 784 
Let PPfin (A : set (measurableTypeR R * measurableTypeR R)) :
  measurable A -> PP A = (fine (PP A))%:E.
Used by 1 declaration in 1 file
lemma cf_norm_sqr_sym main result source, line 792 
forall {R : realType} (mu : probability (measurableTypeR R) R) (t : R),
cf_norm mu t ^+ 2 = \int[(mu \x mu)%E]_p cos (t * (p.1 - p.2))

|cf mu t|^2 is the characteristic function of X - X' at t.

Main result

Stated in the README together with sym_small_ball.

Statement as written in the source
Lemma cf_norm_sqr_sym (t : R) :
  cf_norm mu t ^+ 2 = \int[PP]_p cos (t * (p.1 - p.2)).
Used by 1 declaration in 1 file
lemma sym_cf_bound main result source, line 810 
forall {R : realType} [mu : probability (measurableTypeR R) R] [v lambda eps r t : R],
0 < lambda ->
0 < eps ->
0 < r ->
conc_fun mu lambda <= 1 - eps ->
(\int[mu]_x (x ^+ 2)%:E <= v%:E)%E ->
8 * v <= eps * r ^+ 2 ->
`|t| <= pi / r -> cf_norm mu t ^+ 2 <= 1 - lambda ^+ 2 * eps / (4 * pi ^+ 2) * t ^+ 2

The bound behind the inequality for sums: if Q(mu, lambda) <= 1 - eps and E[X^2] <= v, then 1 - |cf mu t|^2 >= lambda^2 eps t^2 / (4 pi^2) for |t| <= pi / r, as soon as 8 v <= eps r^2.

Main result

Stated in the README together with sym_small_ball.

Statement as written in the source
Lemma sym_cf_bound (v lambda eps r t : R) :
  0 < lambda -> 0 < eps -> 0 < r ->
  conc_fun mu lambda <= 1 - eps ->
  (\int[mu]_x ((x ^+ 2)%R)%:E <= v%:E)%E -> 8 * v <= eps * r ^+ 2 ->
  `|t| <= pi / r ->
  cf_norm mu t ^+ 2 <= 1 - lambda ^+ 2 * eps / (4 * pi ^+ 2) * t ^+ 2.
Used by 1 declaration in 1 file
lemma sym_cf_bound_expR main result source, line 901 
forall {R : realType} [mu : probability (measurableTypeR R) R] [v lambda eps r t : R],
0 < lambda ->
0 < eps ->
0 < r ->
conc_fun mu lambda <= 1 - eps ->
(\int[mu]_x (x ^+ 2)%:E <= v%:E)%E ->
8 * v <= eps * r ^+ 2 ->
`|t| <= pi / r -> cf_norm mu t <= expR (- (lambda ^+ 2 * eps / (8 * pi ^+ 2)) * t ^+ 2)
Main result

Stated in the README together with sym_small_ball.

Statement as written in the source
Lemma sym_cf_bound_expR (v lambda eps r t : R) :
  0 < lambda -> 0 < eps -> 0 < r ->
  conc_fun mu lambda <= 1 - eps ->
  (\int[mu]_x ((x ^+ 2)%R)%:E <= v%:E)%E -> 8 * v <= eps * r ^+ 2 ->
  `|t| <= pi / r ->
  cf_norm mu t <= expR (- (lambda ^+ 2 * eps / (8 * pi ^+ 2)) * t ^+ 2).
Used by 1 declaration in 1 file
sectiongauss_half_line
Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
lemma integral_gauss_half_le main result source, line 929 
forall {R : realType} [c T : R],
0 < c ->
0 < T ->
\int[lebesgue_measure]_(t in `[0, T]) expR (- (c * t) ^+ 2) <=
Num.ExtraDef.sqrtr pi / (2 * c)

The integral of exp (- (c t)^2) over [0, T] is at most sqrt pi / (2 c).

Main result

Stated in the README together with Rintegral_FTC.

Statement as written in the source
Lemma integral_gauss_half_le (c T : R) : 0 < c -> 0 < T ->
  \int[leb]_(t in `[0, T]) expR (- (c * t) ^+ 2) <= Num.sqrt pi / (2 * c).
Used by 1 declaration in 1 file

The inequality for sums of independent variables under a second moment condition (Kolmogorov-Rogozin type).

sectionconc_fun_sum
Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
theorem conc_fun_sum main result source, line 987 
forall {R : realType} [mu : nat -> probability (measurableTypeR R) R] 
  [n : nat] [nu : probability (measurableTypeR R) R] [v lambda eps L : R],
(0 < n)%N ->
0 < v ->
0 < lambda ->
0 < eps ->
0 <= L ->
(forall k : nat, (k < n)%N -> (\int[mu k]_x (x ^+ 2)%:E <= v%:E)%E) ->
(forall k : nat, (k < n)%N -> conc_fun (mu k) lambda <= 1 - eps) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 tuple_prod mu n ((fun x : n.-tuple R => \sum_(k < n) tnth x k) @^-1` A) = nu A) ->
conc_fun nu L <=
2 * pi ^+ 2 * Num.ExtraDef.sqrtr pi * (L + Num.ExtraDef.sqrtr (v / eps)) /
(lambda * Num.ExtraDef.sqrtr (eps * n%:R))
Main result, as the README states it

Concentration of sums: for independent X_1, ..., X_n (n >= 1, laws mu_k, tuple_prod) with E[X_k^2] <= v and Q(mu_k, lambda) <= 1 - eps, the law of X_1 + ... + X_n satisfies Q(S, L) <= 2 pi^2 sqrt pi (L + sqrt (v / eps)) / (lambda sqrt (eps n)) for L >= 0.

Statement as written in the source
Theorem conc_fun_sum (mu : nat -> probability (measurableTypeR R) R) (n : nat)
    (nu : probability (measurableTypeR R) R) (v lambda eps L : R) :
  (0 < n)%N -> 0 < v -> 0 < lambda -> 0 < eps -> 0 <= L ->
  (forall k, (k < n)%N -> (\int[mu k]_x ((x ^+ 2)%R)%:E <= v%:E)%E) ->
  (forall k, (k < n)%N -> conc_fun (mu k) lambda <= 1 - eps) ->
  (forall A : set (measurableTypeR R), measurable A ->
     tuple_prod mu n ((fun x => \sum_(k < n) tnth x k) @^-1` A) = nu A) ->
  conc_fun nu L <= 2 * pi ^+ 2 * Num.sqrt pi * (L + Num.sqrt (v / eps)) /
    (lambda * Num.sqrt (eps * n%:R)).
Used by 1 declaration in 1 file
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.