GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisfouriercharfun_rV

Characteristic functions of laws on row vectors

GaussianAnalysis.fourier.charfun_rVlibrary/fourier/charfun_rV.v900 lines30 lemmas and theorems, 4 definitionssource
Imports 12 library modules and 34 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.finite_group.fingroup, mathcomp.finite_group.perm, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, 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.classical.cardinality, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.algebra.interval_inference, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.analysis.numfun, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.trigo, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.probability_theory.normal_distribution

Imported by 3

For a law nu on 'rV[R]_m, cf_rV nu theta is the characteristic function of nu at theta, given by its real and imaginary parts, the integrals of cos <x, theta> and sin <x, theta> against nu; it is the characteristic function at 1 of the law of <x, theta> (cf_rV_law). It is continuous in theta and of modulus at most one. The characteristic function of gauss m is exp (- |theta|^2 / 2) (cf_rV_gauss). The law of the sum of independent vectors has the complex product of their characteristic functions (cf_rV_add), and the law of \sum_k x_k w_k, for independent real x_k, has the complex product of those of the x_k at <w_k, theta> (cf_rV_tuple_prod).

Gaussian regularization, as in the method of Ball and Nazarov: for Y of law nu and an independent G of law gauss m, E[exp (- |z - Y|^2 / (2 s^2))] is a Gaussian average of cf nu (cf_rV_regularization), hence at most (s / sqrt (2 pi))^m times the integral of |cf nu| exp (- s^2 |theta|^2 / 2) (cf_rV_regularization_le), and P(Y + s G in B) is at most (2 pi)^-m times that integral times the Lebesgue measure of B (prod_gauss_le_cf_rV). No Fourier inversion is needed. The law of y + s G has the density w |-> s^-m gauss_pdf ((w - y) / s) (ge0_integral_gauss_affine). Letting s tend to 0: if |cf nu| is integrable, a closed ball has probability at most (2 pi)^-m (\int |cf nu|) times its Lebesgue measure (ball_le_cf_rV).

Here <x, theta> = mxdot x theta and |x|^2 = mxdot x x.

cf_rV_re nu theta\int[nu]_x cos (mxdot x theta)
cf_rV_im nu theta\int[nu]_x sin (mxdot x theta)
cf_rV nu thetathe pair (cf_rV_re nu theta, cf_rV_im nu theta)
cf_rV_norm nu thetaits modulus cmod (cf_rV nu theta)

Main results

ResultsStatement
cf_rV_recf_rV_imcf_rVcf_rV_normcf_rV_law
The characteristic function of a law nu on 'rV[R]_m at theta, without complex numbers: cf_rV_re nu theta = E[cos <x, theta>] and cf_rV_im nu theta = E[sin <x, theta>] for x of law nu, with <x, theta> = mxdot x theta; it is the characteristic function at 1 of the law of <x, theta>.
cf_rV_norm_le1continuous_cf_rV_recontinuous_cf_rV_imcontinuous_cf_rV_normmeasurable_cf_rV_norm
The modulus is at most one, and the three functions are continuous, hence measurable, in theta.
cf_rV_gausscf_rV_norm_gauss
The characteristic function of gauss m at theta is (exp (- mxdot theta theta / 2), 0).
cf_rV_imagecf_rV_addcf_rV_norm_addcf_rV_tuple_prodcf_rV_norm_tuple_prod
If nu is the law of g under P, cf_rV nu is computed under P. The law of the sum of independent vectors (under nu1 \x nu2) has the complex product of their characteristic functions. For x of law tuple_prod mu n and vectors w k, the law of \sum_k x_k w_k has at theta the complex product of the cf (mu k) <w k, theta>, so its modulus is the product of the cf_norm (mu k) <w k, theta>.
Rintegral_swap_bounded
Fubini for a bounded measurable function on a product of two probabilities: the two iterated integrals agree.
gauss_pdf_scalege0_integral_gauss_affine
The law of y + s G, for G of law gauss m and s > 0, has the density w |-> s^-m gauss_pdf ((w - y) / s) with respect to lebesgue_rV m.
cf_rV_regularizationcf_rV_regularization_le
Gaussian regularization: for Y of law nu, G of law gauss m and s > 0, E[exp (- |z - Y|^2 / (2 s^2))] = E[cos <G/s, z> cf_rV_re nu (G/s) + sin <G/s, z> cf_rV_im nu (G/s)], hence it is at most (s / sqrt (2 pi))^m \int |cf_rV nu theta| exp (- s^2 |theta|^2 / 2) dtheta, where |.| is the Euclidean norm.
prod_gauss_le_cf_rV
For Y of law nu and an independent G of law gauss m, s > 0 and a measurable B, P(Y + s G in B) <= (2 pi)^-m (\int |cf_rV nu theta| exp (- s^2 |theta|^2 / 2) dtheta) lebesgue_rV m B, with values in [0, +oo]. No Fourier inversion is used.
ball_le_cf_rV
If \int |cf_rV nu| < +oo, every closed Euclidean ball B of radius r > 0 satisfies nu B <= (2 pi)^-m (\int |cf_rV nu theta| dtheta) lebesgue_rV m B: prod_gauss_le_cf_rV with s -> 0.
measurable_ball_rVlebesgue_rV_ball_scaleintegral_gauss_mxdot_selfgauss_frobenius_ge
Closed Euclidean balls are measurable, and scaling the radius by a > 0 multiplies their Lebesgue measure by a^m. For G of law gauss m, E[|G|^2] = m and P(|G| <= t) >= 1 - m / t^2.

Declarations34 exported, 4 local

lemma, theoremdefinitioninstancelocal
sectioncf_rV
Context {R : realType} {m : nat}.
Implicit Types (nu : probability 'rV[R]_m R) (theta : 'rV[R]_m).
definition cf_rV_re main result source, line 70
Type
forall {R : realType} {m : nat}, probability 'rV_m R -> 'rV_m -> R
Definition
Definition cf_rV_re nu theta := \int[nu]_x cos (mxdot x theta).
Main result, as the README states it

The characteristic function of a law nu on 'rV[R]_m at theta, without complex numbers: cf_rV_re nu theta = E[cos <x, theta>] and cf_rV_im nu theta = E[sin <x, theta>] for x of law nu, with <x, theta> = mxdot x theta; it is the characteristic function at 1 of the law of <x, theta>.

Used by 14 declarations in 2 files
definition cf_rV_im main result source, line 72
Type
forall {R : realType} {m : nat}, probability 'rV_m R -> 'rV_m -> R
Definition
Definition cf_rV_im nu theta := \int[nu]_x sin (mxdot x theta).
Main result

Stated in the README together with cf_rV_re.

Used by 14 declarations in 2 files
definition cf_rV main result source, line 74
Type
forall {R : realType} {m : nat}, probability 'rV_m R -> 'rV_m -> R * R
Definition
Definition cf_rV nu theta : R * R := (cf_rV_re nu theta, cf_rV_im nu theta).
Main result

Stated in the README together with cf_rV_re.

Used by 8 declarations in 2 files
definition cf_rV_norm main result source, line 76
Type
forall {R : realType} {m : nat}, probability 'rV_m R -> 'rV_m -> R
Definition
Definition cf_rV_norm nu theta := cmod (cf_rV nu theta).
Main result

Stated in the README together with cf_rV_re.

Used by 27 declarations in 3 files
lemma cf_rV_norm_ge0 source, line 78 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) (theta : 'rV_m),
0 <= cf_rV_norm nu theta
Statement as written in the source
Lemma cf_rV_norm_ge0 nu theta : 0 <= cf_rV_norm nu theta.
Used by 10 declarations in 3 files
lemma cf_rV_law main result source, line 83 
forall {R : realType} {m : nat} [nu : probability 'rV_m R] [theta : 'rV_m]
  [mu : probability (measurableTypeR R) R],
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 nu ((mxdot (n:=m))^~ theta @^-1` A) = mu A) ->
cf_rV nu theta = cf mu 1

If mu is the law of <x, theta> for x of law nu, then cf_rV nu theta is the characteristic function of mu at 1.

Main result

Stated in the README together with cf_rV_re.

Statement as written in the source
Lemma cf_rV_law nu theta (mu : probability (measurableTypeR R) R) :
  (forall A : set (measurableTypeR R), measurable A ->
     nu ((fun x => mxdot x theta) @^-1` A) = mu A) ->
  cf_rV nu theta = cf mu 1.
Used by 2 declarations in 1 file
lemma cf_rV_norm_le1 main result source, line 93 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) (theta : 'rV_m),
cf_rV_norm nu theta <= 1
Main result, as the README states it

The modulus is at most one, and the three functions are continuous, hence measurable, in theta.

Statement as written in the source
Lemma cf_rV_norm_le1 nu theta : cf_rV_norm nu theta <= 1.
Used by 2 declarations in 2 files
lemma cf_rV_re_le1 source, line 105 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) (theta : 'rV_m),
`|cf_rV_re nu theta| <= 1
Statement as written in the source
Lemma cf_rV_re_le1 nu theta : `|cf_rV_re nu theta| <= 1.
lemma cf_rV_im_le1 source, line 111 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) (theta : 'rV_m),
`|cf_rV_im nu theta| <= 1
Statement as written in the source
Lemma cf_rV_im_le1 nu theta : `|cf_rV_im nu theta| <= 1.
let continuous_mxdotr section-local source, line 117 
Let continuous_mxdotr x : continuous (fun theta : 'rV[R]_m => mxdot x theta).
Used by 2 declarations in 1 file
lemma continuous_cf_rV_re main result source, line 125 
forall {R : realType} {m : nat} [nu : probability 'rV_m R], continuous (cf_rV_re nu)
Main result

Stated in the README together with cf_rV_norm_le1.

Statement as written in the source
Lemma continuous_cf_rV_re nu : continuous (cf_rV_re nu).
Used by 2 declarations in 1 file
lemma continuous_cf_rV_im main result source, line 138 
forall {R : realType} {m : nat} [nu : probability 'rV_m R], continuous (cf_rV_im nu)
Main result

Stated in the README together with cf_rV_norm_le1.

Statement as written in the source
Lemma continuous_cf_rV_im nu : continuous (cf_rV_im nu).
Used by 2 declarations in 1 file
lemma continuous_cf_rV_norm main result source, line 151 
forall {R : realType} {m : nat} [nu : probability 'rV_m R], continuous (cf_rV_norm nu)
Main result

Stated in the README together with cf_rV_norm_le1.

Statement as written in the source
Lemma continuous_cf_rV_norm nu : continuous (cf_rV_norm nu).
Used by 1 declaration in 1 file
lemma measurable_cf_rV_norm main result source, line 165 
forall {R : realType} {m : nat} (nu : probability 'rV_m R),
measurable_fun [set: 'rV_m] (cf_rV_norm nu)
Main result

Stated in the README together with cf_rV_norm_le1.

Statement as written in the source
Lemma measurable_cf_rV_norm nu : measurable_fun [set: 'rV[R]_m] (cf_rV_norm nu).
Used by 3 declarations in 2 files
lemma measurable_cf_rV_re source, line 168 
forall {R : realType} {m : nat} (nu : probability 'rV_m R),
measurable_fun [set: 'rV_m] (cf_rV_re nu)
Statement as written in the source
Lemma measurable_cf_rV_re nu : measurable_fun [set: 'rV[R]_m] (cf_rV_re nu).
Used by 3 declarations in 2 files
lemma measurable_cf_rV_im source, line 171 
forall {R : realType} {m : nat} (nu : probability 'rV_m R),
measurable_fun [set: 'rV_m] (cf_rV_im nu)
Statement as written in the source
Lemma measurable_cf_rV_im nu : measurable_fun [set: 'rV[R]_m] (cf_rV_im nu).
Used by 3 declarations in 2 files
lemma cf_rV_gauss main result source, line 175 
forall {R : realType} {m : nat} (theta : 'rV_m),
cf_rV (gauss m) theta = (expR (- mxdot theta theta / 2), 0)

The characteristic function of the standard Gaussian measure.

Main result, as the README states it

The characteristic function of gauss m at theta is (exp (- mxdot theta theta / 2), 0).

Statement as written in the source
Lemma cf_rV_gauss theta :
  cf_rV (gauss m) theta = (expR (- mxdot theta theta / 2), 0).
Used by 3 declarations in 2 files
lemma cf_rV_norm_gauss main result source, line 190 
forall {R : realType} {m : nat} (theta : 'rV_m),
cf_rV_norm (gauss m) theta = expR (- mxdot theta theta / 2)
Main result

Stated in the README together with cf_rV_gauss.

Statement as written in the source
Lemma cf_rV_norm_gauss theta :
  cf_rV_norm (gauss m) theta = expR (- mxdot theta theta / 2).

If nu is the law of g under P, the characteristic function of nu is computed under P.

sectioncf_rV_image
Context {R : realType} {m : nat} d (T : measurableType d) (P : probability T R).
Variables (nu : probability 'rV[R]_m R) (g : T -> 'rV[R]_m).
Hypothesis mg : measurable_fun [set: T] g.
Hypothesis gnu : forall A : set 'rV[R]_m, measurable A ->
  P (g @^-1` A) = nu A.
lemma cf_rV_image main result source, line 208 
forall {R : realType} {m : nat} [d : measure_display] [T : measurableType d]
  [P : probability T R] [nu : probability 'rV_m R] [g : T -> 'rV_m],
measurable_fun [set: T] g ->
(forall A : set 'rV_m,
 (measure_matrix_display default_measure_display).-measurable A -> P (g @^-1` A) = nu A) ->
forall theta : 'rV_m,
cf_rV nu theta = (\int[P]_x cos (mxdot (g x) theta), \int[P]_x sin (mxdot (g x) theta))
Main result, as the README states it

If nu is the law of g under P, cf_rV nu is computed under P. The law of the sum of independent vectors (under nu1 \x nu2) has the complex product of their characteristic functions. For x of law tuple_prod mu n and vectors w k, the law of \sum_k x_k w_k has at theta the complex product of the cf (mu k) <w k, theta>, so its modulus is the product of the cf_norm (mu k) <w k, theta>.

Statement as written in the source
Lemma cf_rV_image theta :
  cf_rV nu theta =
  (\int[P]_x cos (mxdot (g x) theta), \int[P]_x sin (mxdot (g x) theta)).
Used by 3 declarations in 1 file
lemma cf_rV_norm_image source, line 221 
forall {R : realType} {m : nat} [d : measure_display] [T : measurableType d]
  [P : probability T R] [nu : probability 'rV_m R] [g : T -> 'rV_m],
measurable_fun [set: T] g ->
(forall A : set 'rV_m,
 (measure_matrix_display default_measure_display).-measurable A -> P (g @^-1` A) = nu A) ->
forall theta : 'rV_m,
cf_rV_norm nu theta =
cmod (\int[P]_x cos (mxdot (g x) theta), \int[P]_x sin (mxdot (g x) theta))
Statement as written in the source
Lemma cf_rV_norm_image theta :
  cf_rV_norm nu theta =
  cmod (\int[P]_x cos (mxdot (g x) theta), \int[P]_x sin (mxdot (g x) theta)).
sectioncf_rV_independent
Context {R : realType} {m : nat}.
lemma cf_rV_add main result source, line 233 
forall {R : realType} {m : nat} [nu1 nu2 nu : probability 'rV_m R],
(forall A : set 'rV_m,
 (measure_matrix_display default_measure_display).-measurable A ->
 (nu1 \x nu2)%E
   ((fun
       p : 'rV[R]_m *
           'rV[R]_m =>
     p.1 + p.2) @^-1`
    A) =
 nu A) ->
forall theta : 'rV_m, cf_rV nu theta = cmul (cf_rV nu1 theta) (cf_rV nu2 theta)

For independent Y and Z of laws nu1 and nu2, the characteristic function of the law of Y + Z is the complex product of those of nu1 and nu2.

Main result

Stated in the README together with cf_rV_image.

Statement as written in the source
Lemma cf_rV_add (nu1 nu2 nu : probability 'rV[R]_m R) :
  (forall A : set 'rV[R]_m, measurable A ->
     (nu1 \x nu2)%E ((fun p => p.1 + p.2) @^-1` A) = nu A) ->
  forall theta, cf_rV nu theta = cmul (cf_rV nu1 theta) (cf_rV nu2 theta).
Used by 1 declaration in 1 file
lemma cf_rV_norm_add main result source, line 254 
forall {R : realType} {m : nat} [nu1 nu2 nu : probability 'rV_m R],
(forall A : set 'rV_m,
 (measure_matrix_display default_measure_display).-measurable A ->
 (nu1 \x nu2)%E
   ((fun
       p : 'rV[R]_m *
           'rV[R]_m =>
     p.1 + p.2) @^-1`
    A) =
 nu A) ->
forall theta : 'rV_m, cf_rV_norm nu theta = cf_rV_norm nu1 theta * cf_rV_norm nu2 theta
Main result

Stated in the README together with cf_rV_image.

Statement as written in the source
Lemma cf_rV_norm_add (nu1 nu2 nu : probability 'rV[R]_m R) :
  (forall A : set 'rV[R]_m, measurable A ->
     (nu1 \x nu2)%E ((fun p => p.1 + p.2) @^-1` A) = nu A) ->
  forall theta,
    cf_rV_norm nu theta = cf_rV_norm nu1 theta * cf_rV_norm nu2 theta.
lemma cf_rV_tuple_prod main result source, line 265 
forall {R : realType} {m : nat} [mu : nat -> probability (measurableTypeR R) R] 
  [n : nat] [w : nat -> 'rV_m] [nu : probability 'rV_m R],
(forall A : set 'rV_m,
 (measure_matrix_display default_measure_display).-measurable A ->
 tuple_prod mu n ((fun x : n.-tuple R => \sum_(k < n) tnth x k *: w k) @^-1` A) = nu A) ->
forall theta : 'rV_m,
cf_rV nu theta = \big[cmul/(1, 0)]_(k < n) cf (mu k) (mxdot (w k) theta)

Independent coordinates: for x of law tuple_prod mu n and vectors w k, the characteristic function of the law of \sum_k x_k w_k at theta is the complex product of the characteristic functions of the mu k at <w k, theta>.

Main result

Stated in the README together with cf_rV_image.

Statement as written in the source
Lemma cf_rV_tuple_prod (mu : nat -> probability (measurableTypeR R) R) n
    (w : nat -> 'rV[R]_m) (nu : probability 'rV[R]_m R) :
  (forall A : set 'rV[R]_m, measurable A ->
     tuple_prod mu n ((fun x => \sum_(k < n) tnth x k *: w k) @^-1` A) =
     nu A) ->
  forall theta,
    cf_rV nu theta = \big[cmul/(1, 0)]_(k < n) cf (mu k) (mxdot (w k) theta).
Used by 1 declaration in 1 file
lemma cf_rV_norm_tuple_prod main result source, line 292 
forall {R : realType} {m : nat} [mu : nat -> probability (measurableTypeR R) R] 
  [n : nat] [w : nat -> 'rV_m] [nu : probability 'rV_m R],
(forall A : set 'rV_m,
 (measure_matrix_display default_measure_display).-measurable A ->
 tuple_prod mu n ((fun x : n.-tuple R => \sum_(k < n) tnth x k *: w k) @^-1` A) = nu A) ->
forall theta : 'rV_m,
cf_rV_norm nu theta = \prod_(k < n) cf_norm (mu k) (mxdot (w k) theta)
Main result

Stated in the README together with cf_rV_image.

Statement as written in the source
Lemma cf_rV_norm_tuple_prod (mu : nat -> probability (measurableTypeR R) R) n
    (w : nat -> 'rV[R]_m) (nu : probability 'rV[R]_m R) :
  (forall A : set 'rV[R]_m, measurable A ->
     tuple_prod mu n ((fun x => \sum_(k < n) tnth x k *: w k) @^-1` A) =
     nu A) ->
  forall theta,
    cf_rV_norm nu theta = \prod_(k < n) cf_norm (mu k) (mxdot (w k) theta).
Used by 1 declaration in 1 file
sectionbounded_swap
Context {R : realType}.
lemma Rintegral_swap_bounded main result source, line 311 
forall {R : realType} [d1 d2 : measure_display] [T1 : measurableType d1]
  [T2 : measurableType d2] (P1 : probability T1 R) (P2 : probability T2 R)
  [F : T1 * T2 -> R] [C : R],
measurable_fun [set: T1 * T2] F ->
(forall p : T1 * T2, `|F p| <= C) ->
\int[P1]_x \int[P2]_y F (x, y) = \int[P2]_y \int[P1]_x F (x, y)

Fubini for a bounded measurable function on a product of probabilities, as an exchange of the iterated integrals.

Main result, as the README states it

Fubini for a bounded measurable function on a product of two probabilities: the two iterated integrals agree.

Statement as written in the source
Lemma Rintegral_swap_bounded d1 d2 (T1 : measurableType d1)
    (T2 : measurableType d2) (P1 : probability T1 R) (P2 : probability T2 R)
    (F : T1 * T2 -> R) (C : R) :
  measurable_fun [set: T1 * T2] F -> (forall p, `|F p| <= C) ->
  \int[P1]_x \int[P2]_y F (x, y) = \int[P2]_y \int[P1]_x F (x, y).
Used by 1 declaration in 1 file
sectiongauss_regularization
Context {R : realType} {m : nat}.
lemma cf_rV_regularization main result source, line 341 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) [s : R] (z : 'rV_m),
0 < s ->
\int[nu]_y expR (- mxdot (z - y) (z - y) / (2 * s ^+ 2)) =
\int[gauss m]_g
   (cos (mxdot (s^-1 *: g) z) * cf_rV_re nu (s^-1 *: g) +
    sin (mxdot (s^-1 *: g) z) * cf_rV_im nu (s^-1 *: g))

The Gaussian regularization identity: for Y of law nu and G of law gauss m, independent, E[exp (- |z - Y|^2 / (2 s^2))] is the Gaussian average of cos <G/s, z> cf_re (G/s) + sin <G/s, z> cf_im (G/s).

Main result, as the README states it

Gaussian regularization: for Y of law nu, G of law gauss m and s > 0, E[exp (- |z - Y|^2 / (2 s^2))] = E[cos <G/s, z> cf_rV_re nu (G/s) + sin <G/s, z> cf_rV_im nu (G/s)], hence it is at most (s / sqrt (2 pi))^m \int |cf_rV nu theta| exp (- s^2 |theta|^2 / 2) dtheta, where |.| is the Euclidean norm.

Statement as written in the source
Lemma cf_rV_regularization (nu : probability 'rV[R]_m R) (s : R)
    (z : 'rV[R]_m) : 0 < s ->
  \int[nu]_y expR (- mxdot (z - y) (z - y) / (2 * s ^+ 2)) =
  \int[gauss m]_g (cos (mxdot (s^-1 *: g) z) * cf_rV_re nu (s^-1 *: g) +
                   sin (mxdot (s^-1 *: g) z) * cf_rV_im nu (s^-1 *: g)).
Used by 2 declarations in 2 files
lemma gauss_pdf_scale main result source, line 377 
forall {R : realType} {m : nat} [s : R] (v : 'rV_m),
0 < s ->
gauss_pdf (s^-1 *: v) =
Num.ExtraDef.sqrtr (2 * pi) ^- m * expR (- mxdot v v / (2 * s ^+ 2))
Main result, as the README states it

The law of y + s G, for G of law gauss m and s > 0, has the density w |-> s^-m gauss_pdf ((w - y) / s) with respect to lebesgue_rV m.

Statement as written in the source
Lemma gauss_pdf_scale (s : R) (v : 'rV[R]_m) : 0 < s ->
  gauss_pdf (s^-1 *: v) =
  Num.sqrt (2 * pi) ^- m * expR (- mxdot v v / (2 * s ^+ 2)).
Used by 2 declarations in 2 files
Local Open Scope ereal_scope.
lemma ge0_integral_gauss_affine main result source, line 389 
forall {R : realType} {m : nat} (y : 'rV_m) [s : R] [f : 'rV_m -> \bar R],
0 < s ->
measurable_fun [set: 'rV_m] f ->
(forall x : 'rV_m, (0%R <= f x)%E) ->
(\int[gauss m]_g f (y + s *: g)%R)%E =
((s ^- m)%:E * \int[lebesgue_rV m]_w (f w * (gauss_pdf (s^-1 *: (w - y)))%:E))%E

The law of y + s G, for G of law gauss m and s > 0, has the density w |-> s^-m gauss_pdf ((w - y) / s).

Main result

Stated in the README together with gauss_pdf_scale.

Statement as written in the source
Lemma ge0_integral_gauss_affine (y : 'rV[R]_m) (s : R)
    (f : 'rV[R]_m -> \bar R) :
  (0 < s)%R -> measurable_fun [set: 'rV[R]_m] f -> (forall x, 0 <= f x) ->
  \int[gauss m]_g f (y + s *: g)%R =
  (s ^- m)%:E * \int[lebesgue_rV m]_w (f w * (gauss_pdf (s^-1 *: (w - y)))%:E).
Used by 4 declarations in 2 files
lemma cf_rV_regularization_le main result source, line 426 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) [s : R] (z : 'rV_m),
0 < s ->
((\int[nu]_y expR (- mxdot (z - y) (z - y) / (2 * s ^+ 2)))%:E <=
 ((s / Num.ExtraDef.sqrtr (2 * pi)) ^+ m)%:E *
 \int[lebesgue_rV m]_th (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_norm nu th)%:E)%E

The bound behind the inequality of Ball and Nazarov: the Gaussian average of exp (- |z - Y|^2 / (2 s^2)) is at most (s / sqrt (2 pi))^m times the integral of |cf nu| exp (- s^2 |theta|^2 / 2).

Main result

Stated in the README together with cf_rV_regularization.

Statement as written in the source
Lemma cf_rV_regularization_le (nu : probability 'rV[R]_m R) (s : R)
    (z : 'rV[R]_m) : (0 < s)%R ->
  (\int[nu]_y expR (- mxdot (z - y) (z - y) / (2 * s ^+ 2)))%:E <=
  ((s / Num.sqrt (2 * pi)) ^+ m)%:E *
  \int[lebesgue_rV m]_th
    (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_norm nu th)%:E.
Used by 1 declaration in 1 file
lemma prod_gauss_le_cf_rV main result source, line 510 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) [s : R] [B : set 'rV_m],
0 < s ->
(measure_matrix_display default_measure_display).-measurable B ->
((nu \x gauss m) [set p | B (p.1 + s *: p.2)%R] <=
 ((2 * pi) ^- m)%:E *
 \int[lebesgue_rV m]_th (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_norm nu th)%:E *
 lebesgue_rV m B)%E

Gaussian regularization: for Y of law nu and G of law gauss m, independent, P(Y + s G in B) is at most (2 pi)^-m times the integral of |cf nu| exp (- s^2 |theta|^2 / 2), times the Lebesgue measure of B.

Main result, as the README states it

For Y of law nu and an independent G of law gauss m, s > 0 and a measurable B, P(Y + s G in B) <= (2 pi)^-m (\int |cf_rV nu theta| exp (- s^2 |theta|^2 / 2) dtheta) lebesgue_rV m B, with values in [0, +oo]. No Fourier inversion is used.

Statement as written in the source
Lemma prod_gauss_le_cf_rV (nu : probability 'rV[R]_m R) (s : R)
    (B : set 'rV[R]_m) : (0 < s)%R -> measurable B ->
  (nu \x gauss m) [set p | B (p.1 + s *: p.2)%R] <=
  ((2 * pi) ^- m)%:E *
  \int[lebesgue_rV m]_th
    (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_norm nu th)%:E *
  lebesgue_rV m B.
Used by 2 declarations in 2 files
sectionball_cf_rV
Context {R : realType} {m : nat}.
let measurable_mxdot_self section-local source, line 650 
Let measurable_mxdot_self :
  measurable_fun [set: 'rV[R]_m] (fun x => mxdot x x).
Used by 3 declarations in 1 file
lemma measurable_ball_rV main result source, line 657 
forall {R : realType} {m : nat} (z : 'rV_m) (r : R),
(measure_matrix_display default_measure_display).-measurable
  [set y | frobenius (y - z) <= r]
Main result, as the README states it

Closed Euclidean balls are measurable, and scaling the radius by a > 0 multiplies their Lebesgue measure by a^m. For G of law gauss m, E[|G|^2] = m and P(|G| <= t) >= 1 - m / t^2.

Statement as written in the source
Lemma measurable_ball_rV (z : 'rV[R]_m) (r : R) :
  measurable [set y : 'rV[R]_m | frobenius (y - z) <= r].
Used by 6 declarations in 2 files
lemma lebesgue_rV_ball_scale main result source, line 676 
forall {R : realType} {m : nat} (z : 'rV_m) [r a : R],
0 <= r ->
0 < a ->
lebesgue_rV m [set y | frobenius (y - z) <= a * r] =
((a ^+ m)%:E * lebesgue_rV m [set y | (frobenius (y - z) <= r)%R])%E

Scaling the radius of a ball by a > 0 multiplies its measure by a^m.

Main result

Stated in the README together with measurable_ball_rV.

Statement as written in the source
Lemma lebesgue_rV_ball_scale (z : 'rV[R]_m) (r a : R) : 0 <= r -> 0 < a ->
  lebesgue_rV m [set y | frobenius (y - z) <= a * r] =
  ((a ^+ m)%:E * lebesgue_rV m [set y | (frobenius (y - z) <= r)%R])%E.
Used by 1 declaration in 1 file
lemma integral_gauss_mxdot_self main result source, line 699 
forall {R : realType} {m : nat}, (\int[gauss m]_g (mxdot g g)%:E)%E = (m%:R)%:E
Main result

Stated in the README together with measurable_ball_rV.

Statement as written in the source
Lemma integral_gauss_mxdot_self :
  (\int[@gauss R m]_g (mxdot g g)%:E = m%:R%:E)%E.
Used by 3 declarations in 3 files
lemma gauss_frobenius_ge main result source, line 717 
forall {R : realType} {m : nat} [t : R],
0 < t -> ((1 - m%:R / t ^+ 2)%:E <= gauss m [set g | (frobenius g <= t)%R])%E

Markov's inequality for |G|^2, G of law gauss m.

Main result

Stated in the README together with measurable_ball_rV.

Statement as written in the source
Lemma gauss_frobenius_ge (t : R) : 0 < t ->
  ((1 - m%:R / t ^+ 2)%:E <=
   @gauss R m [set g : 'rV[R]_m | (frobenius g <= t)%R])%E.
Used by 2 declarations in 2 files
let pow1D_le section-local source, line 768 
Let pow1D_le (e : R) n : 0 <= e -> e <= 1 ->
  (1 + e) ^+ n <= 1 + e * (n%:R * 2 ^+ n).
Used by 1 declaration in 1 file
let le_of_le_mul section-local source, line 781 
Let le_of_le_mul (x c : R) n : 0 <= x -> 0 <= c ->
  (forall e, 0 < e -> e <= 2^-1 -> x * (1 - e) <= c * (1 + e) ^+ n) ->
  x <= c.
Used by 1 declaration in 1 file
lemma ball_le_cf_rV main result source, line 805 
forall {R : realType} {m : nat} [nu : probability 'rV_m R] (z : 'rV_m) [r : R],
0 < r ->
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
(nu [set y | (frobenius (y - z) <= r)%R] <=
 ((2 * pi) ^- m)%:E * \int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E *
 lebesgue_rV m [set y | (frobenius (y - z) <= r)%R])%E

If |cf nu| is integrable, a closed ball has probability at most (2 pi)^-m (\int |cf nu|) times its Lebesgue measure.

Main result, as the README states it

If \int |cf_rV nu| < +oo, every closed Euclidean ball B of radius r > 0 satisfies nu B <= (2 pi)^-m (\int |cf_rV nu theta| dtheta) lebesgue_rV m B: prod_gauss_le_cf_rV with s -> 0.

Statement as written in the source
Lemma ball_le_cf_rV (nu : probability 'rV[R]_m R) (z : 'rV[R]_m) (r : R) :
  0 < r ->
  (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
  (nu [set y | (frobenius (y - z) <= r)%R] <=
   ((2 * pi) ^- m)%:E * \int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E *
   lebesgue_rV m [set y | (frobenius (y - z) <= r)%R])%E.
Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.