On this page

GaussianAnalysiscomparisonornstein_uhlenbeck

The Ornstein-Uhlenbeck semigroup

GaussianAnalysis.comparison.ornstein_uhlenbecklibrary/comparison/ornstein_uhlenbeck.v1,654 lines48 lemmas and theorems, 8 definitionssource

Imports 6 library modules and 28 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, 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.derive, mathcomp.analysis.realfun, 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, mathcomp.analysis.ftc

Imported by 1

GaussianAnalysis.comparison.brascamp_lieb

For f : R -> R bounded and measurable, the Mehler transform mehler r f x is E[f (r x + sqrt (1 - r^2) Z)] for Z of law normal_prob 0 1, and the Ornstein-Uhlenbeck semigroup is ou t f = mehler (expR (- t)) f (Mehler's formula, ouE). Then mehler 1 f = f and mehler 0 f is the mean of f (mehler1, mehler0, ou0), mehler r f keeps the bounds of f (mehler_le, mehler_ge), the standard normal law is invariant (integral_mehler) and mehler r is a contraction of L^1 of that law (mehler_contraction).

For |r| < 1 the law of r x + sqrt (1 - r^2) Z has the density mehler_kernel r x against normal_prob 0 1 (mehler_kernel_integral): the exponential of a quadratic polynomial in x and y. Differentiating it under the integral (is_derive_normal_kernel) gives the derivatives of mehler r f of order 1, 2 and 3 in x and the derivative in r (is_derive_mehler, is_derive_mehler_d1, is_derive_mehler_d2, is_derive_mehler_r), written as integrals against Hermite polynomials. They satisfy the generator identity r d/dr mehler r f = x (mehler r f)' - (mehler r f)'' (mehler_generator); for t > 0 it reads d/dt ou t f = (ou t f)'' - x (ou t f)' (is_derive_ou_t). The derivatives are bounded (mehler_d1_le, mehler_d2_le, mehler_dr_le) and continuous (continuous_mehler, continuous_mehler_d1, continuous_mehler_d2). The kernel gives the derivative in t as well as those in x, so it replaces the Cameron-Martin formula, which only shifts x.

As t -> +oo, ou t f x tends to the mean of f (ou_cvgy). As t -> 0 from the right, ou t f x tends to f x when f is continuous (ou_cvg0, mehler_cvg1), and ou t f tends to f in L^1 of the standard normal law for every bounded measurable f (ou_cvg0_L1, mehler_cvg_L1). The last limit goes through the density of bounded continuous functions in that space (normal_continuous_approx), which follows from the density of continuous functions in L^1 of Lebesgue measure on a segment (approximation_continuous_integrable of MathComp-Analysis).

`mehler_kernel r x y`	the density at y, against normal_prob 0 1, of the law of r x + sqrt (1 - r^2) Z, \|r\| < 1
`mehler r f x`	E[f (r x + b Z)], with b = sqrt (1 - r^2)
`mehler_d1 r f x`	r / b * E[f (r x + b Z) Z], the derivative of mehler r f at x
`mehler_d2 r f x`	r^2 / b^2 * E[f (r x + b Z) (Z^2 - 1)]
`mehler_d3 r f x`	r^3 / b^3 * E[f (r x + b Z) (Z^3 - 3 Z)]
`mehler_dr r f x`	E[f (r x + b Z) (x Z / b - r (Z^2 - 1) / b^2)], the derivative of r \|-> mehler r f x
`ou t f x`	mehler (expR (- t)) f x
`mehler_bound r1 X`	a constant C such that the kernel times a polynomial factor of degree 3 is at most C expR (c \|y\|) for \|r\| <= r1 < 1, \|x\| <= X

Main results

Results	Statement
mehlerououEmehler1mehler0ou0	The Mehler transform `mehler r f x = E[f (r x + sqrt (1 - r^2) Z)]`, `Z` of law `normal_prob 0 1`, and the Ornstein-Uhlenbeck semigroup `ou t f = mehler (expR (- t)) f` (Mehler's formula). `mehler 1 f = f` and `mehler 0 f` is the mean of `f`.
mehler_lemehler_geintegral_mehlermehler_contraction	For `f` bounded and measurable: the bounds of `f` hold for `mehler r f`; for `\|r\| < 1` the standard normal law is invariant, `E[mehler r f] = E[f]`, and `mehler r` is a contraction of `L^1` of that law.
mehler_kernel_integral	For `\|r\| < 1` the law of `r x + sqrt (1 - r^2) Z` has the density `mehler_kernel r x`, an explicit exponential of a quadratic polynomial, with respect to `normal_prob 0 1`.
is_derive_normal_kernel	Differentiation under the integral against `normal_prob 0 1`, with a bounded measurable factor, for a kernel and its derivative in the parameter dominated by `C expR (c \|y\|)` on an open interval.
is_derive_mehleris_derive_mehler_d1is_derive_mehler_d2is_derive_mehler_rmehler_generator	For `f` bounded and measurable and `\|r\| < 1`, `mehler r f` has derivatives of order 1, 2 and 3 in `x` and a derivative in `r`, given by integrals against Hermite polynomials (`mehler_d1`, `mehler_d2`, `mehler_d3`, `mehler_dr`): for instance `(mehler r f)' x = r / b E[f (r x + b Z) Z]` with `b = sqrt (1 - r^2)`. Generator identity: `r d/dr mehler r f = x (mehler r f)' - (mehler r f)''`.
is_derive_ouis_derive_ou_d1is_derive_ou_t	For `t > 0`, the first two derivatives of `ou t f` in `x`, and `d/dt ou t f x = (ou t f)'' x - x (ou t f)' x`.
mehler_d1_lemehler_d2_lemehler_dr_lecontinuous_mehlercontinuous_mehler_d1continuous_mehler_d2measurable_mehler	For `\|f\| <= K` and `\|r\| < 1`: `\|(mehler r f)'\| <= \|r\| / b K E\|Z\|`, `\|(mehler r f)''\| <= r^2 / b^2 K E\|Z^2 - 1\|`, `\|d/dr mehler r f x\| <= \|x\| / b K E\|Z\| + \|r\| / b^2 K E\|Z^2 - 1\|`; `mehler r f` and its first two derivatives are continuous.
ou_cvgyou_cvg0ou_cvg0_L1mehler_cvg1mehler_cvg_L1continuous_mehler_xcontinuous_mehler_r	As `t -> +oo`, `ou t f x` tends to the mean of `f`. As `t -> 0` from the right (`r -> 1`), `ou t f x` tends to `f x` for `f` continuous and bounded, and `ou t f` tends to `f` in `L^1` of the standard normal law for every bounded measurable `f`.
normal_continuous_approx	Bounded continuous functions are dense in `L^1` of the standard normal law: a measurable `f` with values in `[lo, hi]` is within `eps` of a continuous `h` with values in `[lo, hi]`.

Declarations56 exported, 40 local

sectionmehler_def

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Implicit Types (r x y : R) (f : R -> R).

definition mehler_kernel source, line 84

Type

forall {R : realType}, R -> R -> R -> R

Definition

Definition mehler_kernel r x y : R :=
  expR (- ln (1 - r ^+ 2) / 2 +
    (2 * r * x * y - r ^+ 2 * (x ^+ 2 + y ^+ 2)) / (2 * (1 - r ^+ 2))).

The density at y, against the standard normal law, of the law of r x + sqrt (1 - r^2) Z for Z standard normal, when |r| < 1.

Used by 22 declarations in 1 file

this file: mehler_kernel_gt0, normal_pdf_mehler, measurable_mehler_kernel, mehler_kernel_integral, mehler_kernel_le, mehler_kernel_mul_le, is_derive_kx, is_derive_kpx, is_derive_k1, is_derive_k2, is_derive_kr, kernel_bounds, hermite_eq, mehlerE, mehler_d1E, mehler_d2E, mehler_d3E, mehler_drE, is_derive_mehler, is_derive_mehler_d1, is_derive_mehler_d2, is_derive_mehler_r

definition mehler main result source, line 89

Type

forall {R : realType}, R -> (R -> R) -> R -> R

Definition

Definition mehler r f x : R :=
  \int[N]_z f (r * x + Num.sqrt (1 - r ^+ 2) * z).

The Mehler transform with correlation r: E[f (r x + sqrt (1 - r^2) Z)].

Main result, as the README states it

The Mehler transform mehler r f x = E[f (r x + sqrt (1 - r^2) Z)], Z of law normal_prob 0 1, and the Ornstein-Uhlenbeck semigroup ou t f = mehler (expR (- t)) f (Mehler's formula). mehler 1 f = f and mehler 0 f is the mean of f.

Used by 26 declarations in 2 files

this file: ou, mehler1, mehler0, ouE, mehler_le, mehler_ge, mehlerE, is_derive_mehler, is_derive_mehler_r, continuous_mehler, measurable_mehler, integral_mehler, mehler_contraction, ou_cvgy, continuous_mehler_x, continuous_mehler_r, mehler_cvg1, mehler_L1_le, continuous_mehler_r_abs, mehler_L1_near, mehler_cvg_L1, ou_cvg0_L1, ou_cvg0
GaussianAnalysis.comparison.brascamp_lieb: g, Lambda_lip, Lambda_cvg1

definition mehler_d1 source, line 93

Type

forall {R : realType}, R -> (R -> R) -> R -> R

Definition

Definition mehler_d1 r f x : R :=
  r / Num.sqrt (1 - r ^+ 2) *
  \int[N]_z (f (r * x + Num.sqrt (1 - r ^+ 2) * z) * z).

Its derivatives of order 1, 2 and 3 in x, and its derivative in r.

Used by 10 declarations in 2 files

this file: mehler_d1E, is_derive_mehler, is_derive_mehler_d1, mehler_generator, continuous_mehler_d1, mehler_d1_le, is_derive_ou, is_derive_ou_d1, is_derive_ou_t
GaussianAnalysis.comparison.brascamp_lieb: g1

definition mehler_d2 source, line 97

Type

forall {R : realType}, R -> (R -> R) -> R -> R

Definition

Definition mehler_d2 r f x : R :=
  r ^+ 2 / (1 - r ^+ 2) *
  \int[N]_z (f (r * x + Num.sqrt (1 - r ^+ 2) * z) * (z ^+ 2 - 1)).

Used by 9 declarations in 2 files

this file: mehler_d2E, is_derive_mehler_d1, is_derive_mehler_d2, mehler_generator, continuous_mehler_d2, mehler_d2_le, is_derive_ou_d1, is_derive_ou_t
GaussianAnalysis.comparison.brascamp_lieb: g2

definition mehler_d3 source, line 101

Type

forall {R : realType}, R -> (R -> R) -> R -> R

Definition

Definition mehler_d3 r f x : R :=
  r ^+ 3 / Num.sqrt (1 - r ^+ 2) ^+ 3 *
  \int[N]_z (f (r * x + Num.sqrt (1 - r ^+ 2) * z) * (z ^+ 3 - 3 * z)).

Used by 2 declarations in 1 file

this file: mehler_d3E, is_derive_mehler_d2

definition mehler_dr source, line 105

Type

forall {R : realType}, R -> (R -> R) -> R -> R

Definition

Definition mehler_dr r f x : R :=
  \int[N]_z (f (r * x + Num.sqrt (1 - r ^+ 2) * z) *
    (x * z / Num.sqrt (1 - r ^+ 2) - r * (z ^+ 2 - 1) / (1 - r ^+ 2))).

Used by 9 declarations in 2 files

this file: mehler_drE, is_derive_mehler_r, mehler_generator, mehler_dr_split, mehler_dr_le
GaussianAnalysis.comparison.brascamp_lieb: dG, is_derive_G, is_derive_Lambda, rdG

definition ou main result source, line 110

Type

forall {R : realType}, R -> (R -> R) -> R -> R

Definition

Definition ou (t : R) f x : R := mehler (expR (- t)) f x.

The Ornstein-Uhlenbeck semigroup, by Mehler's formula.

Main result

Stated in the README together with mehler.

Used by 7 declarations in 1 file

this file: ouE, ou0, is_derive_ou, is_derive_ou_t, ou_cvgy, ou_cvg0_L1, ou_cvg0

sectionmehler_basic

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Implicit Types (r x y : R) (f : R -> R).

lemma mehler1 main result source, line 119

forall {R : realType} (f : R -> R) (x : R), mehler 1 f x = f x

Main result

Stated in the README together with mehler.

Statement as written in the source

Lemma mehler1 f x : mehler 1 f x = f x.

Used by 6 declarations in 2 files

this file: ou0, mehler_cvg1, mehler_L1_near
GaussianAnalysis.comparison.brascamp_lieb: measurable_G, Lambda1, G1

lemma mehler0 main result source, line 126

forall {R : realType} (f : R -> R) (x : R), mehler 0 f x = \int[normal_prob 0 1]_z f z

Main result

Stated in the README together with mehler.

Statement as written in the source

Lemma mehler0 f x : mehler 0 f x = \int[N]_z f z.

Used by 2 declarations in 2 files

this file: ou_cvgy
GaussianAnalysis.comparison.brascamp_lieb: Lambda0

lemma ouE main result source, line 132

forall {R : realType} (t : R) (f : R -> R) (x : R),
ou t f x =
\int[normal_prob 0 1]_z f (expR (- t) * x + Num.ExtraDef.sqrtr (1 - expR (- (2 * t))) * z)

Main result

Stated in the README together with mehler.

Statement as written in the source

Lemma ouE (t : R) f x :
  ou t f x = \int[N]_z f (expR (- t) * x + Num.sqrt (1 - expR (- (2 * t))) * z).

lemma ou0 main result source, line 136

forall {R : realType} (f : R -> R) (x : R), ou 0 f x = f x

Main result

Stated in the README together with mehler.

Statement as written in the source

Lemma ou0 f x : ou 0 f x = f x.

Used by 1 declaration in 1 file

this file: ou_cvg0

lemma integrable_normal_bounded source, line 139

forall {R : realType} [F : R -> R] [K : R],
measurable_fun [set: R] F ->
(forall z : R, `|F z| <= K) -> (normal_prob 0 1).-integrable [set: R] (EFin \o F)

Statement as written in the source

Lemma integrable_normal_bounded (F : R -> R) (K : R) :
  measurable_fun [set: R] F -> (forall z, `|F z| <= K) ->
  N.-integrable [set: R] (EFin \o F).

Used by 11 declarations in 1 file

this file: normr_Rintegral_normal_le, Rintegral_normal_ge, mehlerE, integrable_maff, integral_mehler, mehler_contraction, normal_continuous_approx, integrable_cst, continuous_mehler_x, continuous_mehler_r, integrable_abs_bounded

lemma normr_Rintegral_normal_le source, line 148

forall {R : realType} [F : R -> R] [K : R],
measurable_fun [set: R] F ->
(forall z : R, `|F z| <= K) -> `|\int[normal_prob 0 1]_z F z| <= K

Statement as written in the source

Lemma normr_Rintegral_normal_le (F : R -> R) (K : R) :
  measurable_fun [set: R] F -> (forall z, `|F z| <= K) ->
  `|\int[N]_z F z| <= K.

Used by 1 declaration in 1 file

this file: mehler_le

lemma Rintegral_normal_ge source, line 165

forall {R : realType} [F : R -> R] [a K : R],
measurable_fun [set: R] F ->
(forall z : R, `|F z| <= K) -> (forall z : R, a <= F z) -> a <= \int[normal_prob 0 1]_z F z

Statement as written in the source

Lemma Rintegral_normal_ge (F : R -> R) (a K : R) :
  measurable_fun [set: R] F -> (forall z, `|F z| <= K) -> (forall z, a <= F z)
    ->
  a <= \int[N]_z F z.

Used by 2 declarations in 2 files

this file: mehler_ge
GaussianAnalysis.comparison.brascamp_lieb: gauss_brascamp_lieb_bounded_sec

let maff section-local source, line 179

Let maff r x : measurable_fun [set: R] (fun z => r * x + Num.sqrt (1 - r ^+ 2)
  * z).

Used by 2 declarations in 1 file

this file: mehler_le, mehler_ge

lemma mehler_le main result source, line 183

forall {R : realType} [f : R -> R] (r x : R) [K : R],
measurable_fun [set: R] f -> (forall y : R, `|f y| <= K) -> `|mehler r f x| <= K

Main result, as the README states it

For f bounded and measurable: the bounds of f hold for mehler r f; for |r| < 1 the standard normal law is invariant, E[mehler r f] = E[f], and mehler r is a contraction of L^1 of that law.

Statement as written in the source

Lemma mehler_le f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|mehler r f x| <= K.

Used by 5 declarations in 2 files

this file: mehler_contraction, mehler_L1_le, mehler_L1_near
GaussianAnalysis.comparison.brascamp_lieb: gb, Lambda_lip

lemma mehler_ge main result source, line 190

forall {R : realType} [f : R -> R] (r x : R) [a K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) -> (forall y : R, a <= f y) -> a <= mehler r f x

Main result

Stated in the README together with mehler_le.

Statement as written in the source

Lemma mehler_ge f r x (a K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> (forall y, a <= f y) -> a <= mehler r f x.

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.brascamp_lieb: gb

sectionderive_poly

Context {R : realType}.

lemma is_derive_cubic source, line 202

forall {R : realType} (a0 a1 a2 a3 x : R),
is_derive x 1
  (fun x0 : R =>
   a0 + a1 * x0 + a2 * x0 ^+ 2 + a3 * x0 ^+ 3)
  (a1 + 2 * a2 * x + 3 * a3 * x ^+ 2)

Statement as written in the source

Lemma is_derive_cubic (a0 a1 a2 a3 x : R) :
  is_derive x 1 (fun x => a0 + a1 * x + a2 * x ^+ 2 + a3 * x ^+ 3)
    (a1 + 2 * a2 * x + 3 * a3 * x ^+ 2).

Used by 1 declaration in 1 file

this file: is_derive_cubicE

sectionmehler_kernel

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Local Notation mu := (@lebesgue_measure R).
Implicit Types (r x y : R).

lemma onem_sqr_gt0 source, line 228

forall {R : realType} [r : R], `|r| < 1 -> 0 < 1 - r ^+ 2

Statement as written in the source

Lemma onem_sqr_gt0 r : `|r| < 1 -> 0 < 1 - r ^+ 2.

Used by 17 declarations in 2 files

this file: normal_pdf_mehler, mehler_kernel_integral, is_derive_kx, is_derive_k1, is_derive_k2, is_derive_kr, mehler_d1E, mehler_d2E, mehler_d3E, mehler_drE, mehler_generator, mehler_d1_le, mehler_d2_le, integral_mehler, mehler_dr_split, mehler_dr_le
GaussianAnalysis.comparison.brascamp_lieb: w0

lemma mehler_kernel_gt0 source, line 231

forall {R : realType} (r x y : R), 0 < mehler_kernel r x y

Statement as written in the source

Lemma mehler_kernel_gt0 r x y : 0 < mehler_kernel r x y.

Used by 1 declaration in 1 file

this file: mehler_kernel_mul_le

lemma expR_lnN_half source, line 234

forall {R : realType} [v : R], 0 < v -> expR (- ln v / 2) = (Num.ExtraDef.sqrtr v)^-1

Statement as written in the source

Lemma expR_lnN_half (v : R) : 0 < v -> expR (- ln v / 2) = (Num.sqrt v)^-1.

Used by 1 declaration in 1 file

this file: normal_pdf_mehler

lemma normal_pdf_mehler source, line 240

forall {R : realType} [r : R] (x y : R),
`|r| < 1 ->
normal_pdf (r * x) (Num.ExtraDef.sqrtr (1 - r ^+ 2)) y =
mehler_kernel r x y * normal_pdf 0 1 y

Statement as written in the source

Lemma normal_pdf_mehler r x y : `|r| < 1 ->
  normal_pdf (r * x) (Num.sqrt (1 - r ^+ 2)) y =
  mehler_kernel r x y * normal_pdf 0 1 y.

Used by 1 declaration in 1 file

this file: mehler_kernel_integral

lemma measurable_mehler_kernel source, line 257

forall {R : realType} (r x : R), measurable_fun [set: R] (mehler_kernel r x)

Statement as written in the source

Lemma measurable_mehler_kernel r x :
  measurable_fun [set: R] (mehler_kernel r x).

Used by 5 declarations in 1 file

this file: mehler_kernel_integral, is_derive_mehler, is_derive_mehler_d1, is_derive_mehler_d2, is_derive_mehler_r

lemma mehler_kernel_integral main result source, line 268

forall {R : realType} [r x : R] [F : R -> R],
`|r| < 1 ->
measurable_fun [set: R] F ->
(normal_prob 0 1).-integrable [set: R]
  (EFin \o
     (fun z : join_Num_NumDomain_between_Order_Preorder_and_GRing_PzSemiRing R =>
      F (r * x + Num.ExtraDef.sqrtr (1 - r ^+ 2) * z))) ->
\int[normal_prob 0 1]_z F (r * x + Num.ExtraDef.sqrtr (1 - r ^+ 2) * z) =
\int[normal_prob 0 1]_y (F y * mehler_kernel r x y)

The law of r x + sqrt (1 - r^2) Z, for Z standard normal and |r| < 1, has the density mehler_kernel r x against the standard normal law.

Main result, as the README states it

For |r| < 1 the law of r x + sqrt (1 - r^2) Z has the density mehler_kernel r x, an explicit exponential of a quadratic polynomial, with respect to normal_prob 0 1.

Statement as written in the source

Lemma mehler_kernel_integral r x (F : R -> R) : `|r| < 1 ->
  measurable_fun [set: R] F ->
  N.-integrable [set: R] (EFin \o (fun z => F (r * x + Num.sqrt (1 - r ^+ 2) *
    z))) ->
  \int[N]_z F (r * x + Num.sqrt (1 - r ^+ 2) * z) =
  \int[N]_y (F y * mehler_kernel r x y).

Used by 2 declarations in 1 file

this file: hermite_eq, mehlerE

sectionmehler_kernel_bounds

Context {R : realType}.
Implicit Types (r x y : R).

lemma mehler_kernel_le source, line 332

forall {R : realType} [r x : R] (y : R) [r1 : R]
  [X : {|
         Num.POrderZmodule.sort := R;
         Num.POrderZmodule.class :=
           {|
             Num.POrderZmodule.choice_hasChoice_mixin := Real.class R;
             Num.POrderZmodule.eqtype_hasDecEq_mixin := Real.class R;
             Num.POrderZmodule.Order_isDuallyPreorder_mixin := Real.class R;
             Num.POrderZmodule.Order_Preorder_isDuallyPOrder_mixin := Real.class R;
             Num.POrderZmodule.Algebra_hasOpp_mixin := Real.class R;
             Num.POrderZmodule.Algebra_hasZero_mixin := Real.class R;
             Num.POrderZmodule.Algebra_hasAdd_mixin := Real.class R;
             Num.POrderZmodule.Algebra_BaseZmoduleNmodule_isZmodule_mixin := Real.class R;
             Num.POrderZmodule.Algebra_BaseAddUMagma_isAddUMagma_mixin := Real.class R;
             Num.POrderZmodule.Algebra_BaseAddMagma_isAddMagma_mixin := Real.class R;
             Num.POrderZmodule.Algebra_AddMagma_isAddSemigroup_mixin := Real.class R
           |}
       |}],
0 <= r1 < 1 ->
`|r| <= r1 ->
`|x| <= X ->
mehler_kernel r x y <= expR (- ln (1 - r1 ^+ 2) / 2) * expR (X / (1 - r1 ^+ 2) * `|y|)

Statement as written in the source

Lemma mehler_kernel_le r x y r1 X : 0 <= r1 < 1 -> `|r| <= r1 -> `|x| <= X ->
  mehler_kernel r x y <=
  expR (- ln (1 - r1 ^+ 2) / 2) * expR (X / (1 - r1 ^+ 2) * `|y|).

Used by 1 declaration in 1 file

this file: mehler_kernel_mul_le

definition mehler_bound source, line 362

Type

forall {R : realType}, R -> R -> R

Definition

Definition mehler_bound (r1 X : R) : R :=
  24 * expR (- ln (1 - r1 ^+ 2) / 2) * expR (X + 1) / (1 - r1 ^+ 2) ^+ 3.

Used by 6 declarations in 1 file

this file: mehler_kernel_mul_le, kernel_bounds, is_derive_mehler, is_derive_mehler_d1, is_derive_mehler_d2, is_derive_mehler_r

lemma mehler_kernel_mul_le source, line 365

forall {R : realType} [r x y r1 : R]
  [X : {|
         Num.POrderZmodule.sort := R;
         Num.POrderZmodule.class :=
           {|
             Num.POrderZmodule.choice_hasChoice_mixin := Real.class R;
             Num.POrderZmodule.eqtype_hasDecEq_mixin := Real.class R;
             Num.POrderZmodule.Order_isDuallyPreorder_mixin := Real.class R;
             Num.POrderZmodule.Order_Preorder_isDuallyPOrder_mixin := Real.class R;
             Num.POrderZmodule.Algebra_hasOpp_mixin := Real.class R;
             Num.POrderZmodule.Algebra_hasZero_mixin := Real.class R;
             Num.POrderZmodule.Algebra_hasAdd_mixin := Real.class R;
             Num.POrderZmodule.Algebra_BaseZmoduleNmodule_isZmodule_mixin := Real.class R;
             Num.POrderZmodule.Algebra_BaseAddUMagma_isAddUMagma_mixin := Real.class R;
             Num.POrderZmodule.Algebra_BaseAddMagma_isAddMagma_mixin := Real.class R;
             Num.POrderZmodule.Algebra_AddMagma_isAddSemigroup_mixin := Real.class R
           |}
       |}]
  [p : R],
0 <= r1 < 1 ->
`|r| <= r1 ->
`|x| <= X ->
`|p| <= 4 * (`|y| + X + 1) ^+ 3 / (1 - r1 ^+ 2) ^+ 3 ->
`|mehler_kernel r x y * p| <= mehler_bound r1 X * expR ((X / (1 - r1 ^+ 2) + 1) * `|y|)

Statement as written in the source

Lemma mehler_kernel_mul_le r x y r1 X (p : R) : 0 <= r1 < 1 -> `|r| <= r1 ->
  `|x| <= X -> `|p| <= 4 * (`|y| + X + 1) ^+ 3 / (1 - r1 ^+ 2) ^+ 3 ->
  `|mehler_kernel r x y * p| <=
  mehler_bound r1 X * expR ((X / (1 - r1 ^+ 2) + 1) * `|y|).

Used by 1 declaration in 1 file

this file: kernel_bounds

sectionnormal_kernel_derive

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

lemma is_derive_normal_kernel main result source, line 410

forall {R : realType} [f : R -> R] [K : R] [k dk : R -> R -> R] [u v s C c : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
s \in `]u, v[ ->
(forall s' : R, measurable_fun [set: R] (k s')) ->
(forall s' y : R, s' \in `]u, v[ -> is_derive s' 1 (k^~ y) (dk s' y)) ->
(forall s' y : R, s' \in `]u, v[ -> `|k s' y| <= C * expR (c * `|y|)) ->
(forall s' y : R, s' \in `]u, v[ -> `|dk s' y| <= C * expR (c * `|y|)) ->
is_derive s 1
  (fun s' : R =>
   \int[normal_prob 0 1]_y (f y * k s' y))
  (\int[normal_prob 0 1]_y (f y * dk s y))

Differentiation under the integral sign against the standard normal law, for a parameter kernel k s y and its derivative dk s y in s, both dominated by C expR (c |y|) for s in an open interval.

Main result, as the README states it

Differentiation under the integral against normal_prob 0 1, with a bounded measurable factor, for a kernel and its derivative in the parameter dominated by C expR (c |y|) on an open interval.

Statement as written in the source

Lemma is_derive_normal_kernel (f : R -> R) (K : R) (k dk : R -> R -> R)
    (u v s C c : R) :
  measurable_fun [set: R] f -> (forall y, `|f y| <= K) -> s \in `]u, v[ ->
  (forall s', measurable_fun [set: R] (k s')) ->
  (forall s' y, s' \in `]u, v[ -> is_derive s' 1 (k ^~ y) (dk s' y)) ->
  (forall s' y, s' \in `]u, v[ -> `|k s' y| <= C * expR (c * `|y|)) ->
  (forall s' y, s' \in `]u, v[ -> `|dk s' y| <= C * expR (c * `|y|)) ->
  is_derive s 1 (fun s' => \int[N]_y (f y * k s' y)) (\int[N]_y (f y * dk s y)).

Used by 4 declarations in 1 file

this file: is_derive_mehler, is_derive_mehler_d1, is_derive_mehler_d2, is_derive_mehler_r

sectionmehler_derive

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Implicit Types (r x y : R) (f : R -> R).

lemma is_derive_cubicE source, line 449

forall {R : realType} [p : R -> R] [a0 a1 a2 a3 x d : R],
(forall t : R, p t = a0 + a1 * t + a2 * t ^+ 2 + a3 * t ^+ 3) ->
d = a1 + 2 * a2 * x + 3 * a3 * x ^+ 2 -> is_derive x 1 p d

Statement as written in the source

Lemma is_derive_cubicE (p : R -> R) (a0 a1 a2 a3 x d : R) :
  (forall t, p t = a0 + a1 * t + a2 * t ^+ 2 + a3 * t ^+ 3) ->
  d = a1 + 2 * a2 * x + 3 * a3 * x ^+ 2 -> is_derive x 1 p d.

Used by 5 declarations in 2 files

this file: is_derive_kx, is_derive_k1, is_derive_k2, is_derive_kr
GaussianAnalysis.comparison.brascamp_lieb: is_derive_mxdot

let mk1 section-local source, line 460

Let mk1 r x y := r * (y - r * x) / (1 - r ^+ 2).

The polynomial factors of the derivatives of the kernel.

Used by 8 declarations in 1 file

this file: is_derive_kx, is_derive_kpx, is_derive_k1, is_derive_k2, measurable_mk1, mehler_d1E, is_derive_mehler, is_derive_mehler_d1

let mk2 section-local source, line 461

Let mk2 r x y := r ^+ 2 * ((y - r * x) ^+ 2 - (1 - r ^+ 2)) / (1 - r ^+ 2) ^+ 2.

Used by 6 declarations in 1 file

this file: is_derive_k1, is_derive_k2, measurable_mk2, mehler_d2E, is_derive_mehler_d1, is_derive_mehler_d2

let mk3 section-local source, line 462

Let mk3 r x y :=
  r ^+ 3 * ((y - r * x) ^+ 3 - 3 * (1 - r ^+ 2) * (y - r * x)) / (1 - r ^+ 2)
    ^+ 3.

Used by 4 declarations in 1 file

this file: is_derive_k2, measurable_mk3, mehler_d3E, is_derive_mehler_d2

let mkr section-local source, line 465

Let mkr r x y := (x * (y - r * x) * (1 - r ^+ 2) - r * (y - r * x) ^+ 2 +
  r * (1 - r ^+ 2)) / (1 - r ^+ 2) ^+ 2.

Used by 4 declarations in 1 file

this file: is_derive_kr, measurable_mkr, mehler_drE, is_derive_mehler_r

let is_derive_kx section-local source, line 468

Let is_derive_kx r x y : `|r| < 1 ->
  is_derive x 1 (fun x => mehler_kernel r x y)
    (mehler_kernel r x y * mk1 r x y).

Used by 2 declarations in 1 file

this file: is_derive_kpx, is_derive_mehler

let is_derive_kpx section-local source, line 486

Let is_derive_kpx r x y (p : R -> R) (dp : R) : `|r| < 1 -> is_derive x 1 p dp
  ->
  is_derive x 1 (fun x => mehler_kernel r x y * p x)
    (mehler_kernel r x y * (mk1 r x y * p x + dp)).

Used by 2 declarations in 1 file

this file: is_derive_k1, is_derive_k2

let is_derive_k1 section-local source, line 495

Let is_derive_k1 r x y : `|r| < 1 ->
  is_derive x 1 (fun x => mehler_kernel r x y * mk1 r x y)
    (mehler_kernel r x y * mk2 r x y).

Used by 1 declaration in 1 file

this file: is_derive_mehler_d1

let is_derive_k2 section-local source, line 510

Let is_derive_k2 r x y : `|r| < 1 ->
  is_derive x 1 (fun x => mehler_kernel r x y * mk2 r x y)
    (mehler_kernel r x y * mk3 r x y).

Used by 1 declaration in 1 file

this file: is_derive_mehler_d2

let is_derive_kr section-local source, line 527

Let is_derive_kr r x y : `|r| < 1 ->
  is_derive r 1 (fun r => mehler_kernel r x y)
    (mehler_kernel r x y * mkr r x y).

Used by 1 declaration in 1 file

this file: is_derive_mehler_r

let frac_le section-local source, line 560

Let frac_le (a P w w1 : R) (j : nat) : 0 < w1 -> w1 <= w -> w <= 1 ->
  (j <= 3)%N -> `|a| <= 4 * P ^+ 3 -> `|a / w ^+ j| <= 4 * P ^+ 3 / w1 ^+ 3.

Bounds on the polynomial factors, for |r| <= r1 < 1 and |x| <= X.

Used by 1 declaration in 1 file

this file: kernel_bounds

let num_le section-local source, line 574

Let num_le r x y X : `|r| <= 1 -> `|x| <= X ->
  let P := `|y| + X + 1 in let z := y - r * x in let w := 1 - r ^+ 2 in
  [/\ `|r * z| <= 4 * P ^+ 3, `|r ^+ 2 * (z ^+ 2 - w)| <= 4 * P ^+ 3,
      `|r ^+ 3 * (z ^+ 3 - 3 * w * z)| <= 4 * P ^+ 3 &
      `|x * z * w - r * z ^+ 2 + r * w| <= 4 * P ^+ 3].

Used by 4 declarations in 1 file

this file: is_derive_mehler, is_derive_mehler_d1, is_derive_mehler_d2, is_derive_mehler_r

let kernel_bounds section-local source, line 624

Let kernel_bounds r x y r1 X (j : nat) (a : R) : 0 <= r1 < 1 -> `|r| <= r1 ->
  `|x| <= X -> (j <= 3)%N -> `|a| <= 4 * (`|y| + X + 1) ^+ 3 ->
  `|mehler_kernel r x y * (a / (1 - r ^+ 2) ^+ j)| <=
  mehler_bound r1 X * expR ((X / (1 - r1 ^+ 2) + 1) * `|y|).

Used by 4 declarations in 1 file

this file: is_derive_mehler, is_derive_mehler_d1, is_derive_mehler_d2, is_derive_mehler_r

let integrable_fpoly section-local source, line 637

Let integrable_fpoly f r x (h : R -> R) (K C0 : R) (k : nat) :
  measurable_fun [set: R] f -> (forall y, `|f y| <= K) ->
  measurable_fun [set: R] h -> (forall z, `|h z| <= C0 * (1 + `|z| ^+ k)) ->
  N.-integrable [set: R]
    (EFin \o (fun z => f (r * x + Num.sqrt (1 - r ^+ 2) * z) * h z)).

Used by 5 declarations in 1 file

this file: hermite_eq, mehler_d1E, mehler_d2E, mehler_d3E, mehler_generator

let hermite_eq section-local source, line 650

Let hermite_eq f r x (K : R) (q h : R -> R) (C0 : R) (k : nat) : `|r| < 1 ->
  measurable_fun [set: R] f -> (forall y, `|f y| <= K) ->
  measurable_fun [set: R] q -> measurable_fun [set: R] h ->
  (forall z, q (r * x + Num.sqrt (1 - r ^+ 2) * z) = h z) ->
  (forall z, `|h z| <= C0 * (1 + `|z| ^+ k)) ->
  \int[N]_z (f (r * x + Num.sqrt (1 - r ^+ 2) * z) * h z) =
  \int[N]_y (f y * (mehler_kernel r x y * q y)).

Used by 4 declarations in 1 file

this file: mehler_d1E, mehler_d2E, mehler_d3E, mehler_drE

let mehlerE section-local source, line 669

Let mehlerE f r x (K : R) : `|r| < 1 -> measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) ->
  mehler r f x = \int[N]_y (f y * mehler_kernel r x y).

Used by 2 declarations in 1 file

this file: is_derive_mehler, is_derive_mehler_r

let measurable_mk1 section-local source, line 679

Let measurable_mk1 r x : measurable_fun [set: R] (mk1 r x).

Used by 2 declarations in 1 file

this file: mehler_d1E, is_derive_mehler_d1

let measurable_mk2 section-local source, line 685

Let measurable_mk2 r x : measurable_fun [set: R] (mk2 r x).

Used by 2 declarations in 1 file

this file: mehler_d2E, is_derive_mehler_d2

let measurable_mk3 section-local source, line 691

Let measurable_mk3 r x : measurable_fun [set: R] (mk3 r x).

Used by 1 declaration in 1 file

this file: mehler_d3E

let measurable_mkr section-local source, line 699

Let measurable_mkr r x : measurable_fun [set: R] (mkr r x).

Used by 1 declaration in 1 file

this file: mehler_drE

let normz_le1 section-local source, line 708

Let normz_le1 (z : R) : `|z| <= 1 + `|z| ^+ 2.

Used by 2 declarations in 1 file

this file: mehler_d3E, mehler_drE

let mehler_d1E section-local source, line 711

Let mehler_d1E f r x (K : R) : `|r| < 1 -> measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) ->
  mehler_d1 r f x = \int[N]_y (f y * (mehler_kernel r x y * mk1 r x y)).

Used by 2 declarations in 1 file

this file: is_derive_mehler, is_derive_mehler_d1

let mehler_d2E section-local source, line 733

Let mehler_d2E f r x (K : R) : `|r| < 1 -> measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) ->
  mehler_d2 r f x = \int[N]_y (f y * (mehler_kernel r x y * mk2 r x y)).

Used by 2 declarations in 1 file

this file: is_derive_mehler_d1, is_derive_mehler_d2

let mehler_d3E section-local source, line 760

Let mehler_d3E f r x (K : R) : `|r| < 1 -> measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) ->
  mehler_d3 r f x = \int[N]_y (f y * (mehler_kernel r x y * mk3 r x y)).

Used by 1 declaration in 1 file

this file: is_derive_mehler_d2

let mehler_drE section-local source, line 791

Let mehler_drE f r x (K : R) : `|r| < 1 -> measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) ->
  mehler_dr r f x = \int[N]_y (f y * (mehler_kernel r x y * mkr r x y)).

Used by 1 declaration in 1 file

this file: is_derive_mehler_r

let x_near section-local source, line 817

Let x_near (x x' : R) : x' \in `]x - 1, x + 1[ -> `|x'| <= `|x| + 1.

Used by 3 declarations in 1 file

this file: is_derive_mehler, is_derive_mehler_d1, is_derive_mehler_d2

let x_in section-local source, line 824

Let x_in (x : R) : x \in `]x - 1, x + 1[.

Used by 3 declarations in 1 file

this file: is_derive_mehler, is_derive_mehler_d1, is_derive_mehler_d2

theorem is_derive_mehler main result source, line 827

forall {R : realType} [f : R -> R] [r : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) -> `|r| < 1 -> is_derive x 1 (mehler r f) (mehler_d1 r f x)

Main result, as the README states it

For f bounded and measurable and |r| < 1, mehler r f has derivatives of order 1, 2 and 3 in x and a derivative in r, given by integrals against Hermite polynomials (mehler_d1, mehler_d2, mehler_d3, mehler_dr): for instance (mehler r f)' x = r / b E[f (r x + b Z) Z] with b = sqrt (1 - r^2). Generator identity: r d/dr mehler r f = x (mehler r f)' - (mehler r f)''.

Statement as written in the source

Theorem is_derive_mehler f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 ->
  is_derive x 1 (mehler r f) (mehler_d1 r f x).

Used by 3 declarations in 2 files

this file: continuous_mehler, is_derive_ou
GaussianAnalysis.comparison.brascamp_lieb: is_derive_g

theorem is_derive_mehler_d1 main result source, line 854

forall {R : realType} [f : R -> R] [r : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) -> `|r| < 1 -> is_derive x 1 (mehler_d1 r f) (mehler_d2 r f x)

Main result

Stated in the README together with is_derive_mehler.

Statement as written in the source

Theorem is_derive_mehler_d1 f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 ->
  is_derive x 1 (mehler_d1 r f) (mehler_d2 r f x).

Used by 3 declarations in 2 files

this file: continuous_mehler_d1, is_derive_ou_d1
GaussianAnalysis.comparison.brascamp_lieb: is_derive_g1

theorem is_derive_mehler_d2 main result source, line 881

forall {R : realType} [f : R -> R] [r : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) -> `|r| < 1 -> is_derive x 1 (mehler_d2 r f) (mehler_d3 r f x)

Main result

Stated in the README together with is_derive_mehler.

Statement as written in the source

Theorem is_derive_mehler_d2 f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 ->
  is_derive x 1 (mehler_d2 r f) (mehler_d3 r f x).

Used by 1 declaration in 1 file

this file: continuous_mehler_d2

theorem is_derive_mehler_r main result source, line 907

forall {R : realType} [f : R -> R] [r : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
`|r| < 1 -> is_derive r 1 (fun r0 : R => mehler r0 f x) (mehler_dr r f x)

Main result

Stated in the README together with is_derive_mehler.

Statement as written in the source

Theorem is_derive_mehler_r f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 ->
  is_derive r 1 (fun r => mehler r f x) (mehler_dr r f x).

Used by 3 declarations in 2 files

this file: is_derive_ou_t, ou_cvgy
GaussianAnalysis.comparison.brascamp_lieb: is_derive_G

theorem mehler_generator main result source, line 949

forall {R : realType} [f : R -> R] [r : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
`|r| < 1 -> r * mehler_dr r f x = x * mehler_d1 r f x - mehler_d2 r f x

The generator identity, in the variable r = expR (- t).

Main result

Stated in the README together with is_derive_mehler.

Statement as written in the source

Theorem mehler_generator f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 ->
  r * mehler_dr r f x = x * mehler_d1 r f x - mehler_d2 r f x.

Used by 2 declarations in 2 files

this file: is_derive_ou_t
GaussianAnalysis.comparison.brascamp_lieb: rdG

sectionmehler_properties

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Implicit Types (r x y : R) (f : R -> R).

let maff section-local source, line 994

Let maff r x : measurable_fun [set: R] (fun z => r * x + Num.sqrt (1 - r ^+ 2)
  * z).

Used by 2 declarations in 1 file

this file: mehler_d1_le, mehler_d2_le

lemma continuous_mehler main result source, line 998

forall {R : realType} [f : R -> R] [r K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) -> `|r| < 1 -> continuous (mehler r f)

Main result

Stated in the README together with mehler_d1_le.

Statement as written in the source

Lemma continuous_mehler f r (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 -> continuous (mehler r f).

Used by 1 declaration in 1 file

this file: measurable_mehler

lemma continuous_mehler_d1 main result source, line 1005

forall {R : realType} [f : R -> R] [r K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) -> `|r| < 1 -> continuous (mehler_d1 r f)

Main result

Stated in the README together with mehler_d1_le.

Statement as written in the source

Lemma continuous_mehler_d1 f r (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 -> continuous (mehler_d1 r f).

lemma continuous_mehler_d2 main result source, line 1012

forall {R : realType} [f : R -> R] [r K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) -> `|r| < 1 -> continuous (mehler_d2 r f)

Main result

Stated in the README together with mehler_d1_le.

Statement as written in the source

Lemma continuous_mehler_d2 f r (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 -> continuous (mehler_d2 r f).

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.brascamp_lieb: cg2

lemma measurable_mehler main result source, line 1019

forall {R : realType} [f : R -> R] [r K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) -> `|r| < 1 -> measurable_fun [set: R] (mehler r f)

Main result

Stated in the README together with mehler_d1_le.

Statement as written in the source

Lemma measurable_mehler f r (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 -> measurable_fun [set: R] (mehler r f).

Used by 4 declarations in 2 files

this file: mehler_contraction, mehler_L1_le
GaussianAnalysis.comparison.brascamp_lieb: measurable_G, Lambda_lip

lemma normr_Rintegral_normal_mul_le source, line 1024

forall {R : realType} [F h : R -> R] [K : R],
measurable_fun [set: R] F ->
(forall z : R, `|F z| <= K) ->
measurable_fun [set: R] h ->
(normal_prob 0 1).-integrable [set: R] (EFin \o h) ->
`|\int[normal_prob 0 1]_z (F z * h z)| <= K * \int[normal_prob 0 1]_z `|h z|

Statement as written in the source

Lemma normr_Rintegral_normal_mul_le (F h : R -> R) (K : R) :
  measurable_fun [set: R] F -> (forall z, `|F z| <= K) ->
  measurable_fun [set: R] h -> N.-integrable [set: R] (EFin \o h) ->
  `|\int[N]_z (F z * h z)| <= K * \int[N]_z `|h z|.

Used by 3 declarations in 1 file

this file: mehler_d1_le, mehler_d2_le, mehler_dr_le

lemma mehler_d1_le main result source, line 1054

forall {R : realType} [f : R -> R] [r : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
`|r| < 1 ->
`|mehler_d1 r f x| <=
`|r| / Num.ExtraDef.sqrtr (1 - r ^+ 2) * (K * \int[normal_prob 0 1]_z `|z|)

Main result, as the README states it

For |f| <= K and |r| < 1: |(mehler r f)'| <= |r| / b K E|Z|, |(mehler r f)''| <= r^2 / b^2 K E|Z^2 - 1|, |d/dr mehler r f x| <= |x| / b K E|Z| + |r| / b^2 K E|Z^2 - 1|; mehler r f and its first two derivatives are continuous.

Statement as written in the source

Lemma mehler_d1_le f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 ->
  `|mehler_d1 r f x| <= `|r| / Num.sqrt (1 - r ^+ 2) * (K * \int[N]_z `|z|).

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.brascamp_lieb: a_le

lemma mehler_d2_le main result source, line 1068

forall {R : realType} [f : R -> R] [r : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
`|r| < 1 ->
`|mehler_d2 r f x| <= r ^+ 2 / (1 - r ^+ 2) * (K * \int[normal_prob 0 1]_z `|z ^+ 2 - 1|)

Main result

Stated in the README together with mehler_d1_le.

Statement as written in the source

Lemma mehler_d2_le f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 ->
  `|mehler_d2 r f x| <= r ^+ 2 / (1 - r ^+ 2) * (K * \int[N]_z `|z ^+ 2 - 1|).

Used by 2 declarations in 1 file

GaussianAnalysis.comparison.brascamp_lieb: a'_le, dLambda_le0

sectionmehler_semigroup

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Implicit Types (r x y : R) (f : R -> R).

let maff section-local source, line 1091

Let maff r x : measurable_fun [set: R] (fun z => r * x + Num.sqrt (1 - r ^+ 2)
  * z).

Used by 1 declaration in 1 file

this file: integrable_maff

let integrable_maff section-local source, line 1095

Let integrable_maff f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) ->
  N.-integrable [set: R] (EFin \o (fun z => f (r * x + Num.sqrt (1 - r ^+ 2) *
    z))).

Used by 2 declarations in 1 file

this file: integral_mehler, mehler_contraction

theorem integral_mehler main result source, line 1106

forall {R : realType} [f : R -> R] [r K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
`|r| < 1 -> \int[normal_prob 0 1]_x mehler r f x = \int[normal_prob 0 1]_y f y

The standard normal law is invariant: integrating mehler r f against it is integrating f.

Main result

Stated in the README together with mehler_le.

Statement as written in the source

Theorem integral_mehler f r (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 ->
  \int[N]_x mehler r f x = \int[N]_y f y.

Used by 1 declaration in 1 file

this file: mehler_contraction

theorem mehler_contraction main result source, line 1133

forall {R : realType} [f h : R -> R] [r K : R],
measurable_fun [set: R] f ->
measurable_fun [set: R] h ->
(forall y : R, `|f y| <= K) ->
(forall y : R, `|h y| <= K) ->
`|r| < 1 ->
\int[normal_prob 0 1]_x `|mehler r f x - mehler r h x| <=
\int[normal_prob 0 1]_y `|f y - h y|

Main result

Stated in the README together with mehler_le.

Statement as written in the source

Theorem mehler_contraction f (h : R -> R) r (K : R) :
  measurable_fun [set: R] f -> measurable_fun [set: R] h ->
  (forall y, `|f y| <= K) -> (forall y, `|h y| <= K) -> `|r| < 1 ->
  \int[N]_x `|mehler r f x - mehler r h x| <= \int[N]_y `|f y - h y|.

Used by 1 declaration in 1 file

this file: mehler_L1_le

sectionnormal_continuous_dense

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

let clip section-local source, line 1170

Let clip (lo hi a : R) := Num.min hi (Num.max lo a).

Used by 3 declarations in 1 file

this file: clip_le, clip_in, normal_continuous_approx

let clip_le section-local source, line 1172

Let clip_le (lo hi a b : R) : lo <= hi -> lo <= b <= hi ->
  `|b - clip lo hi a| <= `|b - a|.

Used by 1 declaration in 1 file

this file: normal_continuous_approx

let clip_in section-local source, line 1184

Let clip_in (lo hi a : R) : lo <= hi -> lo <= clip lo hi a <= hi.

Used by 1 declaration in 1 file

this file: normal_continuous_approx

let normal_pdf01_le1 section-local source, line 1191

Let normal_pdf01_le1 (y : R) : normal_pdf 0 1 y <= 1.

Used by 1 declaration in 1 file

this file: normal_continuous_approx

theorem normal_continuous_approx main result source, line 1204

forall {R : realType} [f : R -> R] [lo hi eps : R],
measurable_fun [set: R] f ->
(forall y : R, lo <= f y <= hi) ->
0 < eps ->
exists h : R -> R,
  [/\ continuous h, forall y : R, lo <= h y <= hi
    & \int[normal_prob 0 1]_y `|f y - h y| < eps]

Bounded continuous functions are dense in L^1 of the standard normal law, within the same bounds.

Main result, as the README states it

Bounded continuous functions are dense in L^1 of the standard normal law: a measurable f with values in [lo, hi] is within eps of a continuous h with values in [lo, hi].

Statement as written in the source

Theorem normal_continuous_approx (f : R -> R) (lo hi eps : R) :
  measurable_fun [set: R] f -> (forall y, lo <= f y <= hi) -> 0 < eps ->
  exists h : R -> R, [/\ continuous h, (forall y, lo <= h y <= hi) &
    \int[N]_y `|f y - h y| < eps].

Used by 1 declaration in 1 file

this file: mehler_L1_near

sectionou_semigroup

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Implicit Types (r x y t : R) (f : R -> R).

lemma mehler_dr_split source, line 1356

forall {R : realType} [f : R -> R] [r : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
`|r| < 1 ->
mehler_dr r f x =
x / Num.ExtraDef.sqrtr (1 - r ^+ 2) *
\int[normal_prob 0 1]_z (f (r * x + Num.ExtraDef.sqrtr (1 - r ^+ 2) * z) * z) -
r / (1 - r ^+ 2) *
\int[normal_prob 0 1]_z (f (r * x + Num.ExtraDef.sqrtr (1 - r ^+ 2) * z) * (z ^+ 2 - 1))

Statement as written in the source

Lemma mehler_dr_split f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 ->
  mehler_dr r f x =
  x / Num.sqrt (1 - r ^+ 2) *
    \int[N]_z (f (r * x + Num.sqrt (1 - r ^+ 2) * z) * z) -
  r / (1 - r ^+ 2) *
    \int[N]_z (f (r * x + Num.sqrt (1 - r ^+ 2) * z) * (z ^+ 2 - 1)).

Used by 1 declaration in 1 file

this file: mehler_dr_le

lemma mehler_dr_le main result source, line 1396

forall {R : realType} [f : R -> R] [r : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
`|r| < 1 ->
`|mehler_dr r f x| <=
`|x| / Num.ExtraDef.sqrtr (1 - r ^+ 2) * (K * \int[normal_prob 0 1]_z `|z|) +
`|r| / (1 - r ^+ 2) * (K * \int[normal_prob 0 1]_z `|z ^+ 2 - 1|)

Main result

Stated in the README together with mehler_d1_le.

Statement as written in the source

Lemma mehler_dr_le f r x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> `|r| < 1 ->
  `|mehler_dr r f x| <= `|x| / Num.sqrt (1 - r ^+ 2) * (K * \int[N]_z `|z|) +
    `|r| / (1 - r ^+ 2) * (K * \int[N]_z `|z ^+ 2 - 1|).

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.brascamp_lieb: is_derive_Lambda

lemma expRN_lt1 source, line 1422

forall {R : realType} [t : R], 0 < t -> `|expR (- t)| < 1

Statement as written in the source

Lemma expRN_lt1 t : 0 < t -> `|expR (- t)| < 1.

Used by 3 declarations in 1 file

this file: is_derive_ou, is_derive_ou_d1, is_derive_ou_t

theorem is_derive_ou main result source, line 1425

forall {R : realType} [f : R -> R] [t : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) -> 0 < t -> is_derive x 1 (ou t f) (mehler_d1 (expR (- t)) f x)

Main result, as the README states it

For t > 0, the first two derivatives of ou t f in x, and d/dt ou t f x = (ou t f)'' x - x (ou t f)' x.

Statement as written in the source

Theorem is_derive_ou f t x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> 0 < t ->
  is_derive x 1 (ou t f) (mehler_d1 (expR (- t)) f x).

theorem is_derive_ou_d1 main result source, line 1430

forall {R : realType} [f : R -> R] [t : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
0 < t -> is_derive x 1 (mehler_d1 (expR (- t)) f) (mehler_d2 (expR (- t)) f x)

Main result

Stated in the README together with is_derive_ou.

Statement as written in the source

Theorem is_derive_ou_d1 f t x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> 0 < t ->
  is_derive x 1 (mehler_d1 (expR (- t)) f) (mehler_d2 (expR (- t)) f x).

theorem is_derive_ou_t main result source, line 1436

forall {R : realType} [f : R -> R] [t : R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
0 < t ->
is_derive t 1 (fun t0 : R => ou t0 f x)
  (mehler_d2 (expR (- t)) f x - x * mehler_d1 (expR (- t)) f x)

The generator identity: d/dt ou t f = (ou t f)'' - x (ou t f)'.

Main result

Stated in the README together with is_derive_ou.

Statement as written in the source

Theorem is_derive_ou_t f t x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> 0 < t ->
  is_derive t 1 (fun t => ou t f x)
    (mehler_d2 (expR (- t)) f x - x * mehler_d1 (expR (- t)) f x).

theorem ou_cvgy main result source, line 1452

forall {R : realType} [f : R -> R] (x : R) [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) -> ou t f x @[t --> +oo] --> \int[normal_prob 0 1]_y f y

Main result, as the README states it

As t -> +oo, ou t f x tends to the mean of f. As t -> 0 from the right (r -> 1), ou t f x tends to f x for f continuous and bounded, and ou t f tends to f in L^1 of the standard normal law for every bounded measurable f.

Statement as written in the source

Theorem ou_cvgy f x (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> ou t f x @[t --> +oo] --> \int[N]_y f y.

sectionmehler_limits

Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Implicit Types (r x y t : R) (f h : R -> R).

let integrable_cst section-local source, line 1471

Let integrable_cst (K : R) : N.-integrable [set: R] (EFin \o (fun=> K)).

lemma continuous_mehler_x main result source, line 1476

forall {R : realType} [h : R -> R] [r K : R],
continuous h -> (forall y : R, `|h y| <= K) -> continuous (mehler r h)

For h continuous and bounded, mehler r h x is continuous in x and in r, for every r.

Main result

Stated in the README together with ou_cvgy.

Statement as written in the source

Lemma continuous_mehler_x h r (K : R) : continuous h -> (forall y, `|h y| <= K)
  ->
  continuous (mehler r h).

Used by 1 declaration in 1 file

this file: mehler_L1_near

lemma continuous_mehler_r main result source, line 1493

forall {R : realType} [h : R -> R] [x K : R],
continuous h -> (forall y : R, `|h y| <= K) -> continuous (fun r : R => mehler r h x)

Main result

Stated in the README together with ou_cvgy.

Statement as written in the source

Lemma continuous_mehler_r h x (K : R) : continuous h -> (forall y, `|h y| <= K)
  ->
  continuous (fun r => mehler r h x).

Used by 3 declarations in 1 file

this file: mehler_cvg1, continuous_mehler_r_abs, ou_cvg0

theorem mehler_cvg1 main result source, line 1512

forall {R : realType} [h : R -> R] [x K : R],
continuous h -> (forall y : R, `|h y| <= K) -> mehler r h x @[r --> 1 : R] --> h x

Main result

Stated in the README together with ou_cvgy.

Statement as written in the source

Theorem mehler_cvg1 h x (K : R) : continuous h -> (forall y, `|h y| <= K) ->
  mehler r h x @[r --> (1 : R)] --> h x.

let integrable_abs_bounded section-local source, line 1519

Let integrable_abs_bounded (F : R -> R) (C : R) :
  measurable_fun [set: R] F -> (forall y, `|F y| <= C) ->
  N.-integrable [set: R] (EFin \o (fun y => `|F y|)).

Used by 2 declarations in 1 file

this file: mehler_L1_le, mehler_L1_near

let mehler_L1_le section-local source, line 1528

Let mehler_L1_le f h r (K : R) :
  measurable_fun [set: R] f -> measurable_fun [set: R] h ->
  (forall y, `|f y| <= K) -> (forall y, `|h y| <= K) -> `|r| < 1 ->
  \int[N]_x `|mehler r f x - f x| <=
  \int[N]_y `|f y - h y| + \int[N]_x `|mehler r h x - h x| +
  \int[N]_y `|h y - f y|.

Used by 1 declaration in 1 file

this file: mehler_L1_near

let continuous_mehler_r_abs section-local source, line 1564

Let continuous_mehler_r_abs h (x K : R) : continuous h -> (forall y, `|h y| <=
  K) ->
  continuous (fun r => `|mehler r h x - h x|).

Used by 1 declaration in 1 file

this file: mehler_L1_near

let sum3_lt section-local source, line 1572

Let sum3_lt (a b c e : R) : a < e / 3 -> b < e / 3 -> c < e / 3 -> a + b + c <=
  e.

Used by 1 declaration in 1 file

this file: mehler_L1_near

let mehler_L1_near section-local source, line 1576

Let mehler_L1_near f (K eps : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) -> 0 < eps ->
  \forall r \near (1 : R), `|r| < 1 -> \int[N]_x `|mehler r f x - f x| <= eps.

Used by 1 declaration in 1 file

this file: mehler_cvg_L1

theorem mehler_cvg_L1 main result source, line 1614

forall {R : realType} [f : R -> R] [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
\int[normal_prob 0 1]_x `|mehler r f x - f x| @[r --> (1 : R)^'-] --> 0

For f bounded and measurable, mehler r f tends to f in L^1 of the standard normal law as r tends to 1 from the left.

Main result

Stated in the README together with ou_cvgy.

Statement as written in the source

Theorem mehler_cvg_L1 f (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) ->
  \int[N]_x `|mehler r f x - f x| @[r --> (1 : R)^'-] --> 0.

Used by 2 declarations in 2 files

this file: ou_cvg0_L1
GaussianAnalysis.comparison.brascamp_lieb: Lambda_cvg1

theorem ou_cvg0_L1 main result source, line 1630

forall {R : realType} [f : R -> R] [K : R],
measurable_fun [set: R] f ->
(forall y : R, `|f y| <= K) ->
\int[normal_prob 0 1]_x `|ou t f x - f x| @[t --> (0 : R)^'+] --> 0

Main result

Stated in the README together with ou_cvgy.

Statement as written in the source

Theorem ou_cvg0_L1 f (K : R) : measurable_fun [set: R] f ->
  (forall y, `|f y| <= K) ->
  \int[N]_x `|ou t f x - f x| @[t --> (0 : R)^'+] --> 0.

theorem ou_cvg0 main result source, line 1643

forall {R : realType} [h : R -> R] [x K : R],
continuous h -> (forall y : R, `|h y| <= K) -> ou t h x @[t --> (0 : R)^'+] --> h x

Main result

Stated in the README together with ou_cvgy.

Statement as written in the source

Theorem ou_cvg0 h x (K : R) : continuous h -> (forall y, `|h y| <= K) ->
  ou t h x @[t --> (0 : R)^'+] --> h x.

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.