GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisfouriergauss_factor

Gaussian factors of characteristic functions

GaussianAnalysis.fourier.gauss_factorlibrary/fourier/gauss_factor.v1,099 lines27 lemmas and theorems, 5 definitionssource
Imports 6 library modules and 30 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.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 1

The bound of Lemma 3.5 of Koehler and Sohn's vector small-ball estimate: for a law mu on the line with E[X^2] <= v and Q(mu, lambda) <= 1 - eps, and for 0 < r <= 1/2 and r <= s,

\int |cf mu u|^(1/r^2) exp (- s^2 u^2 / (2 r^2)) du <= r C,
C = 16 pi^3 sqrt pi e^(1/8) (1 + sqrt (4 v / eps)) / (lambda sqrt eps)

(gauss_factor_le; gauss_factor_scaled_le after the substitution u = r t; gauss_factor_exists with the constant uniform in mu). The same holds with E[(X - a)^2] <= v for any a, the variance when a is the mean (gauss_factor_center_le, gauss_factor_center_exists). With N = floor (1 / (2 r^2)), |cf mu u|^(1/r^2) <= |cf mu u|^(2 N), the characteristic function of the sum S of N independent copies of the symmetrized law (cf_re_sum_sym). The Gaussian Fubini identity

\int cf_re nu u exp (- u^2 / 2) du = sqrt (2 pi) E[exp (- X^2 / 2)]

(Rintegral_cf_re_gauss_weight), the bound

E[exp (- X^2 / 2)] <= 2 e^(1/8) sqrt (2 pi) Q(nu, 1)

for X of law nu (gauss_weight_conc_fun), and the concentration of sums of esseen.v, Q(S, 1) <= C' / sqrt N <= 2 C' r, conclude.

The first half of the same lemma, for any truncation level c: a law with mean 0, variance 1 and E[X^2 1_{|X| <= M}] >= c has, for every L > 0,

Q(mu, L) <= 1 - min ((c - 4 L^2) / M^2, L^2 / (2 L^2 + 1))

(conc_fun_truncated_level, conc_fun_truncated_level_exists). For c = 1/2 and L = 1/8 this gives the paper's Q(mu, 1/8) <= 1 - min (7 / (16 M^2), 1/100) (conc_fun_truncated, conc_fun_truncated_exists). The length must depend on c: if c < 1/256, a law with mass close to 1 at +-1/16 and a small mass far away has Q(mu, 1/8) close to 1.

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

sym_diff pp.1 - p.2, as a measurable function on pairs
sym_law muthe law of X - X' for independent X and X' of law mu
tuple_sum xthe sum of the coordinates of the tuple x
sum_law mu nthe law of X_0 + ... + X_(n-1) for independent X_k of laws mu k
gauss_factor_const v lambda epsthe constant C of gauss_factor_le

Main results

ResultsStatement
gauss_factor_legauss_factor_constgauss_factor_const_gt0
Lemma 3.5 of Koehler and Sohn: for a law mu on the line with E[X^2] <= v and Q(mu, lambda) <= 1 - eps (v, lambda, eps > 0), and for 0 < r <= 1/2 and r <= s, \int |cf mu u|^(1/r^2) exp (- s^2 u^2 / (2 r^2)) du <= r C (an integral in [0, +oo]), with C = 16 pi^3 sqrt pi e^(1/8) (1 + sqrt (4 v / eps)) / (lambda sqrt eps).
gauss_factor_scaled_legauss_factor_existsgauss_factor_center_legauss_factor_center_exists
The same bound after the substitution u = r t: \int |cf mu (r t)|^(1/r^2) exp (- s^2 t^2 / 2) dt <= C; the form with a constant C > 0 uniform in mu, r and s for 0 < r <= s <= 1/2; and both with the centered moment E[(X - a)^2] <= v for any a (the variance when a is the mean) in place of E[X^2] <= v, with the same constant.
conc_fun_truncated_levelconc_fun_truncated_level_existsconc_fun_truncatedconc_fun_truncated_exists
The first half of the same lemma, for any truncation level c: a law with mean 0, variance 1 and E[X^2 1_{|X| <= M}] >= c (M > 0) satisfies Q(mu, L) <= 1 - min ((c - 4 L^2) / M^2, L^2 / (2 L^2 + 1)) for every L > 0, a bound with a positive constant when 4 L^2 < c. For c = 1/2 and L = 1/8, the paper's form: Q(mu, 1/8) <= 1 - min (7 / (16 M^2), 1/100).
Rintegral_cf_re_gauss_weightgauss_weight_conc_funRintegral_gauss_weightRintegral_normal01
The Gaussian Fubini identity \int cf_re nu u exp (- u^2 / 2) du = sqrt (2 pi) E[exp (- X^2 / 2)] for X of law nu; the bound E[exp (- X^2 / 2)] <= 2 e^(1/8) sqrt (2 pi) Q(nu, 1); \int exp (- y^2 / 2) dy = sqrt (2 pi); E[f (G)] = \int f phi for G standard normal and f bounded measurable.
sym_lawsum_lawcf_sym_lawconc_fun_sym_lawsym_law_second_momentcf_re_sum_sym
The law of X - X' for X, X' independent of law mu, and the law of a sum of independent variables (tuple_prod): cf (sym_law mu) t = (|cf mu t|^2, 0), Q(sym_law mu, L) <= Q(mu, L), E[(X - X')^2] <= 4 E[X^2], and the sum of n independent copies of X - X' has real characteristic function |cf mu t|^(2 n).

Declarations34 exported, 20 local

lemma, theoremdefinitioninstancelocal
sectionlaws
Context {R : realType}.
definition sym_diff source, line 70
Type
forall {R : realType}, measurableTypeR R * measurableTypeR R -> measurableTypeR R
Definition
Definition sym_diff (p : measurableTypeR R * measurableTypeR R) :
  measurableTypeR R := (p.1 : R) - p.2.
Used by 6 declarations in 1 file
lemma measurable_sym_diff source, line 73 
forall {R : realType},
measurable_fun
  [set: ((g_sigma_algebraType (R.-ocitv).-measurable) * (g_sigma_algebraType (R.-ocitv).-measurable))]
  sym_diff
Statement as written in the source
Lemma measurable_sym_diff : measurable_fun [set: _] sym_diff.
Used by 2 declarations in 1 file
instance instance at line 80 source, line 80 
HB.instance Definition _ :=
  isMeasurableFun.Build _ _ _ _ sym_diff measurable_sym_diff.
definition sym_law main result source, line 84
Type
forall {R : realType},
probability (measurableTypeR R) R -> probability (measurableTypeR R) R
Definition
Definition sym_law (mu : probability (measurableTypeR R) R) :
  probability (measurableTypeR R) R := distribution (mu \x mu)%E sym_diff.

The law of X - X' for X and X' independent of law mu.

Main result, as the README states it

The law of X - X' for X, X' independent of law mu, and the law of a sum of independent variables (tuple_prod): cf (sym_law mu) t = (|cf mu t|^2, 0), Q(sym_law mu, L) <= Q(mu, L), E[(X - X')^2] <= 4 E[X^2], and the sum of n independent copies of X - X' has real characteristic function |cf mu t|^(2 n).

Used by 7 declarations in 1 file
lemma sym_lawE source, line 87 
forall {R : realType} (mu : probability (measurableTypeR R) R)
  [A : set (measurableTypeR R)],
(((R.-ocitv).-measurable).-sigma).-measurable A ->
(mu \x mu)%E ((fun p : R * R => p.1 - p.2 : R) @^-1` A) = sym_law mu A
Statement as written in the source
Lemma sym_lawE (mu : probability (measurableTypeR R) R)
    (A : set (measurableTypeR R)) : measurable A ->
  (mu \x mu)%E ((fun p => p.1 - p.2 : R) @^-1` A) = sym_law mu A.
Used by 2 declarations in 1 file
definition tuple_sum source, line 92
Type
forall {R : realType} [n : nat], n.-tuple (measurableTypeR R) -> measurableTypeR R
Definition
Definition tuple_sum n (x : n.-tuple (measurableTypeR R)) : measurableTypeR R :=
  \sum_(k < n) (tnth x k : R).
Used by 3 declarations in 1 file
lemma measurable_tuple_sum source, line 95 
forall {R : realType} [n : nat],
measurable_fun [set: n.-tuple _]
  (tuple_sum (n:=n))
Statement as written in the source
Lemma measurable_tuple_sum n : measurable_fun [set: _] (@tuple_sum n).
Used by 1 declaration in 1 file
instance instance at line 101 source, line 101 
HB.instance Definition _ n :=
  isMeasurableFun.Build _ _ _ _ (@tuple_sum n) (@measurable_tuple_sum n).
definition sum_law main result source, line 105
Type
forall {R : realType},
(nat -> probability (measurableTypeR R) R) -> nat -> probability (measurableTypeR R) R
Definition
Definition sum_law (mu : nat -> probability (measurableTypeR R) R) n :
  probability (measurableTypeR R) R :=
  distribution (tuple_prod mu n) (@tuple_sum n).

The law of X_1 + ... + X_n for independent X_k of laws mu k.

Main result

Stated in the README together with sym_law.

Used by 3 declarations in 1 file
lemma sum_lawE source, line 109 
forall {R : realType} (mu : nat -> probability (measurableTypeR R) R) 
  (n : nat) [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) = sum_law mu n A
Statement as written in the source
Lemma sum_lawE (mu : nat -> probability (measurableTypeR R) R) n
    (A : set (measurableTypeR R)) : measurable A ->
  tuple_prod mu n ((fun x => \sum_(k < n) tnth x k) @^-1` A) = sum_law mu n A.
Used by 1 declaration in 1 file

The first half of Lemma 3.5 of Koehler and Sohn, for any truncation level c: a law of mean 0 and variance 1 with E[X^2 1_{|X| <= M}] >= c puts mass at most 1 - min ((c - 4 L^2) / M^2, L^2 / (2 L^2 + 1)) on every interval of length L > 0.

sectiontruncated_moment
Context {R : realType} (mu : probability (measurableTypeR R) R) (M c : R).
Hypothesis M0 : 0 < M.
Hypothesis mean0 : (\int[mu]_x (x : R)%:E = 0)%E.
Hypothesis var1 : (\int[mu]_x (((x : R) ^+ 2)%R)%:E = 1)%E.
Hypothesis trunc : (c%:E <=
  \int[mu]_x (((x : R) ^+ 2 * \1_[set y : R | `|y| <= M] x)%R)%:E)%E.
Local Notation S := [set y : R | `|y| <= M].
let mx section-local source, line 130 
Let mx : measurable_fun [set: measurableTypeR R] (fun x => x : R).
let mx2 section-local source, line 133 
Let mx2 : measurable_fun [set: measurableTypeR R] (fun x => (x : R) ^+ 2).
let mS section-local source, line 136 
Let mS : measurable S.
Used by 1 declaration in 1 file
let ix2 section-local source, line 143 
Let ix2 : mu.-integrable [set: _] (EFin \o (fun x => (x : R) ^+ 2)).
Used by 4 declarations in 1 file
let ix section-local source, line 150 
Let ix : mu.-integrable [set: _] (EFin \o (fun x => x : R)).
Used by 2 declarations in 1 file
let Ex2 section-local source, line 163 
Let Ex2 : \int[mu]_x ((x : R) ^+ 2) = 1.
Used by 2 declarations in 1 file
let Ex section-local source, line 166 
Let Ex : \int[mu]_x (x : R) = 0.
Used by 1 declaration in 1 file
let prob_fine section-local source, line 169 
Let prob_fine (A : set (measurableTypeR R)) : measurable A ->
  mu A = (fine (mu A))%:E.
Used by 2 declarations in 1 file
let iI section-local source, line 176 
Let iI (A : set (measurableTypeR R)) : measurable A ->
  mu.-integrable [set: _] (EFin \o \1_A).
Used by 2 declarations in 1 file
let RI section-local source, line 184 
Let RI (A : set (measurableTypeR R)) : measurable A ->
  \int[mu]_x \1_A x = fine (mu A).
Used by 2 declarations in 1 file
let ix2A section-local source, line 188 
Let ix2A (A : set (measurableTypeR R)) : measurable A ->
  mu.-integrable [set: _] (EFin \o (fun x => (x : R) ^+ 2 * \1_A x)).
Used by 1 declaration in 1 file
let ixA section-local source, line 198 
Let ixA (A : set (measurableTypeR R)) (sg : R) : measurable A -> sg ^+ 2 = 1 ->
  mu.-integrable [set: _] (EFin \o (fun x => sg * (x : R) * \1_A x)).
Used by 1 declaration in 1 file
let dl_eq section-local source, line 211 
Let dl_eq (I : set (measurableTypeR R)) : measurable I ->
  \int[mu]_x \1_(~` I) x = 1 - fine (mu I).
Used by 2 declarations in 1 file
let case_small section-local source, line 221 
Let case_small (I : set (measurableTypeR R)) (L : R) : measurable I ->
  (forall x, I x -> `|x : R| <= 2 * L) ->
  (c - 4 * L ^+ 2) / M ^+ 2 <= 1 - fine (mu I).

If an interval I lies in [-2 L, 2 L], mu misses it with probability at least (c - 4 L^2) / M^2.

Used by 1 declaration in 1 file
let case_far section-local source, line 289 
Let case_far (I : set (measurableTypeR R)) (sg L : R) : measurable I ->
  0 < L -> sg ^+ 2 = 1 -> (forall x, I x -> L <= sg * x) ->
  L ^+ 2 / (2 * L ^+ 2 + 1) <= 1 - fine (mu I).

If sg x >= L on I, with sg = 1 or sg = -1, then mu misses I with probability at least L^2 / (2 L^2 + 1), because E[X] = 0 and E[X^2] = 1.

Used by 1 declaration in 1 file
lemma conc_fun_truncated_level main result source, line 372 
forall {R : realType} [mu : probability (measurableTypeR R) R] [M c : R],
0 < M ->
(\int[mu]_x (x : R)%:E)%E = 0 ->
(\int[mu]_x ((x : R) ^+ 2)%:E)%E = 1%E ->
(c%:E <= \int[mu]_x ((x : R) ^+ 2 * \1_[set y | `|y| <= M] x)%:E)%E ->
forall [L : R],
0 < L -> conc_fun mu L <= 1 - minr ((c - 4 * L ^+ 2) / M ^+ 2) (L ^+ 2 / (2 * L ^+ 2 + 1))
Main result, as the README states it

The first half of the same lemma, for any truncation level c: a law with mean 0, variance 1 and E[X^2 1_{|X| <= M}] >= c (M > 0) satisfies Q(mu, L) <= 1 - min ((c - 4 L^2) / M^2, L^2 / (2 L^2 + 1)) for every L > 0, a bound with a positive constant when 4 L^2 < c. For c = 1/2 and L = 1/8, the paper's form: Q(mu, 1/8) <= 1 - min (7 / (16 M^2), 1/100).

Statement as written in the source
Lemma conc_fun_truncated_level (L : R) : 0 < L ->
  conc_fun mu L <=
  1 - minr ((c - 4 * L ^+ 2) / M ^+ 2) (L ^+ 2 / (2 * L ^+ 2 + 1)).
Used by 2 declarations in 1 file

The first half of Lemma 3.5 as stated in the paper: level 1/2 and intervals of length 1/8.

sectiontruncated_moment_half
Context {R : realType} (mu : probability (measurableTypeR R) R) (M : R).
Hypothesis M0 : 0 < M.
Hypothesis mean0 : (\int[mu]_x (x : R)%:E = 0)%E.
Hypothesis var1 : (\int[mu]_x (((x : R) ^+ 2)%R)%:E = 1)%E.
Hypothesis trunc : ((2^-1)%:E <=
  \int[mu]_x (((x : R) ^+ 2 * \1_[set y : R | `|y| <= M] x)%R)%:E)%E.
lemma conc_fun_truncated main result source, line 407 
forall {R : realType} [mu : probability (measurableTypeR R) R] [M : R],
0 < M ->
(\int[mu]_x (x : R)%:E)%E = 0 ->
(\int[mu]_x ((x : R) ^+ 2)%:E)%E = 1%E ->
((2^-1)%:E <= \int[mu]_x ((x : R) ^+ 2 * \1_[set y | `|y| <= M] x)%:E)%E ->
conc_fun mu 8^-1 <= 1 - minr (7 / (16 * M ^+ 2)) 100^-1
Main result

Stated in the README together with conc_fun_truncated_level.

Statement as written in the source
Lemma conc_fun_truncated :
  conc_fun mu 8^-1 <= 1 - minr (7 / (16 * M ^+ 2)) 100^-1.
Used by 1 declaration in 1 file

The Gaussian weight exp (- y^2 / 2), of integral sqrt (2 pi).

sectiongauss_weight
Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
lemma normal_peak1V source, line 427 
forall {R : realType}, (normal_peak (1 : R))^-1 = Num.ExtraDef.sqrtr (2 * pi)
Statement as written in the source
Lemma normal_peak1V : (normal_peak (1 : R))^-1 = Num.sqrt (2 * pi).
Used by 2 declarations in 1 file
let peak0 section-local source, line 430 
Let peak0 : 0 < normal_peak (1 : R).
let gwE section-local source, line 433 
Let gwE (y : R) : expR (- y ^+ 2 / 2) = (normal_peak 1)^-1 * normal_pdf 0 1 y.
Used by 3 declarations in 1 file
lemma measurable_gauss_weight source, line 436 
forall {R : realType},
measurable_fun [set: R]
  (fun y : R => expR (- y ^+ 2 / 2))
Statement as written in the source
Lemma measurable_gauss_weight :
  measurable_fun [set: R] (fun y => expR (- y ^+ 2 / 2)).
Used by 4 declarations in 1 file
lemma integrable_gauss_weight source, line 445 
forall {R : realType},
lebesgue_measure.-integrable [set: R]
  (EFin \o
     (fun y : join_GRing_PzRing_between_Algebra_BaseZmodule_and_GRing_PzSemiRing R =>
      expR (- y ^+ 2 / 2)))
Statement as written in the source
Lemma integrable_gauss_weight :
  leb.-integrable [set: R] (EFin \o (fun y => expR (- y ^+ 2 / 2))).
Used by 4 declarations in 1 file
lemma Rintegral_gauss_weight main result source, line 453 
forall {R : realType},
\int[lebesgue_measure]_y expR (- y ^+ 2 / 2) = Num.ExtraDef.sqrtr (2 * pi)
Main result

Stated in the README together with Rintegral_cf_re_gauss_weight.

Statement as written in the source
Lemma Rintegral_gauss_weight :
  \int[leb]_y expR (- y ^+ 2 / 2) = Num.sqrt (2 * pi) :> R.
Used by 1 declaration in 1 file
sectiongauss_conc
Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
let leb_itv section-local source, line 468 
Let leb_itv (a b : R) : a <= b -> leb `[a, b]%classic = (b - a)%:E.
Used by 1 declaration in 1 file
let window section-local source, line 480 
Let window (x : measurableTypeR R) :
  expR (- 8^-1) / 2 * expR (- (x : R) ^+ 2 / 2) <=
  \int[leb]_y (\1_`[(x : R) - 2^-1, (x : R) + 2^-1]%classic y *
    expR (- (y : R) ^+ 2 / 2)).

The integral of exp (- y^2 / 2) over [x - 1/2, x + 1/2] is at least exp (- 1/8) exp (- x^2 / 2) / 2: on the half of the window that is closer to 0, y^2 <= x^2 + 1/4.

Used by 1 declaration in 1 file
lemma gauss_weight_conc_fun main result source, line 552 
forall {R : realType} (nu : probability (measurableTypeR R) R),
\int[nu]_x expR (- (x : R) ^+ 2 / 2) <=
2 * expR 8^-1 * Num.ExtraDef.sqrtr (2 * pi) * conc_fun nu 1

E[exp (- X^2 / 2)] <= 2 e^(1/8) sqrt (2 pi) Q(X, 1).

Main result

Stated in the README together with Rintegral_cf_re_gauss_weight.

Statement as written in the source
Lemma gauss_weight_conc_fun (nu : probability (measurableTypeR R) R) :
  \int[nu]_x expR (- (x : R) ^+ 2 / 2) <=
  2 * expR 8^-1 * Num.sqrt (2 * pi) * conc_fun nu 1.
Used by 1 declaration in 1 file
sectiongauss_fubini
Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
Local Notation N := (@normal_prob R 0 1).
lemma Rintegral_normal01 main result source, line 670 
forall {R : realType} [f : R -> R] [C : R],
measurable_fun [set: R] f ->
(forall x : R, `|f x| <= C) ->
\int[normal_prob 0 1]_x f x = \int[lebesgue_measure]_x (f x * normal_pdf 0 1 x)

For f bounded and measurable, E[f (G)] = \int f (x) phi (x) dx, with G standard normal and phi its density.

Main result

Stated in the README together with Rintegral_cf_re_gauss_weight.

Statement as written in the source
Lemma Rintegral_normal01 (f : R -> R) (C : R) :
  measurable_fun [set: R] f -> (forall x, `|f x| <= C) ->
  \int[N]_x f x = \int[leb]_x (f x * normal_pdf 0 1 x).
Used by 1 declaration in 1 file
lemma Rintegral_cf_re_gauss_weight main result source, line 681 
forall {R : realType} (nu : probability (measurableTypeR R) R),
\int[lebesgue_measure]_u (cf_re nu u * expR (- (u : R) ^+ 2 / 2)) =
Num.ExtraDef.sqrtr (2 * pi) * \int[nu]_x expR (- (x : R) ^+ 2 / 2)

The Gaussian Fubini identity: the integral of cf_re nu against the Gaussian weight is sqrt (2 pi) E[exp (- X^2 / 2)] for X of law nu.

Main result, as the README states it

The Gaussian Fubini identity \int cf_re nu u exp (- u^2 / 2) du = sqrt (2 pi) E[exp (- X^2 / 2)] for X of law nu; the bound E[exp (- X^2 / 2)] <= 2 e^(1/8) sqrt (2 pi) Q(nu, 1); \int exp (- y^2 / 2) dy = sqrt (2 pi); E[f (G)] = \int f phi for G standard normal and f bounded measurable.

Statement as written in the source
Lemma Rintegral_cf_re_gauss_weight (nu : probability (measurableTypeR R) R) :
  \int[leb]_u (cf_re nu u * expR (- (u : R) ^+ 2 / 2)) =
  Num.sqrt (2 * pi) * \int[nu]_x expR (- (x : R) ^+ 2 / 2).
Used by 1 declaration in 1 file

The symmetrized law, and sums of independent copies of it.

sectionsym_sum_facts
Context {R : realType}.
Implicit Types mu : probability (measurableTypeR R) R.
lemma cf_sym_law main result source, line 738 
forall {R : realType} (mu : probability (measurableTypeR R) R) (t : R),
cf (sym_law mu) t = (cf_norm mu t ^+ 2, 0)
Main result

Stated in the README together with sym_law.

Statement as written in the source
Lemma cf_sym_law mu t : cf (sym_law mu) t = (cf_norm mu t ^+ 2, 0).
Used by 1 declaration in 1 file
lemma conc_fun_sym_law main result source, line 741 
forall {R : realType} (mu : probability (measurableTypeR R) R) (L : R),
conc_fun (sym_law mu) L <= conc_fun mu L
Main result

Stated in the README together with sym_law.

Statement as written in the source
Lemma conc_fun_sym_law mu (L : R) : conc_fun (sym_law mu) L <= conc_fun mu L.
Used by 1 declaration in 1 file
lemma sym_law_second_moment main result source, line 751 
forall {R : realType} [mu : probability (measurableTypeR R) R] [v : R],
(\int[mu]_x ((x : R) ^+ 2)%:E <= v%:E)%E ->
(\int[sym_law mu]_x ((x : R) ^+ 2)%:E <= (4 * v)%:E)%E

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

Main result

Stated in the README together with sym_law.

Statement as written in the source
Lemma sym_law_second_moment mu (v : R) :
  (\int[mu]_x (((x : R) ^+ 2)%R)%:E <= v%:E)%E ->
  (\int[sym_law mu]_x (((x : R) ^+ 2)%R)%:E <= (4 * v)%:E)%E.
lemma sym_law_second_moment_center source, line 766 
forall {R : realType} [mu : probability (measurableTypeR R) R] [a v : R],
(\int[mu]_x (((x : R) - a) ^+ 2)%:E <= v%:E)%E ->
(\int[sym_law mu]_x ((x : R) ^+ 2)%:E <= (4 * v)%:E)%E

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

Statement as written in the source
Lemma sym_law_second_moment_center mu (a v : R) :
  (\int[mu]_x ((((x : R) - a) ^+ 2)%R)%:E <= v%:E)%E ->
  (\int[sym_law mu]_x (((x : R) ^+ 2)%R)%:E <= (4 * v)%:E)%E.
Used by 1 declaration in 1 file
lemma cmul_real_big source, line 781 
forall {R : realType} [I : Type] (r : seq I) (P : pred I) (F : I -> R),
\big[cmul/(1, 0)]_(i <- r | P i) (F i, 0) = (\prod_(i <- r | P i) F i, 0)

A complex product of real numbers is real.

Statement as written in the source
Lemma cmul_real_big (I : Type) (r : seq I) (P : pred I) (F : I -> R) :
  \big[cmul/(1, 0)]_(i <- r | P i) (F i, 0) = (\prod_(i <- r | P i) F i, 0).
Used by 1 declaration in 1 file
lemma cf_re_sum_sym main result source, line 790 
forall {R : realType} (mu : probability (measurableTypeR R) R) (n : nat) (t : R),
cf_re (sum_law (fun=> sym_law mu) n) t = cf_norm mu t ^+ (2 * n)

The sum of n independent copies of X - X' has the characteristic function |cf mu t|^(2 n).

Main result

Stated in the README together with sym_law.

Statement as written in the source
Lemma cf_re_sum_sym mu n t :
  cf_re (sum_law (fun=> sym_law mu) n) t = cf_norm mu t ^+ (2 * n).
Used by 1 declaration in 1 file
sectiongauss_factor_bound
Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
definition gauss_factor_const main result source, line 813
Type
forall {R : realType}, R -> R -> R -> R
Definition
Definition gauss_factor_const (v lambda eps : R) : R :=
  16 * pi ^+ 3 * Num.sqrt pi * expR 8^-1 * (1 + Num.sqrt (4 * v / eps)) /
  (lambda * Num.sqrt eps).
Main result

Stated in the README together with gauss_factor_le.

Used by 6 declarations in 1 file
lemma gauss_factor_const_gt0 main result source, line 817 
forall {R : realType} [v lambda eps : R],
0 < v -> 0 < lambda -> 0 < eps -> 0 < gauss_factor_const v lambda eps
Main result

Stated in the README together with gauss_factor_le.

Statement as written in the source
Lemma gauss_factor_const_gt0 (v lambda eps : R) :
  0 < v -> 0 < lambda -> 0 < eps -> 0 < gauss_factor_const v lambda eps.
Used by 2 declarations in 1 file
let measurable_integrand section-local source, line 826 
Let measurable_integrand (mu : probability (measurableTypeR R) R) (p a b : R) :
  measurable_fun [set: R]
    (fun u => cf_norm mu u `^ p * expR (- a * u ^+ 2 / b)).
Used by 2 declarations in 1 file
theorem gauss_factor_center_le main result source, line 842 
forall {R : realType} [mu : probability (measurableTypeR R) R] [a v lambda eps r s : R],
0 < v ->
0 < lambda ->
0 < eps ->
(\int[mu]_x (((x : R) - a) ^+ 2)%:E <= v%:E)%E ->
conc_fun mu lambda <= 1 - eps ->
0 < r ->
r <= 2^-1 ->
r <= s ->
(\int[lebesgue_measure]_u
    (cf_norm mu u `^ (r ^- 2) * expR (- s ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <=
 (r * gauss_factor_const v lambda eps)%:E)%E

Lemma 3.5 of Koehler and Sohn: for a law mu on the line with E[(X - a)^2] <= v for some a and Q(mu, lambda) <= 1 - eps, and for 0 < r <= 1/2 and r <= s, \int |cf mu u|^(1/r^2) exp (- s^2 u^2 / (2 r^2)) du <= r C, with C depending only on v, lambda and eps.

Main result

Stated in the README together with gauss_factor_scaled_le.

Statement as written in the source
Theorem gauss_factor_center_le (mu : probability (measurableTypeR R) R)
    (a v lambda eps r s : R) :
  0 < v -> 0 < lambda -> 0 < eps ->
  (\int[mu]_x ((((x : R) - a) ^+ 2)%R)%:E <= v%:E)%E ->
  conc_fun mu lambda <= 1 - eps ->
  0 < r -> r <= 2^-1 -> r <= s ->
  (\int[leb]_u (cf_norm mu u `^ (r ^- 2) *
     expR (- s ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <=
   (r * gauss_factor_const v lambda eps)%:E)%E.
Used by 2 declarations in 1 file
theorem gauss_factor_le main result source, line 979 
forall {R : realType} [mu : probability (measurableTypeR R) R] [v lambda eps r s : R],
0 < v ->
0 < lambda ->
0 < eps ->
(\int[mu]_x ((x : R) ^+ 2)%:E <= v%:E)%E ->
conc_fun mu lambda <= 1 - eps ->
0 < r ->
r <= 2^-1 ->
r <= s ->
(\int[lebesgue_measure]_u
    (cf_norm mu u `^ (r ^- 2) * expR (- s ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <=
 (r * gauss_factor_const v lambda eps)%:E)%E

The case a = 0: E[X^2] <= v.

Main result, as the README states it

Lemma 3.5 of Koehler and Sohn: for a law mu on the line with E[X^2] <= v and Q(mu, lambda) <= 1 - eps (v, lambda, eps > 0), and for 0 < r <= 1/2 and r <= s, \int |cf mu u|^(1/r^2) exp (- s^2 u^2 / (2 r^2)) du <= r C (an integral in [0, +oo]), with C = 16 pi^3 sqrt pi e^(1/8) (1 + sqrt (4 v / eps)) / (lambda sqrt eps).

Statement as written in the source
Theorem gauss_factor_le (mu : probability (measurableTypeR R) R)
    (v lambda eps r s : R) :
  0 < v -> 0 < lambda -> 0 < eps ->
  (\int[mu]_x (((x : R) ^+ 2)%R)%:E <= v%:E)%E ->
  conc_fun mu lambda <= 1 - eps ->
  0 < r -> r <= 2^-1 -> r <= s ->
  (\int[leb]_u (cf_norm mu u `^ (r ^- 2) *
     expR (- s ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <=
   (r * gauss_factor_const v lambda eps)%:E)%E.
Used by 2 declarations in 1 file
corollary gauss_factor_scaled_le main result source, line 996 
forall {R : realType} [mu : probability (measurableTypeR R) R] [v lambda eps r s : R],
0 < v ->
0 < lambda ->
0 < eps ->
(\int[mu]_x ((x : R) ^+ 2)%:E <= v%:E)%E ->
conc_fun mu lambda <= 1 - eps ->
0 < r ->
r <= 2^-1 ->
r <= s ->
(\int[lebesgue_measure]_t
    (cf_norm mu (r * t) `^ (r ^- 2) * expR (- s ^+ 2 * t ^+ 2 / 2))%:E <=
 (gauss_factor_const v lambda eps)%:E)%E

The same bound after the substitution u = r t: \int |cf mu (r t)|^(1/r^2) exp (- s^2 t^2 / 2) dt <= C.

Main result, as the README states it

The same bound after the substitution u = r t: \int |cf mu (r t)|^(1/r^2) exp (- s^2 t^2 / 2) dt <= C; the form with a constant C > 0 uniform in mu, r and s for 0 < r <= s <= 1/2; and both with the centered moment E[(X - a)^2] <= v for any a (the variance when a is the mean) in place of E[X^2] <= v, with the same constant.

Statement as written in the source
Corollary gauss_factor_scaled_le (mu : probability (measurableTypeR R) R)
    (v lambda eps r s : R) :
  0 < v -> 0 < lambda -> 0 < eps ->
  (\int[mu]_x (((x : R) ^+ 2)%R)%:E <= v%:E)%E ->
  conc_fun mu lambda <= 1 - eps ->
  0 < r -> r <= 2^-1 -> r <= s ->
  (\int[leb]_t (cf_norm mu (r * t) `^ (r ^- 2) *
     expR (- s ^+ 2 * t ^+ 2 / 2))%:E <=
   (gauss_factor_const v lambda eps)%:E)%E.
corollary gauss_factor_exists main result source, line 1027 
forall {R : realType} [v lambda eps : R],
0 < v ->
0 < lambda ->
0 < eps ->
exists2 C : R,
  0 < C &
  forall (mu : probability (measurableTypeR R) R) (r s : R),
  (\int[mu]_x ((x : R) ^+ 2)%:E <= v%:E)%E ->
  conc_fun mu lambda <= 1 - eps ->
  0 < r <= s ->
  s <= 2^-1 ->
  (\int[lebesgue_measure]_u
      (cf_norm mu u `^ (r ^- 2) * expR (- s ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <=
   (r * C)%:E)%E

The form with a constant uniform in the law.

Main result

Stated in the README together with gauss_factor_scaled_le.

Statement as written in the source
Corollary gauss_factor_exists (v lambda eps : R) :
  0 < v -> 0 < lambda -> 0 < eps ->
  exists2 C : R, 0 < C &
  forall (mu : probability (measurableTypeR R) R) (r s : R),
    (\int[mu]_x (((x : R) ^+ 2)%R)%:E <= v%:E)%E ->
    conc_fun mu lambda <= 1 - eps ->
    0 < r <= s -> s <= 2^-1 ->
    (\int[leb]_u (cf_norm mu u `^ (r ^- 2) *
       expR (- s ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <= (r * C)%:E)%E.
Used by 1 declaration in 1 file
corollary gauss_factor_center_exists main result source, line 1045 
forall {R : realType} [v lambda eps : R],
0 < v ->
0 < lambda ->
0 < eps ->
exists2 C : R,
  0 < C &
  forall (mu : probability (measurableTypeR R) R) (a r s : R),
  (\int[mu]_x (((x : R) - a) ^+ 2)%:E <= v%:E)%E ->
  conc_fun mu lambda <= 1 - eps ->
  0 < r <= s ->
  s <= 2^-1 ->
  (\int[lebesgue_measure]_u
      (cf_norm mu u `^ (r ^- 2) * expR (- s ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <=
   (r * C)%:E)%E

The same with a centered second moment, E[(X - a)^2] <= v for some a: the variance when a is the mean.

Main result

Stated in the README together with gauss_factor_scaled_le.

Statement as written in the source
Corollary gauss_factor_center_exists (v lambda eps : R) :
  0 < v -> 0 < lambda -> 0 < eps ->
  exists2 C : R, 0 < C &
  forall (mu : probability (measurableTypeR R) R) (a r s : R),
    (\int[mu]_x ((((x : R) - a) ^+ 2)%R)%:E <= v%:E)%E ->
    conc_fun mu lambda <= 1 - eps ->
    0 < r <= s -> s <= 2^-1 ->
    (\int[leb]_u (cf_norm mu u `^ (r ^- 2) *
       expR (- s ^+ 2 * u ^+ 2 / (2 * r ^+ 2)))%:E <= (r * C)%:E)%E.
Used by 1 declaration in 1 file
corollary conc_fun_truncated_exists main result source, line 1064 
forall {R : realType} [M : R],
0 < M ->
exists2 c : R,
  0 < c &
  forall mu : probability (measurableTypeR R) R,
  (\int[mu]_x (x : R)%:E)%E = 0 ->
  (\int[mu]_x ((x : R) ^+ 2)%:E)%E = 1%E ->
  ((2^-1)%:E <= \int[mu]_x ((x : R) ^+ 2 * \1_[set y | `|y| <= M] x)%:E)%E ->
  conc_fun mu 8^-1 <= 1 - c

The first half of Lemma 3.5 with a constant uniform in the law.

Main result

Stated in the README together with conc_fun_truncated_level.

Statement as written in the source
Corollary conc_fun_truncated_exists {R : realType} (M : R) : 0 < M ->
  exists2 c : R, 0 < c &
  forall mu : probability (measurableTypeR R) R,
    (\int[mu]_x (x : R)%:E = 0)%E ->
    (\int[mu]_x (((x : R) ^+ 2)%R)%:E = 1)%E ->
    ((2^-1)%:E <=
      \int[mu]_x (((x : R) ^+ 2 * \1_[set y : R | `|y| <= M] x)%R)%:E)%E ->
    conc_fun mu 8^-1 <= 1 - c.
Used by 1 declaration in 1 file
corollary conc_fun_truncated_level_exists main result source, line 1081 
forall {R : realType} [M c L : R],
0 < M ->
0 < L ->
4 * L ^+ 2 < c ->
exists2 k : R,
  0 < k &
  forall mu : probability (measurableTypeR R) R,
  (\int[mu]_x (x : R)%:E)%E = 0 ->
  (\int[mu]_x ((x : R) ^+ 2)%:E)%E = 1%E ->
  (c%:E <= \int[mu]_x ((x : R) ^+ 2 * \1_[set y | `|y| <= M] x)%:E)%E ->
  conc_fun mu L <= 1 - k

The same for any truncation level c, on intervals of any length L with 4 L^2 < c (for instance L = sqrt c / 4).

Main result

Stated in the README together with conc_fun_truncated_level.

Statement as written in the source
Corollary conc_fun_truncated_level_exists {R : realType} (M c L : R) :
  0 < M -> 0 < L -> 4 * L ^+ 2 < c ->
  exists2 k : R, 0 < k &
  forall mu : probability (measurableTypeR R) R,
    (\int[mu]_x (x : R)%:E = 0)%E ->
    (\int[mu]_x (((x : R) ^+ 2)%R)%:E = 1)%E ->
    (c%:E <=
      \int[mu]_x (((x : R) ^+ 2 * \1_[set y : R | `|y| <= M] x)%R)%:E)%E ->
    conc_fun mu L <= 1 - k.
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.