GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisfourierinversion

The Fourier inversion theorem on row vectors

GaussianAnalysis.fourier.inversionlibrary/fourier/inversion.v1,050 lines24 lemmas and theorems, 4 definitionssource
Imports 13 library modules and 35 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.charge, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.probability_theory.normal_distribution

Let nu be a law on 'rV[R]_m whose characteristic function is integrable: \int |cf nu theta| dtheta < +oo against lebesgue_rV m. Then nu has the density cf_rV_density nu with respect to lebesgue_rV m (cf_rV_inversion):

cf_rV_density nu w = (2 pi)^-m \int (cos <theta, w> cf_rV_re nu theta
                        + sin <theta, w> cf_rV_im nu theta) dtheta.

This density is continuous (continuous_cf_rV_density), nonnegative (cf_rV_density_ge0), of integral one (integral_cf_rV_density), and bounded by (2 pi)^-m \int |cf nu| (cf_rV_density_le).

The proof uses no complex numbers and no Fourier transform of functions. For s > 0 the regularized density, the same integral with the factor exp (- s^2 |theta|^2 / 2), is the density s^-m E[gauss_pdf ((w - Y) / s)] of Y + s G, for Y of law nu and G of law gauss m independent (cf_rV_density_regE, integral_add_gauss), and it is also the average of cf_rV_density over w + s G (integral_cf_rV_density_gauss). It tends to cf_rV_density as s tends to 0 (cvg_cf_rV_density_reg), which gives the nonnegativity; the average gives the total mass. Hence Y + s G has the same law for Y of law nu and for Y of law cf_rV_inv_prob h, the probability with density cf_rV_density nu (integral_gauss_pdf_inv_prob). For a Lipschitz test function with values in [0, 1], the expectation under either law is within |L| s (1 + m) / 2 of the expectation of the smoothed variable (lipschitz_add_gauss), and measure_lipschitz_unique concludes.

cf_rV_kernel nu w thetacos <theta, w> cf_rV_re nu theta + sin <theta, w> cf_rV_im nu theta
cf_rV_density nu w(2 pi)^-m \int cf_rV_kernel nu w theta dtheta
cf_rV_density_reg nu s wthe same, with the factor exp (- s^2 |theta|^2 / 2)
cf_rV_inv_prob hfor h : \int |cf nu| < +oo, the probability with density cf_rV_density nu

Main results

ResultsStatement
cf_rV_inversion
The Fourier inversion theorem on row vectors: if \int |cf_rV nu theta| dtheta < +oo against lebesgue_rV m, then nu X = \int_X cf_rV_density nu w dw for every measurable X, with cf_rV_density nu w = (2 pi)^-m \int (cos <theta, w> cf_rV_re nu theta + sin <theta, w> cf_rV_im nu theta) dtheta.
cf_rV_density_lecontinuous_cf_rV_densitycf_rV_density_ge0integral_cf_rV_densitycf_rV_inv_prob
The density is bounded by (2 pi)^-m \int |cf_rV nu|, continuous, nonnegative and of integral one; cf_rV_inv_prob h is the probability it defines.
cf_rV_density_regcf_rV_density_regEcvg_cf_rV_density_regintegral_cf_rV_density_gaussintegral_cf_rV_kernel_gauss
Gaussian regularization of the density: for s > 0, (2 pi)^-m \int exp (- s^2 |theta|^2 / 2) (...) dtheta is the density s^-m E[gauss_pdf ((w - Y) / s)] of Y + s G, it is the average of cf_rV_density nu over w + s G, and it tends to cf_rV_density nu w as s -> 0.
integral_add_gausslipschitz_add_gauss
For any law mu on 'rV[R]_m and G of law gauss m: E[phi (Y + s G)] = s^-m \int phi w E[gauss_pdf ((w - Y) / s)] dw for nonnegative measurable phi, and |E[phi (Y + s G)] - E[phi Y]| <= |L| s (1 + m) / 2 for phi with values in [0, 1] and Lipschitz with constant L.

Declarations30 exported, 13 local

lemma, theoremdefinitioninstancelocal
sectioncf_rV_density
Context {R : realType} {m : nat}.
Variable nu : probability 'rV[R]_m R.
definition cf_rV_kernel source, line 75
Type
forall {R : realType} {m : nat}, probability 'rV_m R -> 'rV_m -> 'rV_m -> R
Definition
Definition cf_rV_kernel (w th : 'rV[R]_m) : R :=
  cos (mxdot th w) * cf_rV_re nu th + sin (mxdot th w) * cf_rV_im nu th.

The integrand of the inversion formula at w: the real part of exp (- i <theta, w>) cf nu theta.

Used by 12 declarations in 1 file
lemma cf_rV_kernel_le source, line 79 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) (w th : 'rV_m),
`|cf_rV_kernel nu w th| <= cf_rV_norm nu th

It is bounded by |cf nu theta|.

Statement as written in the source
Lemma cf_rV_kernel_le w th : `|cf_rV_kernel w th| <= cf_rV_norm nu th.
Used by 7 declarations in 1 file
lemma measurable_cf_rV_kernel source, line 85 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) (w : 'rV_m),
measurable_fun [set: 'rV_m] (cf_rV_kernel nu w)
Statement as written in the source
Lemma measurable_cf_rV_kernel w :
  measurable_fun [set: 'rV[R]_m] (cf_rV_kernel w).
Used by 6 declarations in 1 file

From here on, |cf nu| is integrable.

Hypothesis int_cf :
  (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E.
lemma integrable_cf_rV_norm source, line 99 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
(lebesgue_rV m).-integrable [set: 'rV_m] (EFin \o cf_rV_norm nu)
Statement as written in the source
Lemma integrable_cf_rV_norm :
  (lebesgue_rV m).-integrable [set: 'rV[R]_m] (EFin \o cf_rV_norm nu).
Used by 6 declarations in 1 file
lemma integrable_cf_rV_kernel source, line 112 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
forall w : 'rV_m, (lebesgue_rV m).-integrable [set: 'rV_m] (EFin \o cf_rV_kernel nu w)
Statement as written in the source
Lemma integrable_cf_rV_kernel w :
  (lebesgue_rV m).-integrable [set: 'rV[R]_m] (EFin \o cf_rV_kernel w).
Used by 3 declarations in 1 file
definition cf_rV_density source, line 122
Type
forall {R : realType} {m : nat}, probability 'rV_m R -> 'rV_m -> R
Definition
Definition cf_rV_density (w : 'rV[R]_m) : R :=
  (2 * pi) ^- m * \int[lebesgue_rV m]_th cf_rV_kernel w th.

The density given by the inversion formula.

Used by 13 declarations in 1 file
lemma cf_rV_density_le main result source, line 126 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
forall w : 'rV_m,
`|cf_rV_density nu w| <= (2 * pi) ^- m * \int[lebesgue_rV m]_th cf_rV_norm nu th

The density is bounded by (2 pi)^-m \int |cf nu|.

Main result, as the README states it

The density is bounded by (2 pi)^-m \int |cf_rV nu|, continuous, nonnegative and of integral one; cf_rV_inv_prob h is the probability it defines.

Statement as written in the source
Lemma cf_rV_density_le w :
  `|cf_rV_density w| <=
  (2 * pi) ^- m * \int[lebesgue_rV m]_th cf_rV_norm nu th.
Used by 2 declarations in 1 file
let measurable_mxdot_self section-local source, line 145 
Let measurable_mxdot_self :
  measurable_fun [set: 'rV[R]_m] (fun x => mxdot x x).
Used by 2 declarations in 1 file
let continuous_mxdotr section-local source, line 152 
Let continuous_mxdotr (x : 'rV[R]_m) :
  continuous (fun theta : 'rV[R]_m => mxdot x theta).
Used by 1 declaration in 1 file
lemma continuous_cf_rV_density main result source, line 162 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E -> continuous (cf_rV_density nu)

The density is continuous, by dominated convergence.

Main result

Stated in the README together with cf_rV_density_le.

Statement as written in the source
Lemma continuous_cf_rV_density : continuous cf_rV_density.
Used by 1 declaration in 1 file
definition cf_rV_density_reg main result source, line 192
Type
forall {R : realType} {m : nat}, probability 'rV_m R -> R -> 'rV_m -> R
Definition
Definition cf_rV_density_reg (s : R) (w : 'rV[R]_m) : R :=
  (2 * pi) ^- m * \int[lebesgue_rV m]_th
    (expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_kernel w th).

The regularized density: (2 pi)^-m times the integral of exp (- s^2 |theta|^2 / 2) times the kernel.

Main result, as the README states it

Gaussian regularization of the density: for s > 0, (2 pi)^-m \int exp (- s^2 |theta|^2 / 2) (...) dtheta is the density s^-m E[gauss_pdf ((w - Y) / s)] of Y + s G, it is the average of cf_rV_density nu over w + s G, and it tends to cf_rV_density nu w as s -> 0.

Used by 6 declarations in 1 file
lemma cf_rV_density_reg0 source, line 196 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) (w : 'rV_m),
cf_rV_density_reg nu 0 w = cf_rV_density nu w
Statement as written in the source
Lemma cf_rV_density_reg0 w : cf_rV_density_reg 0 w = cf_rV_density w.
Used by 1 declaration in 1 file
lemma cvg_cf_rV_density_reg main result source, line 203 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
forall [w : 'rV_m], cf_rV_density_reg nu s w @[s --> 0] --> cf_rV_density nu w

The regularized density tends to the density as s tends to 0.

Main result

Stated in the README together with cf_rV_density_reg.

Statement as written in the source
Lemma cvg_cf_rV_density_reg w :
  cf_rV_density_reg s w @[s --> 0] --> cf_rV_density w.
Used by 1 declaration in 1 file
let measurable_rV_subl section-local source, line 250 
Let measurable_rV_subl (w : 'rV[R]_m) :
  measurable_fun [set: 'rV[R]_m] (fun y : 'rV[R]_m => w - y).
Used by 2 declarations in 1 file
let measurable_mxdot2 section-local source, line 260 
Let measurable_mxdot2 d (T : measurableType d) (f g : T -> 'rV[R]_m) :
  measurable_fun [set: T] f -> measurable_fun [set: T] g ->
  measurable_fun [set: T] (fun x => mxdot (f x) (g x)).
Used by 2 declarations in 1 file
let reg_le section-local source, line 270 
Let reg_le (s : R) w th :
  `|expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_kernel w th| <=
  cf_rV_norm nu th.
Used by 1 declaration in 1 file
let integrable_reg section-local source, line 280 
Let integrable_reg (s : R) w : (lebesgue_rV m).-integrable [set: 'rV[R]_m]
  (EFin \o (fun th => expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_kernel w th)).
Used by 1 declaration in 1 file
lemma cf_rV_density_regE main result source, line 297 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
forall [s : R] (w : 'rV_m),
0 < s -> cf_rV_density_reg nu s w = s ^- m * \int[nu]_y gauss_pdf (s^-1 *: (w - y))

For s > 0, the regularized density is the density of the law of Y + s G, for Y of law nu and G of law gauss m, independent: w |-> s^-m E[gauss_pdf ((w - Y) / s)].

Main result

Stated in the README together with cf_rV_density_reg.

Statement as written in the source
Lemma cf_rV_density_regE (s : R) w : 0 < s ->
  cf_rV_density_reg s w = s ^- m * \int[nu]_y gauss_pdf (s^-1 *: (w - y)).
Used by 3 declarations in 1 file
lemma integral_cf_rV_kernel_gauss main result source, line 370 
forall {R : realType} {m : nat} (nu : probability 'rV_m R) (s : R)
  (w : 'rV[R]_m) (th : 'rV_m),
\int[gauss m]_g cf_rV_kernel nu (w + s *: g) th =
expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_kernel nu w th

The Gaussian side: E[cf_rV_kernel (w + s G) theta] for G of law gauss m is exp (- s^2 |theta|^2 / 2) cf_rV_kernel w theta.

Main result

Stated in the README together with cf_rV_density_reg.

Statement as written in the source
Lemma integral_cf_rV_kernel_gauss (s : R) w th :
  \int[gauss m]_g cf_rV_kernel (w + s *: g) th =
  expR (- s ^+ 2 * mxdot th th / 2) * cf_rV_kernel w th.
Used by 1 declaration in 1 file
lemma integral_cf_rV_density_gauss main result source, line 419 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
forall (s : R) (w : 'rV[R]_m),
\int[gauss m]_g cf_rV_density nu (w + s *: g) = cf_rV_density_reg nu s w

Convolution: the density at w + s G, averaged over G of law gauss m, is the regularized density at w.

Main result

Stated in the README together with cf_rV_density_reg.

Statement as written in the source
Lemma integral_cf_rV_density_gauss (s : R) w :
  \int[gauss m]_g cf_rV_density (w + s *: g) = cf_rV_density_reg s w.
Used by 2 declarations in 1 file
lemma cf_rV_density_ge0 main result source, line 464 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
forall w : 'rV_m, 0 <= cf_rV_density nu w

The density is nonnegative, as a limit of the densities of Y + s G.

Main result

Stated in the README together with cf_rV_density_le.

Statement as written in the source
Lemma cf_rV_density_ge0 w : 0 <= cf_rV_density w.
Used by 4 declarations in 1 file
lemma measurable_cf_rV_density source, line 476 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
measurable_fun [set: 'rV_m] (cf_rV_density nu)
Statement as written in the source
Lemma measurable_cf_rV_density :
  measurable_fun [set: 'rV[R]_m] cf_rV_density.
Used by 6 declarations in 1 file
lemma integral_cf_rV_density main result source, line 481 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
(\int[lebesgue_rV m]_w (cf_rV_density nu w)%:E)%E = 1%E

The density has integral one.

Main result

Stated in the README together with cf_rV_density_le.

Statement as written in the source
Lemma integral_cf_rV_density :
  (\int[lebesgue_rV m]_w (cf_rV_density w)%:E = 1)%E.
Used by 1 declaration in 1 file
definition cf_rV_inv_prob main result source, line 570
Type
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E -> set 'rV_m -> \bar R
Definition
Definition cf_rV_inv_prob
    (h : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E) :
    set 'rV[R]_m -> \bar R :=
  fun A => (\int[lebesgue_rV m]_(w in A) (cf_rV_density w)%:E)%E.

The law with density cf_rV_density with respect to lebesgue_rV m; the proof h of the integrability of |cf nu| makes it a probability.

Main result

Stated in the README together with cf_rV_density_le.

Used by 11 declarations in 1 file
sectioncf_rV_inv_prob
Context {R : realType} {m : nat} (nu : probability 'rV[R]_m R).
Variable h : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E.
lemma cf_rV_inv_prob0 source, line 581 
forall {R : realType} {m : nat} [nu : probability 'rV_m R]
  (h : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E),
cf_rV_inv_prob h set0 = 0
Statement as written in the source
Lemma cf_rV_inv_prob0 : cf_rV_inv_prob h set0 = 0%E.
Used by 1 declaration in 1 file
lemma cf_rV_inv_prob_ge0 source, line 584 
forall {R : realType} {m : nat} [nu : probability 'rV_m R]
  (h : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E) 
  (A : set 'rV_m),
(0%R <= cf_rV_inv_prob h A)%E
Statement as written in the source
Lemma cf_rV_inv_prob_ge0 A : (0 <= cf_rV_inv_prob h A)%E.
Used by 1 declaration in 1 file
lemma cf_rV_inv_prob_sigma source, line 589 
forall {R : realType} {m : nat} [nu : probability 'rV_m R]
  [h : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E],
semi_sigma_additive (cf_rV_inv_prob h)
Statement as written in the source
Lemma cf_rV_inv_prob_sigma : semi_sigma_additive (cf_rV_inv_prob h).
Used by 1 declaration in 1 file
lemma cf_rV_inv_prob_setT source, line 596 
forall {R : realType} {m : nat} [nu : probability 'rV_m R]
  (h : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E),
cf_rV_inv_prob h [set: 'rV_m] = 1%E
Statement as written in the source
Lemma cf_rV_inv_prob_setT : cf_rV_inv_prob h [set: 'rV[R]_m] = 1%E.
Used by 1 declaration in 1 file

HB declares canonical projections that the structures of the measure already provide; the warning says so. The setting lasts until the end of this file and is not exported.

Set Warnings "-redundant-canonical-projection".
instance instance at line 606 source, line 606 
HB.instance Definition _ (R : realType) (m : nat)
    (nu : probability 'rV[R]_m R)
    (h : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E) :=
  isMeasure.Build _ _ _ (@cf_rV_inv_prob R m nu h)
    (@cf_rV_inv_prob0 R m nu h) (@cf_rV_inv_prob_ge0 R m nu h)
    (@cf_rV_inv_prob_sigma R m nu h).
instance instance at line 613 source, line 613 
HB.instance Definition _ (R : realType) (m : nat)
    (nu : probability 'rV[R]_m R)
    (h : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E) :=
  Measure_isProbability.Build _ _ _ (@cf_rV_inv_prob R m nu h)
    (@cf_rV_inv_prob_setT R m nu h).
sectionadd_gauss
Context {R : realType} {m : nat}.
let measurable_mxdot_self section-local source, line 623 
Let measurable_mxdot_self :
  measurable_fun [set: 'rV[R]_m] (fun x => mxdot x x).
Used by 1 declaration in 1 file
let measurable_rV_subl section-local source, line 630 
Let measurable_rV_subl (w : 'rV[R]_m) :
  measurable_fun [set: 'rV[R]_m] (fun y : 'rV[R]_m => w - y).
Used by 1 declaration in 1 file
let msub2 section-local source, line 640 
Let msub2 : measurable_fun [set: 'rV[R]_m * 'rV[R]_m]
  (fun q : 'rV[R]_m * 'rV[R]_m => q.2 - q.1).
Used by 1 declaration in 1 file
let pdf_le2 section-local source, line 652 
Let pdf_le2 (x : 'rV[R]_m) : `|gauss_pdf x| <= Num.sqrt (2 * pi) ^- m.
Used by 1 declaration in 1 file
lemma integral_add_gauss main result source, line 662 
forall {R : realType} {m : nat} (mu : probability 'rV_m R) [phi : 'rV_m -> R] [s : R],
0 < s ->
measurable_fun [set: 'rV_m] phi ->
(forall x : 'rV_m, 0 <= phi x) ->
(\int[mu]_y \int[gauss m]_g (phi (y + s *: g))%:E)%E =
((s ^- m)%:E *
 \int[lebesgue_rV m]_w ((phi w)%:E * (\int[mu]_y gauss_pdf (s^-1 *: (w - y)))%:E))%E

For Y of law mu and G of law gauss m, independent, and s > 0, the law of Y + s G has the density w |-> s^-m E[gauss_pdf ((w - Y) / s)].

Main result, as the README states it

For any law mu on 'rV[R]_m and G of law gauss m: E[phi (Y + s G)] = s^-m \int phi w E[gauss_pdf ((w - Y) / s)] dw for nonnegative measurable phi, and |E[phi (Y + s G)] - E[phi Y]| <= |L| s (1 + m) / 2 for phi with values in [0, 1] and Lipschitz with constant L.

Statement as written in the source
Lemma integral_add_gauss (mu : probability 'rV[R]_m R)
    (phi : 'rV[R]_m -> R) (s : R) :
  0 < s -> measurable_fun [set: 'rV[R]_m] phi -> (forall x, 0 <= phi x) ->
  (\int[mu]_y \int[gauss m]_g (phi (y + s *: g))%:E =
   (s ^- m)%:E * \int[lebesgue_rV m]_w
     ((phi w)%:E * (\int[mu]_y gauss_pdf (s^-1 *: (w - y)))%:E))%E.
Used by 1 declaration in 1 file
lemma lipschitz_add_gauss main result source, line 710 
forall {R : realType} {m : nat} (mu : probability 'rV_m R) [phi : 'rV_m -> R] [L s : R],
0 < s ->
(forall x : 'rV_m, 0 <= phi x <= 1) ->
(forall x y : 'rV_m, `|phi x - phi y| <= L * frobenius (x - y)) ->
`|\int[mu]_y \int[gauss m]_g phi (y + s *: g) - \int[mu]_y phi y| <=
`|L| * s * (1 + m%:R) / 2

For a law mu, s > 0 and phi with values in [0, 1] and Lipschitz with constant L: |E[phi (Y + s G)] - E[phi Y]| <= |L| s (1 + m) / 2.

Main result

Stated in the README together with integral_add_gauss.

Statement as written in the source
Lemma lipschitz_add_gauss (mu : probability 'rV[R]_m R)
    (phi : 'rV[R]_m -> R) (L s : R) :
  0 < s -> (forall x, 0 <= phi x <= 1) ->
  (forall x y, `|phi x - phi y| <= L * frobenius (x - y)) ->
  `|\int[mu]_y \int[gauss m]_g phi (y + s *: g) - \int[mu]_y phi y| <=
  `|L| * s * (1 + m%:R) / 2.
Used by 1 declaration in 1 file
sectioncf_rV_inversion
Context {R : realType} {m : nat}.
Variable nu : probability 'rV[R]_m R.
Hypothesis int_cf :
  (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E.
Local Notation P := (cf_rV_inv_prob int_cf).
let measurable_rV_subl section-local source, line 854 
Let measurable_rV_subl (w : 'rV[R]_m) :
  measurable_fun [set: 'rV[R]_m] (fun y : 'rV[R]_m => w - y).
Used by 1 declaration in 1 file
lemma cf_rV_inv_prob_dominates source, line 866 
forall {R : realType} {m : nat} [nu : probability 'rV_m R]
  (int_cf : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E),
cf_rV_inv_prob int_cf `<< lebesgue_rV m

The law with density cf_rV_density nu is absolutely continuous with respect to lebesgue_rV m, and integrals against it carry the density.

Statement as written in the source
Lemma cf_rV_inv_prob_dominates : P `<< lebesgue_rV m.
Used by 2 declarations in 1 file
let RN_density section-local source, line 874 
Let RN_density : ae_eq (lebesgue_rV m) [set: 'rV[R]_m]
  (Radon_Nikodym_SigmaFinite.f P (lebesgue_rV m))
  (fun w => (cf_rV_density nu w)%:E).
Used by 1 declaration in 1 file
lemma ge0_integral_cf_rV_inv_prob source, line 887 
forall {R : realType} {m : nat} [nu : probability 'rV_m R]
  (int_cf : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E) 
  [g : 'rV_m -> \bar R],
measurable_fun [set: 'rV_m] g ->
(forall x : 'rV_m, (0%R <= g x)%E) ->
(\int[cf_rV_inv_prob int_cf]_x g x)%E =
(\int[lebesgue_rV m]_x (g x * (cf_rV_density nu x)%:E))%E
Statement as written in the source
Lemma ge0_integral_cf_rV_inv_prob (g : 'rV[R]_m -> \bar R) :
  measurable_fun [set: 'rV[R]_m] g -> (forall x, 0 <= g x)%E ->
  (\int[P]_x g x = \int[lebesgue_rV m]_x (g x * (cf_rV_density nu x)%:E))%E.
Used by 1 declaration in 1 file
lemma integral_gauss_pdf_inv_prob source, line 904 
forall {R : realType} {m : nat} [nu : probability 'rV_m R]
  (int_cf : (\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E) 
  [s : R] (w : 'rV[R]_m),
0 < s ->
\int[cf_rV_inv_prob int_cf]_y gauss_pdf (s^-1 *: (w - y)) =
\int[nu]_y gauss_pdf (s^-1 *: (w - y))

The densities of Y + s G for Y of law nu and for Y of law P coincide.

Statement as written in the source
Lemma integral_gauss_pdf_inv_prob (s : R) w : 0 < s ->
  \int[P]_y gauss_pdf (s^-1 *: (w - y)) =
  \int[nu]_y gauss_pdf (s^-1 *: (w - y)).
Used by 1 declaration in 1 file
let smooth_EFin section-local source, line 953 
Let smooth_EFin (mu : probability 'rV[R]_m R) (Phi : 'rV[R]_m -> R) (s : R) :
  0 < s -> (forall x, 0 <= Phi x <= 1) -> measurable_fun [set: 'rV[R]_m] Phi ->
  (\int[mu]_y \int[gauss m]_g Phi (y + s *: g))%:E =
  ((s ^- m)%:E * \int[lebesgue_rV m]_w
    ((Phi w)%:E * (\int[mu]_y gauss_pdf (s^-1 *: (w - y)))%:E))%E.
Used by 1 declaration in 1 file
theorem cf_rV_inversion main result source, line 998 
forall {R : realType} {m : nat} [nu : probability 'rV_m R],
(\int[lebesgue_rV m]_th (cf_rV_norm nu th)%:E < +oo)%E ->
forall [X : set 'rV_m],
(measure_matrix_display default_measure_display).-measurable X ->
nu X = (\int[lebesgue_rV m]_(w in X) (cf_rV_density nu w)%:E)%E

The inversion theorem: if |cf nu| is integrable with respect to Lebesgue measure, then nu has the density cf_rV_density nu.

Main result, as the README states it

The Fourier inversion theorem on row vectors: if \int |cf_rV nu theta| dtheta < +oo against lebesgue_rV m, then nu X = \int_X cf_rV_density nu w dw for every measurable X, with cf_rV_density nu w = (2 pi)^-m \int (cos <theta, w> cf_rV_re nu theta + sin <theta, w> cf_rV_im nu theta) dtheta.

Statement as written in the source
Theorem cf_rV_inversion (X : set 'rV[R]_m) : measurable X ->
  nu X = (\int[lebesgue_rV m]_(w in X) (cf_rV_density nu w)%:E)%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.