On this page

Lebesgue measure on row vectors

GaussianAnalysis.gaussian.lebesgue_rVlibrary/gaussian/lebesgue_rV.v923 lines38 lemmas and theorems, 4 definitionssource

Imports 5 library modules and 32 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.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 4

lebesgue_rV n is Lebesgue measure on 'rV[R]_n, built as gauss n is: the image of the product of Lebesgue measure on the line (first coordinate) and lebesgue_rV n' (the others) under rV_cons. It is sigma-finite, gives a box the product of the lengths of its sides (lebesgue_rV_box), and it is the only measure that does (lebesgue_rV_unique). Integrals against it are iterated integrals over the first coordinate and the others (ge0_integral_lebesgue_rV_cons), or over two blocks of coordinates (ge0_integral_lebesgue_rV_row_mx); the integral of a product of functions of the coordinates is the product of their integrals (ge0_integral_lebesgue_rV_prod).

It is invariant under translations (lebesgue_rV_shift) and permutations of the coordinates (lebesgue_rV_col_perm), and x |-> a x multiplies it by |a|^-n (lebesgue_rV_scale). The standard Gaussian measure gauss n has the density gauss_pdf with respect to it (ge0_integral_gauss_pdf, gauss_lebesgue_rV). Finally, the integral of exp (- frobenius (x - z) ^ 2 / (2 s^2)) is (sqrt (2 pi) s)^n (lebesgue_rV_gauss_integral), and the closed Euclidean ball of radius r has measure at most (sqrt (2 pi e / n) r)^n (lebesgue_rV_ball_le). Here frobenius x is the Euclidean norm of x (matrix/euclidean.v), and frobenius x ^ 2 = mxdot x x.

`lebesgue_rV_cons m`	the image of lebesgue_measure \x m under rV_cons, for a sigma-finite measure m on 'rV[R]_n
`lebesgue_rV_rec n`	Lebesgue measure on 'rV[R]_n as a sigma-finite measure, by recursion on n
`lebesgue_rV n`	the function of lebesgue_rV_rec n, with the same structure; the lemmas are stated for it
`gauss_pdf x`	(2 pi)^(-n/2) exp (- mxdot x x / 2), the density of gauss n with respect to lebesgue_rV n

Main results

Results	Statement
lebesgue_rVlebesgue_rV_boxlebesgue_rV_unique	`lebesgue_rV n`, Lebesgue measure on `'rV[R]_n`, a sigma-finite measure built as `gauss n` is. A box with measurable sides `A i` has measure `\prod_i lebesgue_measure (A i)`, and every measure on `'rV[R]_n` that gives the boxes these values agrees with `lebesgue_rV n` on all measurable sets.
ge0_integral_lebesgue_rV_consintegral_lebesgue_rV_conslebesgue_rV_row_mxge0_integral_lebesgue_rV_row_mxintegral_lebesgue_rV_row_mxge0_integral_lebesgue_rV_prod	Fubini: the integral against `lebesgue_rV n.+1` is the iterated integral over the first coordinate and the others, and the integral against `lebesgue_rV (n + m)` is the iterated integral over the blocks `x` and `y` of `row_mx x y`, for nonnegative measurable or for integrable functions. The integral of `\prod_i f i (x_i)` is `\prod_i` of the integrals of the `f i` against Lebesgue measure.
lebesgue_rV_shiftlebesgue_rV_col_permlebesgue_rV_scalege0_integral_lebesgue_rV_shiftintegral_lebesgue_rV_scaleand others	`lebesgue_rV n` is invariant under translations and permutations of the coordinates, and the preimage of `X` under `x \|-> a x`, `a != 0`, has measure `\|a\|^-n` times that of `X`; the same for integrals (`\int f (a x) dx = \|a\|^-n \int f`), for nonnegative measurable and for integrable `f`.
lebesgue_rV_preimagege0_integral_lebesgue_rV_imageintegral_lebesgue_rV_image	If the preimage of every box under a measurable `phi` has `c > 0` times the measure of the box, then so has the preimage of every measurable set, and `\int f (phi x) dx = c \int f`.
gauss_pdfge0_integral_gauss_pdfintegral_gauss_pdfgauss_lebesgue_rVge0_integral_lebesgue_rV_gauss	`gauss n` has the density `gauss_pdf x = (2 pi)^(-n/2) exp (- mxdot x x / 2)` with respect to `lebesgue_rV n`: `E[f(x)] = \int f gauss_pdf`, and `\int f = E[f(x) / gauss_pdf x]`.
lebesgue_rV_gauss_integral	`\int exp (- mxdot (x - z) (x - z) / (2 s^2)) dx = (sqrt (2 pi) s)^n` over `'rV[R]_n`, for `s > 0`.
lebesgue_rV_ball_le	The closed Euclidean ball `[set x \| frobenius (x - z) <= r]` of `'rV[R]_n`, `r > 0`, has measure at most `(sqrt (2 pi e / n) r)^n`.

Declarations45 exported, 13 local

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".

sectionlebesgue_rV_cons

Context {R : realType} (n : nat).
Variable m : {sigma_finite_measure set 'rV[R]_n -> \bar R}.
Local Notation leb := (@lebesgue_measure R).
Local Open Scope ereal_scope.

definition lebesgue_rV_cons source, line 74

Type

forall {R : realType} [n : nat],
{sigma_finite_measure set 'rV_n -> \bar R} -> set 'rV_n.+1 -> \bar R

Definition

Definition lebesgue_rV_cons (A : set 'rV[R]_n.+1) : \bar R :=
  (leb \x m) (@rV_cons R n @^-1` A).

Used by 7 declarations in 1 file

this file: lebesgue_rV_cons0, lebesgue_rV_cons_ge0, lebesgue_rV_cons_sigma_additive, instance at line 95, lebesgue_rV_cons_sigma_finite, instance at line 138, lebesgue_rV_rec

let mcons section-local source, line 77

Let mcons := @measurable_rV_cons R n.

Used by 1 declaration in 1 file

this file: lebesgue_rV_cons_sigma_additive

let lebesgue_rV_cons0 section-local source, line 79

Let lebesgue_rV_cons0 : lebesgue_rV_cons set0 = 0.

Used by 1 declaration in 1 file

this file: instance at line 95

let lebesgue_rV_cons_ge0 section-local source, line 82

Let lebesgue_rV_cons_ge0 A : 0 <= lebesgue_rV_cons A.

Used by 1 declaration in 1 file

this file: instance at line 95

let lebesgue_rV_cons_sigma_additive section-local source, line 85

Let lebesgue_rV_cons_sigma_additive : semi_sigma_additive lebesgue_rV_cons.

Used by 1 declaration in 1 file

this file: instance at line 95

instance instance at line 95 source, line 95

HB.instance Definition _ := isMeasure.Build _ _ _ lebesgue_rV_cons
  lebesgue_rV_cons0 lebesgue_rV_cons_ge0 lebesgue_rV_cons_sigma_additive.

let uncons section-local source, line 98

Let uncons (x : 'rV[R]_n.+1) : measurableTypeR R * 'rV[R]_n :=
  (x 0%R 0%R, rsubmx (x : 'rV[R]_(1 + n))).

Used by 3 declarations in 1 file

this file: unconsK, measurable_uncons, lebesgue_rV_cons_sigma_finite

let unconsK section-local source, line 101

Let unconsK p : uncons (rV_cons p) = p.

Used by 1 declaration in 1 file

this file: lebesgue_rV_cons_sigma_finite

let measurable_uncons section-local source, line 107

Let measurable_uncons : measurable_fun [set: 'rV[R]_n.+1] uncons.

Used by 1 declaration in 1 file

this file: lebesgue_rV_cons_sigma_finite

let lebesgue_rV_cons_sigma_finite section-local source, line 113

Let lebesgue_rV_cons_sigma_finite : sigma_finite setT lebesgue_rV_cons.

Used by 1 declaration in 1 file

this file: instance at line 138

instance instance at line 138 source, line 138

HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ lebesgue_rV_cons
  lebesgue_rV_cons_sigma_finite.

sectionlebesgue_rV

Context {R : realType}.

fixpoint lebesgue_rV_rec source, line 146

Type

forall {R : realType} (n : nat), {sigma_finite_measure set 'rV_n -> \bar R}

Definition

Fixpoint lebesgue_rV_rec n : {sigma_finite_measure set 'rV[R]_n -> \bar R} :=
  if n is n'.+1 then lebesgue_rV_cons (lebesgue_rV_rec n')
  else \d_(0%R : 'rV[R]_0).

Used by 2 declarations in 1 file

this file: lebesgue_rV, instance at line 152

definition lebesgue_rV main result source, line 150

Type

forall {R : realType} (n : nat), set 'rV_n -> \bar R

Definition

Definition lebesgue_rV n : set 'rV[R]_n -> \bar R := lebesgue_rV_rec n.

Main result, as the README states it

lebesgue_rV n, Lebesgue measure on 'rV[R]_n, a sigma-finite measure built as gauss n is. A box with measurable sides A i has measure \prod_i lebesgue_measure (A i), and every measure on 'rV[R]_n that gives the boxes these values agrees with lebesgue_rV n on all measurable sets.

Used by 66 declarations in 5 files

this file: instance at line 152, lebesgue_rVS, lebesgue_rV_box, lebesgue_rV_unique, integral_lebesgue_rVS, ge0_integral_lebesgue_rV_cons, integrable_lebesgue_rV_cons, integral_lebesgue_rV_cons, ge0_integral_lebesgue_rV_prod, image_lebesgue_rV, ge0_integral_lebesgue_rV_image, integrable_lebesgue_rV_image, integral_lebesgue_rV_image, lebesgue_rV_preimage, lebesgue_rV_shift, lebesgue_rV_scale, lebesgue_rV_col_perm, lebesgue_rV_row_mx, ge0_integral_lebesgue_rV_shift, integral_lebesgue_rV_shift, integrable_lebesgue_rV_shift, ge0_integral_lebesgue_rV_scale, integral_lebesgue_rV_scale, integrable_lebesgue_rV_scale, ge0_integral_lebesgue_rV_col_perm, integral_lebesgue_rV_col_perm, ge0_integral_lebesgue_rV_row_mx, integral_lebesgue_rV_row_mx, lebesgue_rV_gauss_integral, lebesgue_rV_ball_le, ge0_integral_gauss_pdf, integrable_gauss_pdf, integral_gauss_pdf, ge0_integral_lebesgue_rV_gauss, gauss_lebesgue_rV
GaussianAnalysis.comparison.brascamp_lieb_lebesgue: brascamp_lieb
GaussianAnalysis.fourier.charfun_rV: ge0_integral_gauss_affine, cf_rV_regularization_le, prod_gauss_le_cf_rV, lebesgue_rV_ball_scale, ball_le_cf_rV
GaussianAnalysis.fourier.small_ball: add_gauss_ball_le, small_ball_of_cf_bound, brascamp_lieb_ge0, cf_rV_regularized_le
GaussianAnalysis.fourier.inversion: integrable_cf_rV_norm, integrable_cf_rV_kernel, cf_rV_density, cf_rV_density_le, continuous_cf_rV_density, cf_rV_density_reg, cvg_cf_rV_density_reg, integrable_reg, cf_rV_density_regE, integral_cf_rV_density_gauss, integral_cf_rV_density, cf_rV_inv_prob, instance at line 606, instance at line 613, integral_add_gauss, cf_rV_inv_prob_dominates, RN_density, ge0_integral_cf_rV_inv_prob, integral_gauss_pdf_inv_prob, smooth_EFin, cf_rV_inversion

instance instance at line 152 source, line 152

HB.instance Definition _ (n : nat) :=
  SigmaFiniteMeasure.copy (@lebesgue_rV n) (lebesgue_rV_rec n).

Arguments lebesgue_rV {R} n.

sectionlebesgue_rV_box

Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
Local Open Scope ereal_scope.

lemma lebesgue_rVS source, line 163

forall {R : realType} [n : nat] (X : set 'rV_n.+1),
lebesgue_rV n.+1 X = (lebesgue_measure \x lebesgue_rV n)%E (rV_cons (n:=n) @^-1` X)

Statement as written in the source

Lemma lebesgue_rVS n X :
  lebesgue_rV n.+1 X = (leb \x lebesgue_rV n) (@rV_cons R n @^-1` X).

Used by 1 declaration in 1 file

this file: lebesgue_rV_box

lemma lebesgue_rV_box main result source, line 167

forall {R : realType} [n : nat] [A : 'I_n -> set R],
(forall i : 'I_n, 'measurable (A i)) ->
lebesgue_rV n [set x | (forall i : 'I_n, A i (x 0 i))] =
(\prod_(i < n) lebesgue_measure (A i))%E

Main result

Stated in the README together with lebesgue_rV.

Statement as written in the source

Lemma lebesgue_rV_box n (A : 'I_n -> set R) : (forall i, measurable (A i)) ->
  lebesgue_rV n [set x : 'rV[R]_n | forall i, A i (x 0%R i)] =
    \prod_(i < n) leb (A i).

Used by 5 declarations in 1 file

this file: lebesgue_rV_unique, lebesgue_rV_shift, lebesgue_rV_scale, lebesgue_rV_col_perm, lebesgue_rV_row_mx

lemma lebesgue_rV_unique main result source, line 191

forall {R : realType} [n : nat] [mu : measure 'rV_n R],
(forall A : 'I_n -> set R,
 (forall i : 'I_n, 'measurable (A i)) ->
 mu [set x | (forall i : 'I_n, A i (x 0 i))] = (\prod_(i < n) lebesgue_measure (A i))%E) ->
forall [X : set 'rV_n],
(measure_matrix_display default_measure_display).-measurable X -> lebesgue_rV n X = mu X

Main result

Stated in the README together with lebesgue_rV.

Statement as written in the source

Lemma lebesgue_rV_unique n (mu : {measure set 'rV[R]_n -> \bar R}) :
  (forall A : 'I_n -> set R, (forall i, measurable (A i)) ->
     mu [set x : 'rV[R]_n | forall i, A i (x 0%R i)] =
       \prod_(i < n) leb (A i)) ->
  forall X, measurable X -> lebesgue_rV n X = mu X.

Used by 2 declarations in 1 file

this file: lebesgue_rV_preimage, lebesgue_rV_row_mx

sectionlebesgue_rV_integral

Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
Local Open Scope ereal_scope.

let integral_lebesgue_rVS section-local source, line 228

Let integral_lebesgue_rVS n (f : 'rV[R]_n.+1 -> \bar R) D :
  \int[lebesgue_rV n.+1]_(x in D) f x =
  \int[pushforward (leb \x lebesgue_rV n) (@rV_cons R n)]_(x in D) f x.

Used by 3 declarations in 1 file

this file: ge0_integral_lebesgue_rV_cons, integrable_lebesgue_rV_cons, integral_lebesgue_rV_cons

lemma ge0_integral_lebesgue_rV_cons main result source, line 233

forall {R : realType} [n : nat] [f : 'rV_n.+1 -> \bar R],
measurable_fun [set: 'rV_n.+1] f ->
(forall x : 'rV_n.+1, (0%R <= f x)%E) ->
(\int[lebesgue_rV n.+1]_x f x)%E =
(\int[lebesgue_measure]_t \int[lebesgue_rV n]_v f (rV_cons (t, v)))%E

Main result, as the README states it

Fubini: the integral against lebesgue_rV n.+1 is the iterated integral over the first coordinate and the others, and the integral against lebesgue_rV (n + m) is the iterated integral over the blocks x and y of row_mx x y, for nonnegative measurable or for integrable functions. The integral of \prod_i f i (x_i) is \prod_i of the integrals of the f i against Lebesgue measure.

Statement as written in the source

Lemma ge0_integral_lebesgue_rV_cons n (f : 'rV[R]_n.+1 -> \bar R) :
  measurable_fun [set: 'rV[R]_n.+1] f -> (forall x, 0 <= f x) ->
  \int[lebesgue_rV n.+1]_x f x =
    \int[leb]_t \int[lebesgue_rV n]_v f (rV_cons (t, v)).

Used by 2 declarations in 1 file

this file: ge0_integral_lebesgue_rV_prod, ge0_integral_gauss_pdf

lemma integrable_lebesgue_rV_cons source, line 244

forall {R : realType} [n : nat] [f : 'rV_n.+1 -> \bar R],
measurable_fun [set: 'rV_n.+1] f ->
(lebesgue_rV n.+1).-integrable [set: 'rV_n.+1] f <->
(lebesgue_measure \x lebesgue_rV n)%E.-integrable [set: measurableTypeR R * 'rV_n]
  (f \o rV_cons (n:=n))

Statement as written in the source

Lemma integrable_lebesgue_rV_cons n (f : 'rV[R]_n.+1 -> \bar R) :
  measurable_fun [set: 'rV[R]_n.+1] f ->
  (lebesgue_rV n.+1).-integrable [set: 'rV[R]_n.+1] f <->
  (leb \x lebesgue_rV n).-integrable [set: measurableTypeR R * 'rV[R]_n]
    (f \o @rV_cons R n).

Used by 1 declaration in 1 file

this file: integral_lebesgue_rV_cons

lemma integral_lebesgue_rV_cons main result source, line 262

forall {R : realType} [n : nat] [f : 'rV_n.+1 -> \bar R],
(lebesgue_rV n.+1).-integrable [set: 'rV_n.+1] f ->
(\int[lebesgue_rV n.+1]_x f x)%E =
(\int[lebesgue_measure]_t \int[lebesgue_rV n]_v f (rV_cons (t, v)))%E

Main result

Stated in the README together with ge0_integral_lebesgue_rV_cons.

Statement as written in the source

Lemma integral_lebesgue_rV_cons n (f : 'rV[R]_n.+1 -> \bar R) :
  (lebesgue_rV n.+1).-integrable [set: 'rV[R]_n.+1] f ->
  \int[lebesgue_rV n.+1]_x f x =
    \int[leb]_t \int[lebesgue_rV n]_v f (rV_cons (t, v)).

sectionlebesgue_rV_prod

Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
Local Open Scope ereal_scope.

lemma ge0_integral_lebesgue_rV_prod main result source, line 280

forall {R : realType} [n : nat] [f : 'I_n -> R -> R],
(forall i : 'I_n, measurable_fun [set: R] (f i)) ->
(forall (i : 'I_n) (t : R), 0 <= f i t) ->
(\int[lebesgue_rV n]_x (\prod_(i < n) f i (x 0 i))%:E)%E =
(\prod_(i < n) \int[lebesgue_measure]_t (f i t)%:E)%E

Main result

Stated in the README together with ge0_integral_lebesgue_rV_cons.

Statement as written in the source

Lemma ge0_integral_lebesgue_rV_prod n (f : 'I_n -> R -> R) :
  (forall i, measurable_fun [set: R] (f i)) -> (forall i t, (0 <= f i t)%R) ->
  \int[lebesgue_rV n]_x (\prod_(i < n) f i (x 0%R i))%:E =
  \prod_(i < n) \int[leb]_t (f i t)%:E.

Used by 1 declaration in 1 file

this file: lebesgue_rV_gauss_integral

sectionlebesgue_rV_image

Context {R : realType} (n : nat).
Local Open Scope ereal_scope.
Variable phi : 'rV[R]_n -> 'rV[R]_n.
Hypothesis mphi : measurable_fun [set: 'rV[R]_n] phi.
Variable c : {nonneg R}.
Hypothesis phiE : forall X, measurable X ->
  lebesgue_rV n (phi @^-1` X) = c%:num%:E * lebesgue_rV n X.

let image_lebesgue_rV section-local source, line 329

Let image_lebesgue_rV (f : 'rV[R]_n -> \bar R) D :
  \int[pushforward (lebesgue_rV n) phi]_(x in D) f x =
  \int[mscale c (lebesgue_rV n)]_(x in D) f x.

Used by 1 declaration in 1 file

this file: ge0_integral_lebesgue_rV_image

lemma ge0_integral_lebesgue_rV_image main result source, line 334

forall {R : realType} [n : nat] [phi : 'rV_n -> 'rV_n],
measurable_fun [set: 'rV_n] phi ->
forall [c : {nonneg R}],
(forall X : set 'rV_n,
 (measure_matrix_display default_measure_display).-measurable X ->
 lebesgue_rV n (phi @^-1` X) = ((c%:num)%:E * lebesgue_rV n X)%E) ->
forall [f : 'rV_n -> \bar R],
measurable_fun [set: 'rV_n] f ->
(forall x : 'rV_n, (0%R <= f x)%E) ->
(\int[lebesgue_rV n]_x f (phi x))%E = ((c%:num)%:E * \int[lebesgue_rV n]_x f x)%E

Main result

Stated in the README together with lebesgue_rV_preimage.

Statement as written in the source

Lemma ge0_integral_lebesgue_rV_image (f : 'rV[R]_n -> \bar R) :
  measurable_fun [set: 'rV[R]_n] f -> (forall x, 0 <= f x) ->
  \int[lebesgue_rV n]_x f (phi x) = c%:num%:E * \int[lebesgue_rV n]_x f x.

Used by 5 declarations in 1 file

this file: integrable_lebesgue_rV_image, integral_lebesgue_rV_image, ge0_integral_lebesgue_rV_shift, ge0_integral_lebesgue_rV_scale, ge0_integral_lebesgue_rV_col_perm

lemma integrable_lebesgue_rV_image source, line 343

forall {R : realType} [n : nat] [phi : 'rV_n -> 'rV_n],
measurable_fun [set: 'rV_n] phi ->
forall [c : {nonneg R}],
(forall X : set 'rV_n,
 (measure_matrix_display default_measure_display).-measurable X ->
 lebesgue_rV n (phi @^-1` X) = ((c%:num)%:E * lebesgue_rV n X)%E) ->
forall [f : 'rV_n -> \bar R],
(lebesgue_rV n).-integrable [set: 'rV_n] f ->
(lebesgue_rV n).-integrable [set: 'rV_n] (f \o phi)

Statement as written in the source

Lemma integrable_lebesgue_rV_image (f : 'rV[R]_n -> \bar R) :
  (lebesgue_rV n).-integrable [set: 'rV[R]_n] f ->
  (lebesgue_rV n).-integrable [set: 'rV[R]_n] (f \o phi).

Used by 2 declarations in 1 file

this file: integrable_lebesgue_rV_shift, integrable_lebesgue_rV_scale

lemma integral_lebesgue_rV_image main result source, line 355

forall {R : realType} [n : nat] [phi : 'rV_n -> 'rV_n],
measurable_fun [set: 'rV_n] phi ->
forall [c : {nonneg R}],
(forall X : set 'rV_n,
 (measure_matrix_display default_measure_display).-measurable X ->
 lebesgue_rV n (phi @^-1` X) = ((c%:num)%:E * lebesgue_rV n X)%E) ->
forall [f : 'rV_n -> \bar R],
(lebesgue_rV n).-integrable [set: 'rV_n] f ->
(\int[lebesgue_rV n]_x f (phi x))%E = ((c%:num)%:E * \int[lebesgue_rV n]_x f x)%E

Main result

Stated in the README together with lebesgue_rV_preimage.

Statement as written in the source

Lemma integral_lebesgue_rV_image (f : 'rV[R]_n -> \bar R) :
  (lebesgue_rV n).-integrable [set: 'rV[R]_n] f ->
  \int[lebesgue_rV n]_x f (phi x) = c%:num%:E * \int[lebesgue_rV n]_x f x.

Used by 3 declarations in 1 file

this file: integral_lebesgue_rV_shift, integral_lebesgue_rV_scale, integral_lebesgue_rV_col_perm

sectionlebesgue_rV_invariance

Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).

lemma lebesgue_rV_preimage main result source, line 387

forall {R : realType} [n : nat] [phi : 'rV_n -> 'rV_n] [c : R],
measurable_fun [set: 'rV_n] phi ->
0 < c ->
(forall A : 'I_n -> set R,
 (forall i : 'I_n, 'measurable (A i)) ->
 lebesgue_rV n (phi @^-1` [set x | (forall i : 'I_n, A i (x 0 i))]) =
 (c%:E * \prod_(i < n) lebesgue_measure (A i))%E) ->
forall [X : set 'rV_n],
(measure_matrix_display default_measure_display).-measurable X ->
lebesgue_rV n (phi @^-1` X) = (c%:E * lebesgue_rV n X)%E

If the preimage of every box under phi has c times the measure of the box, then so has the preimage of every measurable set.

Main result, as the README states it

If the preimage of every box under a measurable phi has c > 0 times the measure of the box, then so has the preimage of every measurable set, and \int f (phi x) dx = c \int f.

Statement as written in the source

Lemma lebesgue_rV_preimage n (phi : 'rV[R]_n -> 'rV[R]_n) (c : R) :
  measurable_fun [set: 'rV[R]_n] phi -> 0 < c ->
  (forall A : 'I_n -> set R, (forall i, measurable (A i)) ->
    lebesgue_rV n (phi @^-1` [set x : 'rV[R]_n | forall i, A i (x 0 i)]) =
      (c%:E * \prod_(i < n) leb (A i))%E) ->
  forall X, measurable X ->
    lebesgue_rV n (phi @^-1` X) = (c%:E * lebesgue_rV n X)%E.

Used by 3 declarations in 1 file

this file: lebesgue_rV_shift, lebesgue_rV_scale, lebesgue_rV_col_perm

lemma measurable_rV_shift source, line 408

forall {R : realType} [n : nat] (b : 'rV_n), measurable_fun [set: 'rV_n] (+%R^~ b)

Statement as written in the source

Lemma measurable_rV_shift n (b : 'rV[R]_n) :
  measurable_fun [set: 'rV[R]_n] (fun x => x + b).

Used by 4 declarations in 1 file

this file: lebesgue_rV_shift, ge0_integral_lebesgue_rV_shift, integral_lebesgue_rV_shift, integrable_lebesgue_rV_shift

lemma lebesgue_rV_shift main result source, line 412

forall {R : realType} [n : nat] (b : 'rV_n) [X : set 'rV_n],
(measure_matrix_display default_measure_display).-measurable X ->
lebesgue_rV n (+%R^~ b @^-1` X) = lebesgue_rV n X

Main result, as the README states it

lebesgue_rV n is invariant under translations and permutations of the coordinates, and the preimage of X under x |-> a x, a != 0, has measure |a|^-n times that of X; the same for integrals (\int f (a x) dx = |a|^-n \int f), for nonnegative measurable and for integrable f.

Statement as written in the source

Lemma lebesgue_rV_shift n (b : 'rV[R]_n) (X : set 'rV[R]_n) : measurable X ->
  lebesgue_rV n ((fun x => x + b) @^-1` X) = lebesgue_rV n X.

Used by 4 declarations in 2 files

this file: ge0_integral_lebesgue_rV_shift, integral_lebesgue_rV_shift, integrable_lebesgue_rV_shift
GaussianAnalysis.fourier.charfun_rV: lebesgue_rV_ball_scale

lemma measurable_rV_scale source, line 429

forall {R : realType} [n : nat] (a : R), measurable_fun [set: 'rV_n] [eta  *:%R a]

Statement as written in the source

Lemma measurable_rV_scale n (a : R) :
  measurable_fun [set: 'rV[R]_n] (fun x => a *: x).

Used by 12 declarations in 3 files

this file: lebesgue_rV_scale, ge0_integral_lebesgue_rV_scale, integral_lebesgue_rV_scale, integrable_lebesgue_rV_scale
GaussianAnalysis.fourier.charfun_rV: ge0_integral_gauss_affine, cf_rV_regularization_le, prod_gauss_le_cf_rV
GaussianAnalysis.fourier.inversion: cf_rV_density_regE, integral_add_gauss, lipschitz_add_gauss, integral_gauss_pdf_inv_prob, smooth_EFin

lemma lebesgue_rV_scale main result source, line 433

forall {R : realType} [n : nat] [a : R] [X : set 'rV_n],
a != 0 ->
(measure_matrix_display default_measure_display).-measurable X ->
lebesgue_rV n ([eta  *:%R a] @^-1` X) = ((`|a| ^- n)%:E * lebesgue_rV n X)%E

Main result

Stated in the README together with lebesgue_rV_shift.

Statement as written in the source

Lemma lebesgue_rV_scale n (a : R) (X : set 'rV[R]_n) : a != 0 -> measurable X ->
  lebesgue_rV n ((fun x => a *: x) @^-1` X) =
    ((`|a| ^- n)%:E * lebesgue_rV n X)%E.

Used by 4 declarations in 2 files

this file: ge0_integral_lebesgue_rV_scale, integral_lebesgue_rV_scale, integrable_lebesgue_rV_scale
GaussianAnalysis.fourier.charfun_rV: lebesgue_rV_ball_scale

lemma lebesgue_rV_col_perm main result source, line 453

forall {R : realType} [n : nat] (s : {perm 'I_n}) [X : set 'rV_n],
(measure_matrix_display default_measure_display).-measurable X ->
lebesgue_rV n (col_perm s @^-1` X) = lebesgue_rV n X

Main result

Stated in the README together with lebesgue_rV_shift.

Statement as written in the source

Lemma lebesgue_rV_col_perm n (s : 'S_n) (X : set 'rV[R]_n) : measurable X ->
  lebesgue_rV n (col_perm s @^-1` X) = lebesgue_rV n X.

Used by 2 declarations in 1 file

this file: ge0_integral_lebesgue_rV_col_perm, integral_lebesgue_rV_col_perm

lemma lebesgue_rV_row_mx main result source, line 469

forall {R : realType} [n m : nat] [X : set 'rV_(n + m)],
(measure_matrix_display default_measure_display).-measurable X ->
lebesgue_rV (n + m) X =
(lebesgue_rV n \x lebesgue_rV m)%E ((fun p : 'rV_n * 'rV_m => row_mx p.1 p.2) @^-1` X)

Main result

Stated in the README together with ge0_integral_lebesgue_rV_cons.

Statement as written in the source

Lemma lebesgue_rV_row_mx n m (X : set 'rV[R]_(n + m)) : measurable X ->
  lebesgue_rV (n + m) X =
  (lebesgue_rV n \x lebesgue_rV m)%E
    ((fun p : 'rV[R]_n * 'rV[R]_m => row_mx p.1 p.2) @^-1` X).

Used by 2 declarations in 1 file

this file: ge0_integral_lebesgue_rV_row_mx, integral_lebesgue_rV_row_mx

sectionlebesgue_rV_invariance_integral

Context {R : realType}.
Local Open Scope ereal_scope.

lemma ge0_integral_lebesgue_rV_shift main result source, line 512

forall {R : realType} [n : nat] (b : 'rV_n) [f : 'rV_n -> \bar R],
measurable_fun [set: 'rV_n] f ->
(forall x : 'rV_n, (0%R <= f x)%E) ->
(\int[lebesgue_rV n]_x f (x + b)%R)%E = (\int[lebesgue_rV n]_x f x)%E

Main result

Stated in the README together with lebesgue_rV_shift.

Statement as written in the source

Lemma ge0_integral_lebesgue_rV_shift n (b : 'rV[R]_n) (f : 'rV[R]_n -> \bar R) :
  measurable_fun [set: 'rV[R]_n] f -> (forall x, 0 <= f x) ->
  \int[lebesgue_rV n]_x f (x + b)%R = \int[lebesgue_rV n]_x f x.

Used by 2 declarations in 2 files

GaussianAnalysis.fourier.charfun_rV: ge0_integral_gauss_affine
GaussianAnalysis.fourier.inversion: integral_cf_rV_density

lemma integral_lebesgue_rV_shift source, line 525

forall {R : realType} [n : nat] (b : 'rV_n) [f : 'rV_n -> \bar R],
(lebesgue_rV n).-integrable [set: 'rV_n] f ->
(\int[lebesgue_rV n]_x f (x + b)%R)%E = (\int[lebesgue_rV n]_x f x)%E

Statement as written in the source

Lemma integral_lebesgue_rV_shift n (b : 'rV[R]_n) (f : 'rV[R]_n -> \bar R) :
  (lebesgue_rV n).-integrable [set: 'rV[R]_n] f ->
  \int[lebesgue_rV n]_x f (x + b)%R = \int[lebesgue_rV n]_x f x.

lemma integrable_lebesgue_rV_shift source, line 536

forall {R : realType} [n : nat] (b : 'rV_n) [f : 'rV_n -> \bar R],
(lebesgue_rV n).-integrable [set: 'rV_n] f ->
(lebesgue_rV n).-integrable [set: 'rV_n]
  (fun x : 'rV_n => f (x + b))

Statement as written in the source

Lemma integrable_lebesgue_rV_shift n (b : 'rV[R]_n) (f : 'rV[R]_n -> \bar R) :
  (lebesgue_rV n).-integrable [set: 'rV[R]_n] f ->
  (lebesgue_rV n).-integrable [set: 'rV[R]_n] (fun x => f (x + b)%R).

lemma ge0_integral_lebesgue_rV_scale source, line 546

forall {R : realType} [n : nat] [a : R] [f : 'rV_n -> \bar R],
a != 0 ->
measurable_fun [set: 'rV_n] f ->
(forall x : 'rV_n, (0%R <= f x)%E) ->
(\int[lebesgue_rV n]_x f (a *: x))%E = ((`|a| ^- n)%:E * \int[lebesgue_rV n]_x f x)%E

Statement as written in the source

Lemma ge0_integral_lebesgue_rV_scale n (a : R) (f : 'rV[R]_n -> \bar R) :
  (a != 0)%R -> measurable_fun [set: 'rV[R]_n] f -> (forall x, 0 <= f x) ->
  \int[lebesgue_rV n]_x f (a *: x) =
    (`|a| ^- n)%:E * \int[lebesgue_rV n]_x f x.

Used by 1 declaration in 1 file

GaussianAnalysis.fourier.charfun_rV: ge0_integral_gauss_affine

lemma integral_lebesgue_rV_scale main result source, line 558

forall {R : realType} [n : nat] [a : R] [f : 'rV_n -> \bar R],
a != 0 ->
(lebesgue_rV n).-integrable [set: 'rV_n] f ->
(\int[lebesgue_rV n]_x f (a *: x))%E = ((`|a| ^- n)%:E * \int[lebesgue_rV n]_x f x)%E

Main result

Stated in the README together with lebesgue_rV_shift.

Statement as written in the source

Lemma integral_lebesgue_rV_scale n (a : R) (f : 'rV[R]_n -> \bar R) :
  (a != 0)%R -> (lebesgue_rV n).-integrable [set: 'rV[R]_n] f ->
  \int[lebesgue_rV n]_x f (a *: x) =
    (`|a| ^- n)%:E * \int[lebesgue_rV n]_x f x.

Used by 1 declaration in 1 file

GaussianAnalysis.fourier.inversion: cf_rV_density_regE

lemma integrable_lebesgue_rV_scale source, line 570

forall {R : realType} [n : nat] [a : R] [f : 'rV_n -> \bar R],
a != 0 ->
(lebesgue_rV n).-integrable [set: 'rV_n] f ->
(lebesgue_rV n).-integrable [set: 'rV_n]
  (fun x : 'rV_n => f (a *: x))

Statement as written in the source

Lemma integrable_lebesgue_rV_scale n (a : R) (f : 'rV[R]_n -> \bar R) :
  (a != 0)%R -> (lebesgue_rV n).-integrable [set: 'rV[R]_n] f ->
  (lebesgue_rV n).-integrable [set: 'rV[R]_n] (fun x => f (a *: x)).

lemma ge0_integral_lebesgue_rV_col_perm source, line 581

forall {R : realType} [n : nat] (s : {perm 'I_n}) [f : 'rV_n -> \bar R],
measurable_fun [set: 'rV_n] f ->
(forall x : 'rV_n, (0%R <= f x)%E) ->
(\int[lebesgue_rV n]_x f (col_perm s x))%E = (\int[lebesgue_rV n]_x f x)%E

Statement as written in the source

Lemma ge0_integral_lebesgue_rV_col_perm n (s : 'S_n) (f : 'rV[R]_n -> \bar R) :
  measurable_fun [set: 'rV[R]_n] f -> (forall x, 0 <= f x) ->
  \int[lebesgue_rV n]_x f (col_perm s x) = \int[lebesgue_rV n]_x f x.

lemma integral_lebesgue_rV_col_perm source, line 594

forall {R : realType} [n : nat] (s : {perm 'I_n}) [f : 'rV_n -> \bar R],
(lebesgue_rV n).-integrable [set: 'rV_n] f ->
(\int[lebesgue_rV n]_x f (col_perm s x))%E = (\int[lebesgue_rV n]_x f x)%E

Statement as written in the source

Lemma integral_lebesgue_rV_col_perm n (s : 'S_n) (f : 'rV[R]_n -> \bar R) :
  (lebesgue_rV n).-integrable [set: 'rV[R]_n] f ->
  \int[lebesgue_rV n]_x f (col_perm s x) = \int[lebesgue_rV n]_x f x.

lemma ge0_integral_lebesgue_rV_row_mx main result source, line 605

forall {R : realType} [n m : nat] [f : 'rV_(n + m) -> \bar R],
measurable_fun [set: 'rV_(n + m)] f ->
(forall x : 'rV_(n + m), (0%R <= f x)%E) ->
(\int[lebesgue_rV (n + m)]_x f x)%E =
(\int[lebesgue_rV n]_x \int[lebesgue_rV m]_y f (row_mx x y))%E

Main result

Stated in the README together with ge0_integral_lebesgue_rV_cons.

Statement as written in the source

Lemma ge0_integral_lebesgue_rV_row_mx n m (f : 'rV[R]_(n + m) -> \bar R) :
  measurable_fun [set: 'rV[R]_(n + m)] f -> (forall x, 0 <= f x) ->
  \int[lebesgue_rV (n + m)]_x f x =
    \int[lebesgue_rV n]_x \int[lebesgue_rV m]_y f (row_mx x y).

lemma integral_lebesgue_rV_row_mx main result source, line 624

forall {R : realType} [n m : nat] [f : 'rV_(n + m) -> \bar R],
(lebesgue_rV (n + m)).-integrable [set: 'rV_(n + m)] f ->
(\int[lebesgue_rV (n + m)]_x f x)%E =
(\int[lebesgue_rV n]_x \int[lebesgue_rV m]_y f (row_mx x y))%E

Main result

Stated in the README together with ge0_integral_lebesgue_rV_cons.

Statement as written in the source

Lemma integral_lebesgue_rV_row_mx n m (f : 'rV[R]_(n + m) -> \bar R) :
  (lebesgue_rV (n + m)).-integrable [set: 'rV[R]_(n + m)] f ->
  \int[lebesgue_rV (n + m)]_x f x =
    \int[lebesgue_rV n]_x \int[lebesgue_rV m]_y f (row_mx x y).

sectiongauss_density

Context {R : realType}.
Local Notation leb := (@lebesgue_measure R).
Local Notation N := (@normal_prob R 0 1).

definition gauss_pdf main result source, line 662

Type

forall {R : realType} [n : nat], 'rV_n -> R

Definition

Definition gauss_pdf n (x : 'rV[R]_n) : R :=
  Num.sqrt (2 * pi) ^- n * expR (- mxdot x x / 2).

Main result, as the README states it

gauss n has the density gauss_pdf x = (2 pi)^(-n/2) exp (- mxdot x x / 2) with respect to lebesgue_rV n: E[f(x)] = \int f gauss_pdf, and \int f = E[f(x) / gauss_pdf x].

Used by 19 declarations in 4 files

this file: gauss_pdf_gt0, gauss_pdf_ge0, measurable_gauss_pdf, gauss_pdf_cons, ge0_integral_gauss_pdf, integrable_gauss_pdf, integral_gauss_pdf, ge0_integral_lebesgue_rV_gauss, gauss_lebesgue_rV
GaussianAnalysis.comparison.brascamp_lieb_lebesgue: brascamp_lieb
GaussianAnalysis.fourier.charfun_rV: gauss_pdf_scale, ge0_integral_gauss_affine, cf_rV_regularization_le
GaussianAnalysis.fourier.inversion: cf_rV_density_regE, integral_cf_rV_density, pdf_le2, integral_add_gauss, integral_gauss_pdf_inv_prob, smooth_EFin

lemma gauss_pdf_gt0 source, line 665

forall {R : realType} [n : nat] (x : 'rV_n), 0 < gauss_pdf x

Statement as written in the source

Lemma gauss_pdf_gt0 n (x : 'rV[R]_n) : 0 < gauss_pdf x.

Used by 2 declarations in 1 file

this file: gauss_pdf_ge0, ge0_integral_lebesgue_rV_gauss

lemma gauss_pdf_ge0 source, line 671

forall {R : realType} [n : nat] (x : 'rV_n), 0 <= gauss_pdf x

Statement as written in the source

Lemma gauss_pdf_ge0 n (x : 'rV[R]_n) : 0 <= gauss_pdf x.

Used by 10 declarations in 3 files

this file: ge0_integral_gauss_pdf, integrable_gauss_pdf, integral_gauss_pdf, ge0_integral_lebesgue_rV_gauss
GaussianAnalysis.fourier.charfun_rV: ge0_integral_gauss_affine
GaussianAnalysis.fourier.inversion: cf_rV_density_ge0, integral_cf_rV_density, pdf_le2, integral_add_gauss, integral_gauss_pdf_inv_prob

let measurable_mxdotB section-local source, line 674

Let measurable_mxdotB n (z : 'rV[R]_n) :
  measurable_fun [set: 'rV[R]_n] (fun x => mxdot (x - z) (x - z)).

Used by 3 declarations in 1 file

this file: measurable_gauss_pdf, lebesgue_rV_ball_le, ge0_integral_lebesgue_rV_gauss

lemma measurable_gauss_pdf source, line 685

forall {R : realType} [n : nat], measurable_fun [set: 'rV_n] (gauss_pdf (n:=n))

Statement as written in the source

Lemma measurable_gauss_pdf n : measurable_fun [set: 'rV[R]_n] (@gauss_pdf n).

Used by 6 declarations in 3 files

this file: ge0_integral_gauss_pdf, integrable_gauss_pdf
GaussianAnalysis.fourier.charfun_rV: ge0_integral_gauss_affine
GaussianAnalysis.fourier.inversion: integral_cf_rV_density, integral_add_gauss, integral_gauss_pdf_inv_prob

let mxdot_rV_cons_self section-local source, line 694

Let mxdot_rV_cons_self n t (v : 'rV[R]_n) :
  mxdot (rV_cons (t, v)) (rV_cons (t, v)) = t ^+ 2 + mxdot v v.

Used by 1 declaration in 1 file

this file: gauss_pdf_cons

lemma gauss_pdf_cons source, line 701

forall {R : realType} [n : nat] (t : measurableTypeR R) (v : 'rV_n),
gauss_pdf (rV_cons (t, v)) = normal_pdf 0 1 t * gauss_pdf v

Statement as written in the source

Lemma gauss_pdf_cons n t (v : 'rV[R]_n) :
  gauss_pdf (rV_cons (t, v)) = normal_pdf 0 1 t * gauss_pdf v.

Used by 1 declaration in 1 file

this file: ge0_integral_gauss_pdf

let integral_normal_fun section-local source, line 713

Let integral_normal_fun (c s : R) : 0 < s ->
  (\int[leb]_t (normal_fun c s t)%:E = (Num.sqrt (2 * pi) * s)%:E)%E.

Used by 1 declaration in 1 file

this file: lebesgue_rV_gauss_integral

lemma lebesgue_rV_gauss_integral main result source, line 735

forall {R : realType} [n : nat] (z : 'rV_n) [s : R],
0 < s ->
(\int[lebesgue_rV n]_x (expR (- mxdot (x - z) (x - z) / (2 * s ^+ 2)))%:E)%E =
((Num.ExtraDef.sqrtr (2 * pi) * s) ^+ n)%:E

Main result, as the README states it

\int exp (- mxdot (x - z) (x - z) / (2 s^2)) dx = (sqrt (2 pi) s)^n over 'rV[R]_n, for s > 0.

Statement as written in the source

Lemma lebesgue_rV_gauss_integral n (z : 'rV[R]_n) (s : R) : 0 < s ->
  (\int[lebesgue_rV n]_x (expR (- mxdot (x - z) (x - z) / (2 * s ^+ 2)))%:E =
    ((Num.sqrt (2 * pi) * s) ^+ n)%:E)%E.

Used by 1 declaration in 1 file

this file: lebesgue_rV_ball_le

lemma lebesgue_rV_ball_le main result source, line 752

forall {R : realType} [n : nat] (z : 'rV_n) [r : R],
0 < r ->
(lebesgue_rV n [set x | (frobenius (x - z) <= r)%R] <=
 ((Num.ExtraDef.sqrtr (2 * pi * expR 1 / n%:R) * r) ^+ n)%:E)%E

Main result, as the README states it

The closed Euclidean ball [set x | frobenius (x - z) <= r] of 'rV[R]_n, r > 0, has measure at most (sqrt (2 pi e / n) r)^n.

Statement as written in the source

Lemma lebesgue_rV_ball_le n (z : 'rV[R]_n) (r : R) : 0 < r ->
  (lebesgue_rV n [set x | (frobenius (x - z) <= r)%R] <=
    ((Num.sqrt (2 * pi * expR 1 / n%:R) * r) ^+ n)%:E)%E.

Used by 2 declarations in 2 files

GaussianAnalysis.fourier.charfun_rV: ball_le_cf_rV
GaussianAnalysis.fourier.small_ball: add_gauss_ball_le

Local Open Scope ereal_scope.

lemma ge0_integral_gauss_pdf main result source, line 813

forall {R : realType} [n : nat] [f : 'rV_n -> \bar R],
measurable_fun [set: 'rV_n] f ->
(forall x : 'rV_n, (0%R <= f x)%E) ->
(\int[gauss n]_x f x)%E = (\int[lebesgue_rV n]_x (f x * (gauss_pdf x)%:E))%E

Main result

Stated in the README together with gauss_pdf.

Statement as written in the source

Lemma ge0_integral_gauss_pdf n (f : 'rV[R]_n -> \bar R) :
  measurable_fun [set: 'rV[R]_n] f -> (forall x, 0 <= f x) ->
  \int[gauss n]_x f x = \int[lebesgue_rV n]_x (f x * (gauss_pdf x)%:E).

Used by 5 declarations in 2 files

this file: integrable_gauss_pdf, integral_gauss_pdf, ge0_integral_lebesgue_rV_gauss, gauss_lebesgue_rV
GaussianAnalysis.fourier.charfun_rV: ge0_integral_gauss_affine

lemma integrable_gauss_pdf source, line 850

forall {R : realType} [n : nat] [f : 'rV_n -> \bar R],
measurable_fun [set: 'rV_n] f ->
(gauss n).-integrable [set: 'rV_n] f <->
(lebesgue_rV n).-integrable [set: 'rV_n]
  (fun x : 'rV_n =>
   (f x * (gauss_pdf x)%:E)%E)

Statement as written in the source

Lemma integrable_gauss_pdf n (f : 'rV[R]_n -> \bar R) :
  measurable_fun [set: 'rV[R]_n] f ->
  (gauss n).-integrable [set: 'rV[R]_n] f <->
  (lebesgue_rV n).-integrable [set: 'rV[R]_n]
    (fun x => f x * (gauss_pdf x)%:E).

Used by 1 declaration in 1 file

GaussianAnalysis.fourier.inversion: cf_rV_density_regE

lemma integral_gauss_pdf main result source, line 872

forall {R : realType} [n : nat] [f : 'rV_n -> \bar R],
(gauss n).-integrable [set: 'rV_n] f ->
(\int[gauss n]_x f x)%E = (\int[lebesgue_rV n]_x (f x * (gauss_pdf x)%:E))%E

Main result

Stated in the README together with gauss_pdf.

Statement as written in the source

Lemma integral_gauss_pdf n (f : 'rV[R]_n -> \bar R) :
  (gauss n).-integrable [set: 'rV[R]_n] f ->
  \int[gauss n]_x f x = \int[lebesgue_rV n]_x (f x * (gauss_pdf x)%:E).

Used by 1 declaration in 1 file

GaussianAnalysis.fourier.inversion: cf_rV_density_regE

lemma ge0_integral_lebesgue_rV_gauss main result source, line 891

forall {R : realType} [n : nat] [f : 'rV_n -> \bar R],
measurable_fun [set: 'rV_n] f ->
(forall x : 'rV_n, (0%R <= f x)%E) ->
(\int[lebesgue_rV n]_x f x)%E = (\int[gauss n]_x (f x * ((gauss_pdf x)^-1)%:E))%E

Main result

Stated in the README together with gauss_pdf.

Statement as written in the source

Lemma ge0_integral_lebesgue_rV_gauss n (f : 'rV[R]_n -> \bar R) :
  measurable_fun [set: 'rV[R]_n] f -> (forall x, 0 <= f x) ->
  \int[lebesgue_rV n]_x f x = \int[gauss n]_x (f x * ((gauss_pdf x)^-1)%R%:E).

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.brascamp_lieb_lebesgue: brascamp_lieb

lemma gauss_lebesgue_rV main result source, line 912

forall {R : realType} [n : nat] [X : set 'rV_n],
(measure_matrix_display default_measure_display).-measurable X ->
gauss n X = (\int[lebesgue_rV n]_(x in X) (gauss_pdf x)%:E)%E

Main result

Stated in the README together with gauss_pdf.

Statement as written in the source

Lemma gauss_lebesgue_rV n (X : set 'rV[R]_n) : measurable X ->
  gauss n X = \int[lebesgue_rV n]_(x in X) (gauss_pdf x)%:E.

Used by 1 declaration in 1 file

GaussianAnalysis.fourier.inversion: integral_cf_rV_density

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.