GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysiscomparisongauss_shift

Shifts of the standard Gaussian measure

GaussianAnalysis.comparison.gauss_shiftlibrary/comparison/gauss_shift.v209 lines9 lemmas and theoremssource
Imports 6 library modules and 26 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.matrix, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.numfun, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.probability_theory.normal_distribution

Imported by 2

The Cameron-Martin formula for gauss n: shifting a vector of law gauss n by h multiplies its law by the density expR (<h, x> - |h|^2 / 2). For f nonnegative and measurable, E[f (x + h)] = E[f x expR (<h, x> - |h|^2 / 2)] (ge0_integral_gauss_shift); the same identity holds for every measurable f, with integrals in the extended reals (integral_gauss_shift), and one side is integrable exactly when the other is (integrable_gauss_shift). The one-dimensional case is ge0_integral_normal_shift. The general case follows by induction on n, splitting off the first coordinate with rV_cons.

Main results

ResultsStatement
ge0_integral_gauss_shiftintegral_gauss_shift
Cameron-Martin formula: for x of law gauss n, E[f (x + h)] = E[f x expR (<h, x> - |h|^2 / 2)].

Declarations9 exported

lemma, theoremdefinitioninstancelocal
sectionnormal_shift
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Local Notation mu := (@lebesgue_measure R).
lemma normal_pdf01_shift source, line 43 
forall {R : realType} (a x : R),
normal_pdf 0 1 (x - a) = expR (a * x - a ^+ 2 / 2) * normal_pdf 0 1 x
Statement as written in the source
Lemma normal_pdf01_shift (a x : R) :
  normal_pdf 0 1 (x - a) = expR (a * x - a ^+ 2 / 2) * normal_pdf 0 1 x.
Used by 1 declaration in 1 file
lemma ge0_integral_normal_shift source, line 50 
forall {R : realType} (a : R) [f : R -> \bar R],
measurable_fun [set: R] f ->
(forall x : R, (0%R <= f x)%E) ->
(\int[normal_prob 0 1]_x f (x + a)%R)%E =
(\int[normal_prob 0 1]_x (f x * (expR (a * x - a ^+ 2 / 2))%:E))%E
Statement as written in the source
Lemma ge0_integral_normal_shift (a : R) (f : R -> \bar R) :
    measurable_fun [set: R] f -> (forall x, (0 <= f x)%E) ->
  (\int[N]_x f (x + a)%R = \int[N]_x (f x * (expR (a * x - a ^+ 2 / 2)%R)%:E))%E.
Used by 1 declaration in 1 file
sectionrV_cons_shift
Context {R : realType} {n : nat}.
lemma rV_cons_row_tail source, line 82 
forall {R : realType} {n : nat} (h : 'rV_n.+1), h = rV_cons (h 0 ord0, row_tail h)
Statement as written in the source
Lemma rV_cons_row_tail (h : 'rV[R]_n.+1) : h = rV_cons (h 0 ord0, row_tail h).
Used by 1 declaration in 1 file
lemma rV_consD2 source, line 89 
forall {R : realType} {n : nat} (t u : R) (v w : 'rV_n),
rV_cons (t, v) + rV_cons (u, w) = rV_cons (t + u, v + w)
Statement as written in the source
Lemma rV_consD2 (t u : R) (v w : 'rV[R]_n) :
  rV_cons (t, v) + rV_cons (u, w) = rV_cons (t + u, v + w).
Used by 1 declaration in 1 file
lemma measurable_mxdotl source, line 97 
forall {R : realType} {n : nat} (a : 'rV_n), measurable_fun [set: 'rV_n] (mxdot a)
Statement as written in the source
Lemma measurable_mxdotl (a : 'rV[R]_n) : measurable_fun [set: 'rV[R]_n] (mxdot a).
Used by 2 declarations in 2 files
lemma measurable_shift_density source, line 103 
forall {R : realType} {n : nat} (h : 'rV_n) (c : R),
measurable_fun [set: 'rV_n]
  (fun x : 'rV_n =>
   (expR (mxdot h x - c))%:E)
Statement as written in the source
Lemma measurable_shift_density (h : 'rV[R]_n) (c : R) :
  measurable_fun [set: 'rV[R]_n] (fun x => (expR (mxdot h x - c))%:E).
Used by 2 declarations in 1 file
sectiongauss_shift
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Local Open Scope ereal_scope.
theorem ge0_integral_gauss_shift main result source, line 119 
forall {R : realType} [n : nat] (h : 'rV_n) [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 + h)%R)%E =
(\int[gauss n]_x (f x * (expR (mxdot h x - mxdot h h / 2))%:E))%E

The Cameron-Martin formula: shifting a vector of law gauss n by h multiplies the law by the density expR (<h, x> - |h|^2 / 2).

Main result, as the README states it

Cameron-Martin formula: for x of law gauss n, E[f (x + h)] = E[f x expR (<h, x> - |h|^2 / 2)].

Statement as written in the source
Theorem ge0_integral_gauss_shift n (h : 'rV[R]_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 + h)%R =
  \int[gauss n]_x (f x * (expR (mxdot h x - mxdot h h / 2))%:E).
Used by 3 declarations in 2 files
lemma integrable_gauss_shift source, line 164 
forall {R : realType} [n : nat] (h : 'rV_n) [f : 'rV_n -> \bar R],
measurable_fun [set: 'rV_n] f ->
(gauss n).-integrable [set: 'rV_n] (fun x : 'rV_n => f (x + h)) <->
(gauss n).-integrable [set: 'rV_n]
  (fun x : 'rV_n => (f x * (expR (mxdot h x - mxdot h h / 2))%:E)%E)
Statement as written in the source
Lemma integrable_gauss_shift n (h : 'rV[R]_n) (f : 'rV[R]_n -> \bar R) :
  measurable_fun [set: 'rV[R]_n] f ->
  (gauss n).-integrable setT (fun x => f (x + h)%R) <->
  (gauss n).-integrable setT (fun x => f x * (expR (mxdot h x - mxdot h h / 2))%:E).
lemma integral_gauss_shift main result source, line 184 
forall {R : realType} [n : nat] (h : 'rV_n) [f : 'rV_n -> \bar R],
measurable_fun [set: 'rV_n] f ->
(\int[gauss n]_x f (x + h)%R)%E =
(\int[gauss n]_x (f x * (expR (mxdot h x - mxdot h h / 2))%:E))%E
Main result

Stated in the README together with ge0_integral_gauss_shift.

Statement as written in the source
Lemma integral_gauss_shift n (h : 'rV[R]_n) (f : 'rV[R]_n -> \bar R) :
  measurable_fun [set: 'rV[R]_n] f ->
  \int[gauss n]_x f (x + h)%R =
  \int[gauss n]_x (f x * (expR (mxdot h x - mxdot h h / 2))%:E).
Used by 1 declaration in 1 file
Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.