On this page

Gaussian integration by parts

GaussianAnalysis.gaussian.gauss_ibplibrary/gaussian/gauss_ibp.v541 lines16 lemmas and theoremssource

Imports 3 library modules and 31 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.archimedean, 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, 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.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.ftc, mathcomp.analysis.probability_theory.probability

Imported by 18

Required by 1 files of the paper proofs

theories/Gaussian/Law/LibraryBridge.v

Stein's identity for the standard normal law, E[X f(X)] = E[f'(X)] (normal_ibp), and its version in several dimensions for gauss n, E[x_i F(x)] = E[d_i F(x)] (gauss_ibp), for functions of class C^1 of polynomial growth. gauss_ibp_line asks less: F and d_i F measurable, and d_i F continuous along the lines parallel to the i-th axis. A partial derivative of a measurable function is measurable (measurable_derive_rV), so the identity of order two, E[(x_i^2 - 1) F(x)] = E[d_i d_i F(x)] (gauss_ibp2), holds for F measurable and d_i d_i F continuous, without any continuity of d_i F.

Polynomial growth means `|F x| <= C * (1 + `|x| ^+ k) for all x, where `|x| is the largest absolute value of a coordinate of x (gauss.v, section poly_bound).

Main results

Results	Statement	Used by `theories/`
normal_ibp	Stein's identity: `E[X f(X)] = E[f'(X)]` for `X` of law `normal_prob 0 1` and `f` differentiable with a continuous derivative, `f` and `f'` of polynomial growth.
gauss_ibp	Gaussian integration by parts: `E[x_i F(x)] = E[d_i F(x)]` for `x` of law `gauss n`, `F` continuous with a continuous partial derivative `d_i F` (along `delta_mx 0 i`), both of polynomial growth.	`Gaussian/Law/LibraryBridge`, for `Gaussian/Iterated/Stein`
gauss_ibp_line	The same identity when `F` and `d_i F` are only measurable and `d_i F` is continuous along the lines parallel to the i-th axis.
measurable_derive_rV	If a measurable function on `'rV[R]_n` has at every point `x` a derivative `dF x` along a fixed vector `v`, then `dF` is measurable.
gauss_ibp2	Gaussian integration by parts of order two: `E[(x_i^2 - 1) F(x)] = E[d_i d_i F(x)]` for `x` of law `gauss n`, `F` measurable, `d_i d_i F` continuous, and `F`, `d_i F` and `d_i d_i F` of polynomial growth; `d_i F` need not be continuous.	`Gaussian/Law/LibraryBridge`, for `Gaussian/Iterated/Stein`
integrable_nondecreasing_set_cvg_integral	If `F i` increases to `U` and `g` is integrable on `U`, the integrals of `g` over `F i` converge to its integral over `U`.

Declarations16 exported

sectionintegral_nondecreasing_set

Context {d : measure_display} {T : measurableType d} {R : realType}.
Variables (mu : {measure set T -> \bar R}) (F : (set T)^nat) (g : T -> \bar R).
Hypotheses (ndF : nondecreasing_seq F) (mF : forall i, measurable (F i)).
Hypothesis gi : mu.-integrable (\bigcup_i F i) g.

lemma integrable_nondecreasing_set_cvg_integral main result source, line 46

forall {d : measure_display} {T : measurableType d} {R : realType} 
  [mu : measure T R] [F : (set T) ^nat] [g : T -> \bar R],
{homo F : n m / (n <= m)%N >-> (n <= m)%O} ->
(forall i : nat, d.-measurable (F i)) ->
mu.-integrable (\bigcup_i F i) g ->
(\int[mu]_(x in F i) g x)%E @[i --> \oo] --> (\int[mu]_(x in \bigcup_i F i) g x)%E

Main result, as the README states it

If F i increases to U and g is integrable on U, the integrals of g over F i converge to its integral over U.

Statement as written in the source

Lemma integrable_nondecreasing_set_cvg_integral :
  (\int[mu]_(x in F i) g x @[i --> \oo] -->
   \int[mu]_(x in \bigcup_i F i) g x)%E.

Used by 1 declaration in 1 file

this file: normal_ibp

A finite sum of continuous functions is continuous.

sectioncontinuous_sum

Context {K : numFieldType} {V : normedModType K} {T : topologicalType}.

lemma continuous_sum source, line 76

forall {K : numFieldType} {V : normedModType K} {T : topologicalType} 
  [I : Type] [s : seq I] [f : I -> T -> V],
(forall i : I, continuous (f i)) -> continuous (fun x0 : T => \sum_(i <- s) f i x0)

Statement as written in the source

Lemma continuous_sum (I : Type) (s : seq I) (f : I -> T -> V) :
  (forall i, continuous (f i)) -> continuous (fun x => \sum_(i <- s) f i x).

Used by 9 declarations in 8 files

GaussianAnalysis.gaussian.partial_derivative: continuous_partials_linear
GaussianAnalysis.gaussian.gauss_interpolation: gauss_ibp_mulmx
GaussianAnalysis.random_matrix.wigner: continuous_goe_stat
GaussianAnalysis.comparison.slepian: continuous_softmax
GaussianAnalysis.comparison.gordon: continuous_gsum, continuous_gtot
GaussianAnalysis.comparison.brascamp_lieb: cdF
GaussianAnalysis.fourier.charfun_rV: continuous_mxdotr
GaussianAnalysis.fourier.inversion: continuous_mxdotr

sectionnormal_ibp

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

lemma is_derive_normal_pdf01 source, line 92

forall {R : realType} (x : R),
is_derive x 1 (normal_pdf (0 : R) 1) (- x * normal_pdf (0 : R) 1 x)

Statement as written in the source

Lemma is_derive_normal_pdf01 (x : R) : is_derive x 1 phi (- x * phi x).

Used by 1 declaration in 1 file

this file: normal_ibp

lemma normal_pdf01E source, line 108

forall {R : realType} (x : R), normal_pdf (0 : R) 1 x = normal_peak 1 * expR (- x ^+ 2 / 2)

Statement as written in the source

Lemma normal_pdf01E (x : R) : phi x = normal_peak 1 * expR (- x ^+ 2 / 2).

Used by 4 declarations in 2 files

this file: normal_pdf01N, cvgn_poly_normal_pdf01
GaussianAnalysis.fourier.gauss_factor: gwE, Rintegral_cf_re_gauss_weight

lemma normal_pdf01N source, line 113

forall {R : realType} (x : R), normal_pdf (0 : R) 1 (- x) = normal_pdf (0 : R) 1 x

Statement as written in the source

Lemma normal_pdf01N (x : R) : phi (- x) = phi x.

Used by 1 declaration in 1 file

this file: normal_ibp

lemma cvgn_poly_normal_pdf01 source, line 116

forall {R : realType} [C : R] (k : nat),
0 <= C -> C * (1 + n%:R ^+ k) * normal_pdf (0 : R) 1 n%:R @[n --> \oo] --> 0

Statement as written in the source

Lemma cvgn_poly_normal_pdf01 (C : R) k : 0 <= C ->
  C * (1 + n%:R ^+ k) * phi n%:R @[n --> \oo] --> 0.

Used by 1 declaration in 1 file

this file: normal_ibp

lemma normal_ibp main result source, line 150

forall {R : realType} [f f' : R -> R] [C : R] [k : nat],
(forall x : R, is_derive x 1 f (f' x)) ->
continuous f' ->
(forall x : R, `|f x| <= C * (1 + `|x| ^+ k)) ->
(forall x : R, `|f' x| <= C * (1 + `|x| ^+ k)) ->
(\int[normal_prob 0 1]_x (x * f x)%:E)%E = (\int[normal_prob 0 1]_x (f' x)%:E)%E

Main result, as the README states it

Stein's identity: E[X f(X)] = E[f'(X)] for X of law normal_prob 0 1 and f differentiable with a continuous derivative, f and f' of polynomial growth.

Statement as written in the source

Lemma normal_ibp (f f' : R -> R) (C : R) (k : nat) :
  (forall x : R, is_derive x 1 f (f' x)) -> continuous f' ->
  (forall x, `|f x| <= C * (1 + `|x| ^+ k)) ->
  (forall x, `|f' x| <= C * (1 + `|x| ^+ k)) ->
  (\int[N]_x (x * f x)%:E = \int[N]_x (f' x)%:E)%E.

Used by 5 declarations in 3 files

this file: gauss_ibp0
GaussianAnalysis.gaussian.gauss_moments: normal_momentS, normal_mean
GaussianAnalysis.fourier.charfun: normal_x_sin, normal_x_cos

sectionis_derive_transfer

Context {R : realType} {V V' W : normedModType R}.

lemma is_derive_transfer source, line 276

forall {R : realType} {V V' W : normedModType R} [F : V -> W] [G : V' -> W] 
  [a v : V] [b w : V'] [d : W],
(forall h : R, F (h *: v + a) = G (h *: w + b)) -> is_derive b w G d -> is_derive a v F d

Two functions with the same difference quotients have the same directional derivative.

Statement as written in the source

Lemma is_derive_transfer (F : V -> W) (G : V' -> W) a v b w (d : W) :
  (forall h : R, F (h *: v + a) = G (h *: w + b)) ->
  is_derive b w G d -> is_derive a v F d.

Used by 18 declarations in 11 files

this file: gauss_ibp0, gauss_ibp_line, gauss_ibp2
GaussianAnalysis.gaussian.gauss_moments: gauss_cov
GaussianAnalysis.gaussian.partial_derivative: mean_value_coord
GaussianAnalysis.gaussian.gauss_interpolation: gauss_ibp_mulmx
GaussianAnalysis.random_matrix.goe: is_derive_mxentry, is_derive_goe_pow
GaussianAnalysis.random_matrix.matrix_series: is_derive_series_pow
GaussianAnalysis.comparison.gauss_smoothing: gauss_smooth_derive
GaussianAnalysis.comparison.gauss_concentration: herbst_is_derive_Fr
GaussianAnalysis.comparison.slepian: is_derive_expR_coord, is_derive_lift
GaussianAnalysis.comparison.gauss_law: is_derive_affine_comp
GaussianAnalysis.comparison.brascamp_lieb: gauss_ibp_unit, is_derive_comp_dir, is_derive_mxdot, cdF

sectiongauss_ibp

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

lemma rV_consD source, line 295

forall {R : realType} [m : nat] (t h : R) (v : 'rV_m),
rV_cons (h * 1 + t, v) = h *: delta_mx 0 0 + rV_cons (t, v)

Statement as written in the source

Lemma rV_consD m (t h : R) (v : 'rV[R]_m) :
  rV_cons (h * 1 + t, v) = h *: delta_mx 0 0 + rV_cons (t, v).

Used by 1 declaration in 1 file

this file: gauss_ibp0

lemma rV_cons_norm_exprn_le source, line 308

forall {R : realType} [m : nat] (t : R) (v : 'rV_m) (k : nat),
`|rV_cons (t, v)| ^+ k <= `|t| ^+ k + `|v| ^+ k

Statement as written in the source

Lemma rV_cons_norm_exprn_le m (t : R) (v : 'rV[R]_m) k :
  `|rV_cons (t, v)| ^+ k <= `|t| ^+ k + `|v| ^+ k.

Used by 1 declaration in 1 file

this file: gauss_ibp0

lemma integral_gauss_cons21 source, line 325

forall {R : realType} [m : nat] [f : 'rV_m.+1 -> \bar R],
(gauss m.+1).-integrable [set: 'rV_m.+1] f ->
(\int[gauss m.+1]_x f x)%E = (\int[gauss m]_v \int[normal_prob 0 1]_t f (rV_cons (t, v)))%E

Statement as written in the source

Lemma integral_gauss_cons21 m (f : 'rV[R]_m.+1 -> \bar R) :
  (gauss m.+1).-integrable [set: 'rV[R]_m.+1] f ->
  (\int[gauss m.+1]_x f x = \int[gauss m]_v \int[N]_t f (rV_cons (t, v)))%E.

Used by 1 declaration in 1 file

this file: gauss_ibp0

lemma gauss_ibp0 source, line 336

forall {R : realType} [m : nat] [F dF : 'rV_m.+1 -> R] [C : R] [k : nat],
(forall x : 'rV[R]_m.+1,
 is_derive x (delta_mx 0 0) F (dF x)) ->
measurable_fun [set: 'rV_m.+1] F ->
measurable_fun [set: 'rV_m.+1] dF ->
(forall x : 'rV[R]_m.+1,
 continuous (fun t : R => dF (t *: delta_mx 0 0 + x))) ->
(forall x : 'rV_m.+1, `|F x| <= C * (1 + `|x| ^+ k)) ->
(forall x : 'rV_m.+1, `|dF x| <= C * (1 + `|x| ^+ k)) ->
(\int[gauss m.+1]_x (x 0 0 * F x)%:E)%E = (\int[gauss m.+1]_x (dF x)%:E)%E

Statement as written in the source

Lemma gauss_ibp0 m (F dF : 'rV[R]_m.+1 -> R) (C : R) (k : nat) :
  (forall x, is_derive x (delta_mx 0 0) F (dF x)) ->
  measurable_fun [set: 'rV[R]_m.+1] F -> measurable_fun [set: 'rV[R]_m.+1] dF ->
  (forall x, continuous (fun t : R => dF (t *: delta_mx 0 0 + x))) ->
  (forall x, `|F x| <= C * (1 + `|x| ^+ k)) ->
  (forall x, `|dF x| <= C * (1 + `|x| ^+ k)) ->
  (\int[gauss m.+1]_x (x 0 0 * F x)%:E = \int[gauss m.+1]_x (dF x)%:E)%E.

Used by 1 declaration in 1 file

this file: gauss_ibp_line

lemma gauss_ibp_line main result source, line 383

forall {R : realType} [n : nat] [i : 'I_n] [F dF : 'rV_n -> R] [C : R] [k : nat],
(forall x : 'rV[R]_n,
 is_derive x (delta_mx 0 i) F (dF x)) ->
measurable_fun [set: 'rV_n] F ->
measurable_fun [set: 'rV_n] dF ->
(forall x : 'rV[R]_n,
 continuous (fun t : R => dF (t *: delta_mx 0 i + x))) ->
(forall x : 'rV_n, `|F x| <= C * (1 + `|x| ^+ k)) ->
(forall x : 'rV_n, `|dF x| <= C * (1 + `|x| ^+ k)) ->
(\int[gauss n]_x (x 0 i * F x)%:E)%E = (\int[gauss n]_x (dF x)%:E)%E

Integration by parts along the coordinate i, for F and its partial derivative dF measurable, dF continuous along the lines parallel to the i-th axis, both of polynomial growth.

Main result, as the README states it

The same identity when F and d_i F are only measurable and d_i F is continuous along the lines parallel to the i-th axis.

Statement as written in the source

Lemma gauss_ibp_line n (i : 'I_n) (F dF : 'rV[R]_n -> R) (C : R) (k : nat) :
  (forall x, is_derive x (delta_mx 0 i) F (dF x)) ->
  measurable_fun [set: 'rV[R]_n] F -> measurable_fun [set: 'rV[R]_n] dF ->
  (forall x, continuous (fun t : R => dF (t *: delta_mx 0 i + x))) ->
  (forall x, `|F x| <= C * (1 + `|x| ^+ k)) ->
  (forall x, `|dF x| <= C * (1 + `|x| ^+ k)) ->
  (\int[gauss n]_x (x 0 i * F x)%:E = \int[gauss n]_x (dF x)%:E)%E.

Used by 3 declarations in 2 files

this file: gauss_ibp, gauss_ibp2
GaussianAnalysis.comparison.brascamp_lieb: gauss_ibp_unit

lemma gauss_ibp main result source, line 427

forall {R : realType} [n : nat] [i : 'I_n] [F dF : 'rV_n -> R] [C : R] [k : nat],
(forall x : 'rV[R]_n,
 is_derive x (delta_mx 0 i) F (dF x)) ->
continuous F ->
continuous dF ->
(forall x : 'rV_n, `|F x| <= C * (1 + `|x| ^+ k)) ->
(forall x : 'rV_n, `|dF x| <= C * (1 + `|x| ^+ k)) ->
(\int[gauss n]_x (x 0 i * F x)%:E)%E = (\int[gauss n]_x (dF x)%:E)%E

Main result, as the README states it

Gaussian integration by parts: E[x_i F(x)] = E[d_i F(x)] for x of law gauss n, F continuous with a continuous partial derivative d_i F (along delta_mx 0 i), both of polynomial growth.

Used in theories/ by: Gaussian/Law/LibraryBridge, for Gaussian/Iterated/Stein

Statement as written in the source

Lemma gauss_ibp n (i : 'I_n) (F dF : 'rV[R]_n -> R) (C : R) (k : nat) :
  (forall x, is_derive x (delta_mx 0 i) F (dF x)) ->
  continuous F -> continuous dF ->
  (forall x, `|F x| <= C * (1 + `|x| ^+ k)) ->
  (forall x, `|dF x| <= C * (1 + `|x| ^+ k)) ->
  (\int[gauss n]_x (x 0 i * F x)%:E = \int[gauss n]_x (dF x)%:E)%E.

Used by 5 declarations in 5 files

GaussianAnalysis.gaussian.gauss_moments: gauss_cov
GaussianAnalysis.gaussian.gauss_interpolation: gauss_ibp_mulmx
GaussianAnalysis.random_matrix.goe: gauss_ibp_polyfun
GaussianAnalysis.comparison.gauss_concentration: gauss2_ibp_snd
GaussianAnalysis.comparison.gauss_law: gauss_smooth_partial_stein

lemma measurable_derive_rV main result source, line 444

forall {R : realType} [n : nat] [F dF : 'rV_n -> R] [v : 'rV_n],
measurable_fun [set: 'rV_n] F ->
(forall x : 'rV[R]_n,
 is_derive x v F (dF x)) ->
measurable_fun [set: 'rV_n] dF

A partial derivative of a measurable function is measurable: it is the limit of the difference quotients along the sequence 1 / (m + 1).

Main result, as the README states it

If a measurable function on 'rV[R]_n has at every point x a derivative dF x along a fixed vector v, then dF is measurable.

Statement as written in the source

Lemma measurable_derive_rV n (F dF : 'rV[R]_n -> R) (v : 'rV[R]_n) :
  measurable_fun [set: 'rV[R]_n] F -> (forall x, is_derive x v F (dF x)) ->
  measurable_fun [set: 'rV[R]_n] dF.

Used by 1 declaration in 1 file

this file: gauss_ibp2

lemma gauss_ibp2 main result source, line 469

forall {R : realType} [n : nat] [i : 'I_n] [F dF d2F : 'rV_n -> R] [C : R] [k : nat],
(forall x : 'rV[R]_n,
 is_derive x (delta_mx 0 i) F (dF x)) ->
(forall x : 'rV[R]_n,
 is_derive x (delta_mx 0 i) dF (d2F x)) ->
measurable_fun [set: 'rV_n] F ->
continuous d2F ->
(forall x : 'rV_n, `|F x| <= C * (1 + `|x| ^+ k)) ->
(forall x : 'rV_n, `|dF x| <= C * (1 + `|x| ^+ k)) ->
(forall x : 'rV_n, `|d2F x| <= C * (1 + `|x| ^+ k)) ->
(\int[gauss n]_x ((x 0 i ^+ 2 - 1) * F x)%:E)%E = (\int[gauss n]_x (d2F x)%:E)%E

Second-order integration by parts along the coordinate i: E[(x_i^2 - 1) F(x)] = E[d_i d_i F(x)], for F measurable with partial derivatives dF and d2F along the i-th axis, d2F continuous, all three of polynomial growth. dF need not be continuous.

Main result, as the README states it

Gaussian integration by parts of order two: E[(x_i^2 - 1) F(x)] = E[d_i d_i F(x)] for x of law gauss n, F measurable, d_i d_i F continuous, and F, d_i F and d_i d_i F of polynomial growth; d_i F need not be continuous.

Used in theories/ by: Gaussian/Law/LibraryBridge, for Gaussian/Iterated/Stein

Statement as written in the source

Lemma gauss_ibp2 n (i : 'I_n) (F dF d2F : 'rV[R]_n -> R) (C : R) (k : nat) :
  (forall x, is_derive x (delta_mx 0 i) F (dF x)) ->
  (forall x, is_derive x (delta_mx 0 i) dF (d2F x)) ->
  measurable_fun [set: 'rV[R]_n] F -> continuous d2F ->
  (forall x, `|F x| <= C * (1 + `|x| ^+ k)) ->
  (forall x, `|dF x| <= C * (1 + `|x| ^+ k)) ->
  (forall x, `|d2F x| <= C * (1 + `|x| ^+ k)) ->
  (\int[gauss n]_x ((x 0 i ^+ 2 - 1) * F x)%:E =
   \int[gauss n]_x (d2F x)%: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.