On this page

The Gaussian Brascamp-Lieb inequality for bounded functions

GaussianAnalysis.comparison.brascamp_lieblibrary/comparison/brascamp_lieb.v1,005 lines13 lemmas and theoremssource

Imports 11 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.matrix, 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

Imported by 1

GaussianAnalysis.comparison.brascamp_lieb_lebesgue

Ball's geometric form of the Brascamp-Lieb inequality, for the standard Gaussian measure and bounded functions. Let u_1, ..., u_n be unit vectors of 'rV[R]_m and c_1, ..., c_n positive weights such that sum_i c_i u_i^T u_i is the identity matrix of size m: the vectors sqrt (c_i) u_i form a tight frame. For measurable f_1, ..., f_n with values in [delta, K], 0 < delta (gauss_brascamp_lieb_bounded),

int prod_i f_i(<x, u_i>)^{c_i} dgauss_m(x)
  <= prod_i (int f_i d(normal_prob 0 1))^{c_i},

with real integrals and powR. The extension to f_i with values in [0, K] (gauss_brascamp_lieb_ge0) and to measurable F_i : R -> [0, +oo] (gauss_brascamp_lieb), and the form with Lebesgue measures (brascamp_lieb), are derived from this theorem in brascamp_lieb_lebesgue.v.

The proof uses the Mehler transform of ornstein_uhlenbeck.v. For 0 <= r <= 1 let

Lambda(r) = int G_r(x) dgauss_m(x),
G_r(x) = exp (sum_i c_i ln (mehler r f_i)(<x, u_i>)).

Since mehler 1 f = f and mehler 0 f is the mean of f, Lambda(1) is the left side and Lambda(0) the right side. For 0 < r < 1, Lambda is differentiable under the integral. The generator identity r d/dr mehler r f = x (mehler r f)' - (mehler r f)'' and Gaussian integration by parts along each u_i (gauss_ibp_unit) give

r Lambda'(r) = int (|V(x)|^2 - sum_i c_i a_i(x)^2) G_r(x) dgauss_m(x),

where a_i(x) is the derivative of ln (mehler r f_i) at <x, u_i> and V(x) = sum_i c_i a_i(x) u_i. This is nonpositive by a weighted Cauchy-Schwarz inequality for tight frames (tight_frame_cauchy_schwarz). Lambda is continuous at 1 from the left, since mehler r f_i tends to f_i in L^1 of the standard normal law (mehler_cvg_L1), and the mean value theorem gives Lambda(1) <= Lambda(0).

Main results

Results	Statement
gauss_brascamp_lieb_bounded	The Gaussian Brascamp-Lieb inequality for bounded functions: for unit vectors `u_i` of `'rV[R]_m` and weights `c_i > 0` with `sum_i c_i u_i^T u_i = 1`, and measurable `f_i` with values in `[delta, K]`, `0 < delta`, `\int prod_i f_i(<x, u_i>)^(c_i) dgauss_m <= prod_i (\int f_i dnormal_prob 0 1)^(c_i)` (real integrals, `powR`). Proof by the Ornstein-Uhlenbeck semigroup: `\int exp (sum_i c_i ln (mehler r f_i)(<x, u_i>)) dgauss_m` is nonincreasing in `r` on `[0, 1]`, equal to the left side at `r = 1` and to the right side at `r = 0`.
gauss_ibp_unit	Gaussian integration by parts along a unit vector `u`: `E[<x, u> F(x)] = E[d_u F(x)]` for `x` of law `gauss m`, `F` and its derivative `d_u F` along `u` bounded and measurable, `d_u F` continuous along the lines parallel to `u`.
tight_frame_mxdottight_frame_mxdot_sqrtight_frame_sumtight_frame_cauchy_schwarz	If `sum_i c_i u_i^T u_i = 1` for row vectors `u_i` of `'rV[R]_m`: `sum_i c_i <v, u_i> <u_i, w> = <v, w>`, so `sum_i c_i <v, u_i>^2 = \|v\|^2`; `sum_i c_i = m` when the `u_i` are unit vectors; and, for `c_i >= 0`, `\|sum_i c_i a_i u_i\|^2 <= sum_i c_i a_i^2` for all reals `a_i`.
is_derive_comp_diris_derive_mxdotis_derive_mxdot_comp	Directional derivatives: the chain rule for `phi (S x)` along a direction `v`, and the derivative `phi' (<x, w>) <v, w>` of `x \|-> phi (<x, w>)` along `v`.

Declarations13 exported, 81 local

sectiontight_frame

Context {R : realType} (m n : nat) (u : 'I_n -> 'rV[R]_m) (c : 'I_n -> R).
Hypothesis u1 : forall i, mxdot (u i) (u i) = 1.
Hypothesis frame : \sum_i c i *: ((u i)^T *m u i) = 1%:M.

let mxdot_tr_mul section-local source, line 72

Let mxdot_tr_mul (v w : 'rV[R]_m) i :
  \tr (v *m ((u i)^T *m u i) *m w^T) = mxdot v (u i) * mxdot (u i) w.

Used by 1 declaration in 1 file

this file: tight_frame_mxdot

lemma tight_frame_mxdot main result source, line 80

forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R],
\sum_i c i *: ((u i)^T *m u i) = 1%:M ->
forall v w : 'rV_m, \sum_i c i * (mxdot v (u i) * mxdot (u i) w) = mxdot v w

The frame condition, in the form sum_i c_i <v, u_i> <u_i, w> = <v, w>.

Main result, as the README states it

If sum_i c_i u_i^T u_i = 1 for row vectors u_i of 'rV[R]_m: sum_i c_i <v, u_i> <u_i, w> = <v, w>, so sum_i c_i <v, u_i>^2 = |v|^2; sum_i c_i = m when the u_i are unit vectors; and, for c_i >= 0, |sum_i c_i a_i u_i|^2 <= sum_i c_i a_i^2 for all reals a_i.

Statement as written in the source

Lemma tight_frame_mxdot (v w : 'rV[R]_m) :
  \sum_i c i * (mxdot v (u i) * mxdot (u i) w) = mxdot v w.

Used by 1 declaration in 1 file

this file: tight_frame_mxdot_sqr

lemma tight_frame_mxdot_sqr main result source, line 88

forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R],
\sum_i c i *: ((u i)^T *m u i) = 1%:M ->
forall v : 'rV_m, \sum_i c i * mxdot v (u i) ^+ 2 = mxdot v v

Main result

Stated in the README together with tight_frame_mxdot.

Statement as written in the source

Lemma tight_frame_mxdot_sqr (v : 'rV[R]_m) :
  \sum_i c i * mxdot v (u i) ^+ 2 = mxdot v v.

Used by 2 declarations in 2 files

this file: tight_frame_cauchy_schwarz
GaussianAnalysis.comparison.brascamp_lieb_lebesgue: brascamp_lieb

lemma tight_frame_sum main result source, line 96

forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R],
(forall i : 'I_n, mxdot (u i) (u i) = 1) ->
\sum_i c i *: ((u i)^T *m u i) = 1%:M -> \sum_i c i = m%:R

Taking the trace of the frame condition: sum_i c_i = m.

Main result

Stated in the README together with tight_frame_mxdot.

Statement as written in the source

Lemma tight_frame_sum : \sum_i c i = m%:R.

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.brascamp_lieb_lebesgue: brascamp_lieb

lemma tight_frame_cauchy_schwarz main result source, line 104

forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R],
\sum_i c i *: ((u i)^T *m u i) = 1%:M ->
forall a : 'I_n -> R,
(forall i : 'I_n, 0 <= c i) ->
mxdot (\sum_i (c i * a i) *: u i) (\sum_i (c i * a i) *: u i) <= \sum_i c i * a i ^+ 2

A weighted Cauchy-Schwarz inequality: for the vector V = sum_i c_i a_i u_i, |V|^2 <= sum_i c_i a_i^2.

Main result

Stated in the README together with tight_frame_mxdot.

Statement as written in the source

Lemma tight_frame_cauchy_schwarz (a : 'I_n -> R) : (forall i, 0 <= c i) ->
  mxdot (\sum_i (c i * a i) *: u i) (\sum_i (c i * a i) *: u i) <=
  \sum_i c i * a i ^+ 2.

Used by 1 declaration in 1 file

this file: key

sectiongauss_ibp_unit

Context {R : realType}.

theorem gauss_ibp_unit main result source, line 140

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

Gaussian integration by parts along a unit vector u: E[<x, u> F(x)] = E[d_u F(x)] for x of law gauss m, F and its derivative along u bounded and measurable, the derivative continuous along the lines parallel to u. The proof moves u to the first basis vector with a Householder reflection.

Main result, as the README states it

Gaussian integration by parts along a unit vector u: E[<x, u> F(x)] = E[d_u F(x)] for x of law gauss m, F and its derivative d_u F along u bounded and measurable, d_u F continuous along the lines parallel to u.

Statement as written in the source

Theorem gauss_ibp_unit m (u : 'rV[R]_m) (F dF : 'rV[R]_m -> R) (C : R) :
  mxdot u u = 1 -> (forall x, is_derive x u F (dF x)) ->
  measurable_fun [set: 'rV[R]_m] F -> measurable_fun [set: 'rV[R]_m] dF ->
  (forall x, continuous (fun t : R => dF (t *: u + x))) ->
  (forall x, `|F x| <= C) -> (forall x, `|dF x| <= C) ->
  (\int[gauss m]_x (mxdot x u * F x)%:E = \int[gauss m]_x (dF x)%:E)%E.

Used by 1 declaration in 1 file

this file: ibp

sectiondirectional

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

lemma is_derive_comp_dir main result source, line 198

forall {R : realType} {V : normedModType R} [phi : R -> R] [S : V -> R] 
  [x v : V] [dphi dS : R],
is_derive (S x) 1 phi dphi ->
is_derive x v S dS -> is_derive x v (fun y : V => phi (S y)) (dphi * dS)

The chain rule along a direction v, for a real function of a function on V.

Main result, as the README states it

Directional derivatives: the chain rule for phi (S x) along a direction v, and the derivative phi' (<x, w>) <v, w> of x |-> phi (<x, w>) along v.

Statement as written in the source

Lemma is_derive_comp_dir (phi : R -> R) (S : V -> R) (x v : V) (dphi dS : R) :
  is_derive (S x) 1 phi dphi -> is_derive x v S dS ->
  is_derive x v (fun y => phi (S y)) (dphi * dS).

Used by 2 declarations in 1 file

this file: is_derive_mxdot_comp, is_derive_G_dir

sectionmxdot_derive

Context {R : realType} (k : nat).
Implicit Types x v w : 'rV[R]_k.

lemma is_derive_mxdot main result source, line 220

forall {R : realType} [k : nat] (x v w : 'rV_k),
is_derive x v ((mxdot (n:=k))^~ w) (mxdot v w)

Main result

Stated in the README together with is_derive_comp_dir.

Statement as written in the source

Lemma is_derive_mxdot x v w : is_derive x v (fun y => mxdot y w) (mxdot v w).

Used by 1 declaration in 1 file

this file: is_derive_mxdot_comp

lemma is_derive_mxdot_comp main result source, line 230

forall {R : realType} [k : nat] [phi : R -> R] [dphi : R] [x : 'rV_k] 
  (v : 'rV_k) [w : 'rV_k],
is_derive (mxdot x w) 1 phi dphi ->
is_derive x v
  (fun y : 'rV[R]_k => phi (mxdot y w))
  (dphi * mxdot v w)

Main result

Stated in the README together with is_derive_comp_dir.

Statement as written in the source

Lemma is_derive_mxdot_comp (phi : R -> R) (dphi : R) x v w :
  is_derive (mxdot x w) 1 phi dphi ->
  is_derive x v (fun y => phi (mxdot y w)) (dphi * mxdot v w).

Used by 2 declarations in 1 file

this file: is_derive_G_dir, is_derive_F

lemma continuous_mxdot_line source, line 239

forall {R : realType} [k : nat] [phi : R -> R] [x v w : 'rV_k],
continuous phi -> continuous (fun t : R => phi (mxdot (t *: v + x) w))

Statement as written in the source

Lemma continuous_mxdot_line (phi : R -> R) x v w : continuous phi ->
  continuous (fun t : R => phi (mxdot (t *: v + x) w)).

Used by 1 declaration in 1 file

this file: cdF

lemma mxdot_unit_le1 source, line 250

forall {R : realType} [k : nat] [v w : 'rV_k],
mxdot v v = 1 -> mxdot w w = 1 -> `|mxdot v w| <= 1

Statement as written in the source

Lemma mxdot_unit_le1 (v w : 'rV[R]_k) : mxdot v v = 1 -> mxdot w w = 1 ->
  `|mxdot v w| <= 1.

Used by 1 declaration in 1 file

this file: Sd_le

lemma mxdot_le_mx_norm source, line 257

forall {R : realType} [k : nat] (x : 'rV_k) [w : 'rV_k],
mxdot w w = 1 -> `|mxdot x w| <= (1 * k)%:R * `|x|

Statement as written in the source

Lemma mxdot_le_mx_norm (x w : 'rV[R]_k) : mxdot w w = 1 ->
  `|mxdot x w| <= (1 * k)%:R * `|x|.

Used by 2 declarations in 1 file

this file: is_derive_Lambda, dLambda_le0

sectionintegrable_Rsum

Context d {T : measurableType d} {R : realType}
  (mu : {measure set T -> \bar R}).

lemma integrable_Rsum source, line 270

forall [d : measure_display] {T : measurableType d} {R : realType} 
  [mu : measure T R] [I : Type] (s : seq I) [h : I -> T -> R],
(forall i : I, mu.-integrable [set: T] (EFin \o h i)) ->
mu.-integrable [set: T] (EFin \o (fun x : T => \sum_(i <- s) h i x))

Statement as written in the source

Lemma integrable_Rsum (I : Type) (s : seq I) (h : I -> T -> R) :
  (forall i, mu.-integrable [set: T] (EFin \o h i)) ->
  mu.-integrable [set: T] (EFin \o (fun x => \sum_(i <- s) h i x)).

Used by 2 declarations in 1 file

this file: dLambda_le0, Lambda_lip

sectiongauss_brascamp_lieb_bounded

Context {R : realType} (m n : nat) (u : 'I_n -> 'rV[R]_m) (c : 'I_n -> R).
Hypothesis u1 : forall i, mxdot (u i) (u i) = 1.
Hypothesis c0 : forall i, 0 < c i.
Hypothesis frame : \sum_i c i *: ((u i)^T *m u i) = 1%:M.
Variables (f : 'I_n -> R -> R) (delta K : R).
Hypothesis delta0 : 0 < delta.
Hypothesis deltaK : delta <= K.
Hypothesis mf : forall i, measurable_fun [set: R] (f i).
Hypothesis fb : forall i y, delta <= f i y <= K.
Local Notation N := (@normal_prob R 0 1).

let K0 section-local source, line 293

Let K0 : 0 < K := lt_le_trans delta0 deltaK.

let fK section-local source, line 295

Let fK i y : `|f i y| <= K.

Used by 13 declarations in 1 file

this file: gb, measurable_G, is_derive_G, is_derive_Lambda, a_le, a'_le, is_derive_g, is_derive_g1, cg2, rdG, dLambda_le0, Lambda_lip, Lambda_cvg1

let g section-local source, line 300

Let g r i := mehler r (f i).

Used by 26 declarations in 1 file

this file: gb, g_gt0, G, measurable_G, Lambda1, Lambda0, dG, is_derive_G, is_derive_Lambda, a, a', g_ge, invg_le, is_derive_g, is_derive_a, is_derive_lng, cg, clng, is_derive_G_dir, Gg, rdG, key, dLambda_le0, G1, G_lip, Lambda_lip

let gb section-local source, line 302

Let gb r i y : delta <= g r i y <= K.

Used by 5 declarations in 1 file

this file: g_gt0, G_le, is_derive_Lambda, g_ge, G_lip

let g_gt0 section-local source, line 309

Let g_gt0 r i y : 0 < g r i y.

Used by 9 declarations in 1 file

this file: is_derive_G, is_derive_Lambda, invg_le, is_derive_a, is_derive_lng, ca', rdG, key, dLambda_le0

let G section-local source, line 313

Let G r (x : 'rV[R]_m) := expR (\sum_i c i * ln (g r i (mxdot x (u i)))).

The integrand of Lambda, prod_i (mehler r f_i)(<x, u_i>)^{c_i}.

Used by 22 declarations in 1 file

this file: G_gt0, G_le, G_norm, measurable_G, integrable_G, Lambda, Lambda1, Lambda0, dG, is_derive_G, is_derive_Lambda, F, dF, is_derive_G_dir, mG, cdF, Gg, rdG, key, G1, G_lip, Lambda_lip

let GK section-local source, line 315

Let GK := expR ((\sum_i c i) * ln K).

Used by 8 declarations in 1 file

this file: G_le, G_norm, is_derive_Lambda, CF, dLambda_le0, G_lip, Lambda_lip, Lambda_cvg1

let G_gt0 section-local source, line 317

Let G_gt0 r x : 0 < G r x := expR_gt0 _.

Used by 5 declarations in 1 file

this file: is_derive_Lambda, F_le, dF_le, key, dLambda_le0

let G_le section-local source, line 319

Let G_le r x : G r x <= GK.

Used by 1 declaration in 1 file

this file: is_derive_Lambda

let G_norm section-local source, line 326

Let G_norm r x : `|G r x| <= GK.

Used by 2 declarations in 1 file

this file: integrable_G, Lambda_lip

let measurable_G section-local source, line 329

Let measurable_G r : `|r| < 1 \/ r = 1 -> measurable_fun [set: 'rV[R]_m] (G r).

Used by 3 declarations in 1 file

this file: integrable_G, mG, Lambda_lip

let integrable_G section-local source, line 338

Let integrable_G r : `|r| < 1 \/ r = 1 ->
  (gauss m).-integrable [set: 'rV[R]_m] (EFin \o G r).

Used by 2 declarations in 1 file

this file: is_derive_Lambda, Lambda_lip

let Lambda section-local source, line 344

Let Lambda r := \int[gauss m]_x G r x.

Used by 6 declarations in 1 file

this file: Lambda1, Lambda0, is_derive_Lambda, Lambda_lip, Lambda_cvg1, Lambda_le

let Lambda1 section-local source, line 346

Let Lambda1 :
  Lambda 1 = \int[gauss m]_x expR (\sum_i c i * ln (f i (mxdot x (u i)))).

Used by 1 declaration in 1 file

this file: gauss_brascamp_lieb_bounded_sec

let Lambda0 section-local source, line 353

Let Lambda0 : Lambda 0 = expR (\sum_i c i * ln (\int[N]_y f i y)).

Used by 1 declaration in 1 file

this file: gauss_brascamp_lieb_bounded_sec

let sumc0 section-local source, line 359

Let sumc0 : 0 <= \sum_i c i := sumr_ge0 _ (fun i _ => ltW (c0 i)).

let dG section-local source, line 362

Let dG r x := G r x * \sum_i c i *
  (mehler_dr r (f i) (mxdot x (u i)) / g r i (mxdot x (u i))).

The derivative of r |-> G r x.

Used by 5 declarations in 1 file

this file: is_derive_G, is_derive_Lambda, rdG, dLambda_le0, Lambda_le

let is_derive_G section-local source, line 365

Let is_derive_G r x : `|r| < 1 -> is_derive r (1 : R) (G ^~ x) (dG r x).

Used by 1 declaration in 1 file

this file: is_derive_Lambda

let m1 section-local source, line 385

Let m1 : R := \int[N]_z `|z : R|.

Used by 3 declarations in 1 file

this file: m10, is_derive_Lambda, C1

let m2 section-local source, line 386

Let m2 : R := \int[N]_z `|(z : R) ^+ 2 - 1|.

Used by 3 declarations in 1 file

this file: m20, is_derive_Lambda, C2

let m10 section-local source, line 387

Let m10 : 0 <= m1.

Used by 1 declaration in 1 file

this file: is_derive_Lambda

let m20 section-local source, line 388

Let m20 : 0 <= m2.

Used by 1 declaration in 1 file

this file: is_derive_Lambda

let is_derive_Lambda section-local source, line 390

Let is_derive_Lambda r : `|r| < 1 ->
  is_derive r (1 : R) Lambda (\int[gauss m]_x dG r x).

Used by 1 declaration in 1 file

this file: Lambda_le

sectionderivative_sign

Variable r : R.
Hypothesis r0 : 0 < r.
Hypothesis r1 : r < 1.

let r1' section-local source, line 496

Let r1' : `|r| < 1.

Used by 9 declarations in 1 file

this file: w0, a_le, a'_le, is_derive_g, is_derive_g1, cg2, mG, rdG, dLambda_le0

let w0 section-local source, line 497

Let w0 : 0 < 1 - r ^+ 2 := onem_sqr_gt0 r1'.

let b0 section-local source, line 498

Let b0 : 0 < Num.sqrt (1 - r ^+ 2).

let g1 section-local source, line 500

Let g1 i := mehler_d1 r (f i).

Used by 5 declarations in 1 file

this file: a, is_derive_g, is_derive_g1, cg1, rdG

let g2 section-local source, line 501

Let g2 i := mehler_d2 r (f i).

Used by 6 declarations in 1 file

this file: a', is_derive_g1, cg2, Gg, rdG, dLambda_le0

let a section-local source, line 502

Let a i y := g1 i y / g r i y.

Used by 14 declarations in 1 file

this file: a', a_le, is_derive_a, is_derive_lng, ca, F, Sd, dF, is_derive_F, mF, mSd, mdF, rdG, key

let a' section-local source, line 503

Let a' i y := g2 i y / g r i y - a i y ^+ 2.

Used by 6 declarations in 1 file

this file: a'_le, is_derive_a, ca', dF, mdF, key

let C1 section-local source, line 505

Let C1 := `|r| / Num.sqrt (1 - r ^+ 2) * (K * m1).

Used by 5 declarations in 1 file

this file: C10, a_le, a'_le, Sd_le, Ca

let C2 section-local source, line 506

Let C2 := r ^+ 2 / (1 - r ^+ 2) * (K * m2).

Used by 6 declarations in 1 file

this file: C20, a'_le, CF, F_le, dF_le, dLambda_le0

let C10 section-local source, line 507

Let C10 : 0 <= C1.

let C20 section-local source, line 509

Let C20 : 0 <= C2.

let g_ge section-local source, line 514

Let g_ge i y : delta <= g r i y.

let invg_le section-local source, line 516

Let invg_le i y : `|(g r i y)^-1| <= delta^-1.

let a_le section-local source, line 523

Let a_le i y : `|a i y| <= C1 / delta.

Used by 1 declaration in 1 file

this file: F_le

let a'_le section-local source, line 529

Let a'_le i y : `|a' i y| <= C2 / delta + (C1 / delta) ^+ 2.

Used by 1 declaration in 1 file

this file: dF_le

let is_derive_g section-local source, line 537

Let is_derive_g i (y : R) : is_derive y 1 (g r i) (g1 i y) :=
  is_derive_mehler y (mf i) (fK i) r1'.

Used by 3 declarations in 1 file

this file: is_derive_a, is_derive_lng, cg

let is_derive_g1 section-local source, line 540

Let is_derive_g1 i (y : R) : is_derive y 1 (g1 i) (g2 i y) :=
  is_derive_mehler_d1 y (mf i) (fK i) r1'.

Used by 2 declarations in 1 file

this file: is_derive_a, cg1

let is_derive_a section-local source, line 543

Let is_derive_a i (y : R) : is_derive y 1 (a i) (a' i y).

Used by 2 declarations in 1 file

this file: ca, is_derive_F

let is_derive_lng section-local source, line 552

Let is_derive_lng i (y : R) : is_derive y 1 (fun y => ln (g r i y)) (a i y).

Used by 2 declarations in 1 file

this file: clng, is_derive_G_dir

let derive_cont section-local source, line 559

Let derive_cont (h dh : R -> R) : (forall y : R, is_derive y 1 h (dh y)) ->
  continuous h.

Used by 5 declarations in 1 file

this file: cg, cg1, ca, clng, cdF

let cg section-local source, line 566

Let cg i : continuous (g r i) := derive_cont (is_derive_g i).

Used by 2 declarations in 1 file

this file: ca', dLambda_le0

let cg1 section-local source, line 567

Let cg1 i : continuous (g1 i) := derive_cont (is_derive_g1 i).

let cg2 section-local source, line 568

Let cg2 i : continuous (g2 i) := continuous_mehler_d2 (mf i) (fK i) r1'.

Used by 2 declarations in 1 file

this file: ca', dLambda_le0

let ca section-local source, line 569

Let ca i : continuous (a i) := derive_cont (is_derive_a i).

Used by 5 declarations in 1 file

this file: ca', mF, mSd, mdF, cdF

let clng section-local source, line 570

Let clng i : continuous (fun y => ln (g r i y)) :=
  derive_cont (is_derive_lng i).

let ca' section-local source, line 572

Let ca' i : continuous (a' i).

Used by 2 declarations in 1 file

this file: mdF, cdF

let F section-local source, line 579

Let F i (x : 'rV[R]_m) := a i (mxdot x (u i)) * G r x.

Used by 6 declarations in 1 file

this file: is_derive_F, mF, F_le, ibp, rdG, dLambda_le0

let Sd section-local source, line 580

Let Sd i (x : 'rV[R]_m) :=
  \sum_j c j * (a j (mxdot x (u j)) * mxdot (u i) (u j)).

Used by 6 declarations in 1 file

this file: dF, is_derive_G_dir, mSd, cdF, Sd_le, key

let dF section-local source, line 582

Let dF i (x : 'rV[R]_m) :=
  (a' i (mxdot x (u i)) + a i (mxdot x (u i)) * Sd i x) * G r x.

Used by 7 declarations in 1 file

this file: is_derive_F, mdF, cdF, dF_le, ibp, key, dLambda_le0

let is_derive_G_dir section-local source, line 585

Let is_derive_G_dir i (x : 'rV[R]_m) :
  is_derive x (u i) (G r) (G r x * Sd i x).

Used by 2 declarations in 1 file

this file: is_derive_F, cdF

let is_derive_F section-local source, line 603

Let is_derive_F i (x : 'rV[R]_m) : is_derive x (u i) (F i) (dF i x).

Used by 1 declaration in 1 file

this file: ibp

let mline section-local source, line 611

Let mline (phi : R -> R) j : continuous phi ->
  measurable_fun [set: 'rV[R]_m] (fun x => phi (mxdot x (u j))).

Used by 4 declarations in 1 file

this file: mF, mSd, mdF, dLambda_le0

let mG section-local source, line 619

Let mG : measurable_fun [set: 'rV[R]_m] (G r) := measurable_G (or_introl r1').

let mF section-local source, line 621

Let mF i : measurable_fun [set: 'rV[R]_m] (F i).

Used by 1 declaration in 1 file

this file: ibp

let mSd section-local source, line 624

Let mSd i : measurable_fun [set: 'rV[R]_m] (Sd i).

let mdF section-local source, line 630

Let mdF i : measurable_fun [set: 'rV[R]_m] (dF i).

Used by 2 declarations in 1 file

this file: ibp, dLambda_le0

let cdF section-local source, line 637

Let cdF i (x : 'rV[R]_m) : continuous (fun t : R => dF i (t *: u i + x)).

Used by 1 declaration in 1 file

this file: ibp

let Sd_le section-local source, line 656

Let Sd_le i x : `|Sd i x| <= (\sum_j c j) * (C1 / delta).

let Ca section-local source, line 664

Let Ca := C1 / delta.

Used by 4 declarations in 1 file

this file: Ca0, CF, F_le, dF_le

let Ca0 section-local source, line 665

Let Ca0 : 0 <= Ca.

let CF section-local source, line 666

Let CF := (C2 / delta + Ca ^+ 2 + Ca * ((\sum_j c j) * Ca) + Ca) * GK.

Used by 3 declarations in 1 file

this file: F_le, dF_le, dLambda_le0

let F_le section-local source, line 668

Let F_le i x : `|F i x| <= CF.

Used by 2 declarations in 1 file

this file: ibp, dLambda_le0

let dF_le section-local source, line 678

Let dF_le i x : `|dF i x| <= CF.

Used by 2 declarations in 1 file

this file: ibp, dLambda_le0

let ibp section-local source, line 689

Let ibp i : \int[gauss m]_x (mxdot x (u i) * F i x) = \int[gauss m]_x dF i x.

Used by 1 declaration in 1 file

this file: dLambda_le0

let Gg section-local source, line 696

Let Gg i (x : 'rV[R]_m) :=
  G r x * (g2 i (mxdot x (u i)) / g r i (mxdot x (u i))).

Used by 3 declarations in 1 file

this file: rdG, key, dLambda_le0

let rdG section-local source, line 700

Let rdG x : r * dG r x =
  \sum_i c i * (mxdot x (u i) * F i x - Gg i x).

The generator identity, integrated against prod_j g_j^c_j.

Used by 1 declaration in 1 file

this file: dLambda_le0

let key section-local source, line 714

Let key x : \sum_i c i * (dF i x - Gg i x) <= 0.

The sign: sum_i c_i (dF_i - G g2_i / g_i) = G (|V|^2 - sum_i c_i a_i^2) <= 0 for V = sum_i c_i a_i u_i.

Used by 1 declaration in 1 file

this file: dLambda_le0

local lemma dLambda_le0 not exported source, line 732

forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R],
(forall i : 'I_n, mxdot (u i) (u i) = 1) ->
(forall i : 'I_n, 0 < c i) ->
\sum_i c i *: ((u i)^T *m u i) = 1%:M ->
forall [f : 'I_n -> R -> R] [delta K : R],
0 < delta ->
delta <= K ->
(forall i : 'I_n, measurable_fun [set: R] (f i)) ->
(forall (i : 'I_n) (y : R), delta <= f i y <= K) ->
forall [r : R],
0 < r ->
r < 1 ->
\int[gauss m]_x
   (fun (r0 : R) (x0 : 'rV_m) =>
    (fun (r1 : R) (x1 : 'rV_m) =>
     expR
       (\sum_i
           c i * ln ((fun (r2 : R) (i0 : 'I_n) => mehler r2 (f i0)) r1 i (mxdot x1 (u i)))))
      r0 x0 *
    \sum_i
       c i *
       (mehler_dr r0 (f i) (mxdot x0 (u i)) /
        (fun (r1 : R) (i0 : 'I_n) => mehler r1 (f i0)) r0 i (mxdot x0 (u i))))
     r x <=
0

Statement as written in the source

Local Lemma dLambda_le0 : \int[gauss m]_x dG r x <= 0.

Used by 1 declaration in 1 file

this file: Lambda_le

let cvg_sum0 section-local source, line 808

Let cvg_sum0 (F : set_system R) {FF : Filter F} (s : seq 'I_n)
    (h : 'I_n -> R -> R) :
  (forall i, h i x @[x --> F] --> 0) -> \sum_(i <- s) h i x @[x --> F] --> 0.

Used by 1 declaration in 1 file

this file: Lambda_cvg1

let expR_lip section-local source, line 818

Let expR_lip (A B M : R) : A <= M -> B <= M ->
  `|expR A - expR B| <= expR M * `|A - B|.

Used by 1 declaration in 1 file

this file: G_lip

let ln_lip section-local source, line 833

Let ln_lip (a b d : R) : 0 < d -> d <= a -> d <= b ->
  `|ln a - ln b| <= `|a - b| / d.

Used by 1 declaration in 1 file

this file: G_lip

let G1 section-local source, line 853

Let G1 x : G 1 x = expR (\sum_i c i * ln (f i (mxdot x (u i)))).

Used by 1 declaration in 1 file

this file: G_lip

let G_lip section-local source, line 856

Let G_lip r x : `|G r x - G 1 x| <=
  GK / delta * \sum_i c i * `|g r i (mxdot x (u i)) - f i (mxdot x (u i))|.

Used by 1 declaration in 1 file

this file: Lambda_lip

let Lambda_lip section-local source, line 876

Let Lambda_lip r : `|r| < 1 -> `|Lambda r - Lambda 1| <=
  GK / delta * \sum_i c i * \int[N]_y `|mehler r (f i) y - f i y|.

Used by 1 declaration in 1 file

this file: Lambda_cvg1

let Lambda_cvg1 section-local source, line 932

Let Lambda_cvg1 : Lambda r @[r --> (1 : R)^'-] --> Lambda 1.

Used by 1 declaration in 1 file

this file: Lambda_le

local lemma Lambda_le not exported source, line 952

forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R],
(forall i : 'I_n, mxdot (u i) (u i) = 1) ->
(forall i : 'I_n, 0 < c i) ->
\sum_i c i *: ((u i)^T *m u i) = 1%:M ->
forall [f : 'I_n -> R -> R] [delta K : R],
0 < delta ->
delta <= K ->
(forall i : 'I_n, measurable_fun [set: R] (f i)) ->
(forall (i : 'I_n) (y : R), delta <= f i y <= K) ->
(fun r : R =>
 \int[gauss m]_x
    (fun (r0 : R) (x0 : 'rV_m) =>
     expR
       (\sum_i
           c i * ln ((fun (r1 : R) (i0 : 'I_n) => mehler r1 (f i0)) r0 i (mxdot x0 (u i)))))
      r x)
  1 <=
(fun r : R =>
 \int[gauss m]_x
    (fun (r0 : R) (x0 : 'rV_m) =>
     expR
       (\sum_i
           c i * ln ((fun (r1 : R) (i0 : 'I_n) => mehler r1 (f i0)) r0 i (mxdot x0 (u i)))))
      r x)
  0

Statement as written in the source

Local Lemma Lambda_le : Lambda 1 <= Lambda 0.

Used by 1 declaration in 1 file

this file: gauss_brascamp_lieb_bounded_sec

local lemma gauss_brascamp_lieb_bounded_sec not exported source, line 973

forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R],
(forall i : 'I_n, mxdot (u i) (u i) = 1) ->
(forall i : 'I_n, 0 < c i) ->
\sum_i c i *: ((u i)^T *m u i) = 1%:M ->
forall [f : 'I_n -> R -> R] [delta K : R],
0 < delta ->
delta <= K ->
(forall i : 'I_n, measurable_fun [set: R] (f i)) ->
(forall (i : 'I_n) (y : R), delta <= f i y <= K) ->
\int[gauss m]_x \prod_i f i (mxdot x (u i)) `^ c i <=
\prod_i (\int[normal_prob 0 1]_y f i y) `^ c i

Statement as written in the source

Local Lemma gauss_brascamp_lieb_bounded_sec :
  \int[gauss m]_x (\prod_i (f i (mxdot x (u i))) `^ (c i)) <=
  \prod_i (\int[N]_y f i y) `^ (c i).

Used by 1 declaration in 1 file

this file: gauss_brascamp_lieb_bounded

theorem gauss_brascamp_lieb_bounded main result source, line 994

forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R] 
  [f : 'I_n -> R -> R] [delta K : R],
(forall i : 'I_n, mxdot (u i) (u i) = 1) ->
(forall i : 'I_n, 0 < c i) ->
\sum_i c i *: ((u i)^T *m u i) = 1%:M ->
0 < delta ->
delta <= K ->
(forall i : 'I_n, measurable_fun [set: R] (f i)) ->
(forall (i : 'I_n) (y : R), delta <= f i y <= K) ->
\int[gauss m]_x \prod_i f i (mxdot x (u i)) `^ c i <=
\prod_i (\int[normal_prob 0 1]_y f i y) `^ c i

Main result, as the README states it

The Gaussian Brascamp-Lieb inequality for bounded functions: for unit vectors u_i of 'rV[R]_m and weights c_i > 0 with sum_i c_i u_i^T u_i = 1, and measurable f_i with values in [delta, K], 0 < delta, \int prod_i f_i(<x, u_i>)^(c_i) dgauss_m <= prod_i (\int f_i dnormal_prob 0 1)^(c_i) (real integrals, powR). Proof by the Ornstein-Uhlenbeck semigroup: \int exp (sum_i c_i ln (mehler r f_i)(<x, u_i>)) dgauss_m is nonincreasing in r on [0, 1], equal to the left side at r = 1 and to the right side at r = 0.

Statement as written in the source

Theorem gauss_brascamp_lieb_bounded {R : realType} m n (u : 'I_n -> 'rV[R]_m)
    (c : 'I_n -> R) (f : 'I_n -> R -> R) (delta K : R) :
  (forall i, mxdot (u i) (u i) = 1) -> (forall i, 0 < c i) ->
  \sum_i c i *: ((u i)^T *m u i) = 1%:M -> 0 < delta -> delta <= K ->
  (forall i, measurable_fun [set: R] (f i)) ->
  (forall i y, delta <= f i y <= K) ->
  \int[gauss m]_x (\prod_i (f i (mxdot x (u i))) `^ (c i)) <=
  \prod_i (\int[normal_prob 0 1]_y f i y) `^ (c i).

Used by 1 declaration in 1 file

GaussianAnalysis.comparison.brascamp_lieb_lebesgue: gauss_brascamp_lieb_ge0

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.