On this page
The Brascamp-Lieb inequality: from bounded functions to [0, +oo]
Imports 8 library modules and 30 external
- GaussianAnalysis.gaussian.measurable_matrix
- GaussianAnalysis.gaussian.normal_integral
- GaussianAnalysis.gaussian.gauss
- GaussianAnalysis.gaussian.lebesgue_rV
- GaussianAnalysis.matrix.euclidean
- GaussianAnalysis.probability.lindeberg
- GaussianAnalysis.comparison.gauss_linear
- GaussianAnalysis.comparison.brascamp_lieb
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.archimedean, 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.trigo, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.probability_theory.normal_distribution
Imported by 1
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. The Gaussian form of the Brascamp-Lieb inequality for measurable f_i with values in [delta, K], 0 < delta,
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},
is gauss_brascamp_lieb_bounded of brascamp_lieb.v. This file derives:
- the same for measurable f_i with values in [0, K] (gauss_brascamp_lieb_ge0): apply it to f_i + 1/(k+1), and let k -> oo; the right side converges since a^c is continuous on [0, +oo) for c > 0;
- the same for measurable F_i : R -> [0, +oo] (gauss_brascamp_lieb), with extended integrals and poweR: apply the previous case to the truncations min (F_i, k), monotone convergence on the left, and monotonicity on the right; the product of the truncated factors converges to the product of the limits, with 0 * +oo = 0;
- the Lebesgue form (brascamp_lieb)
int_{R^m} prod_i F_i(<x, u_i>)^{c_i} dx <= prod_i (int_R F_i)^{c_i},
from the Gaussian form for f_i(t) = F_i(t) sqrt (2 pi) exp (t^2 / 2): the integral of f_i against the standard normal law is the Lebesgue integral of F_i, and since sum_i c_i <x, u_i>^2 = |x|^2 and sum_i c_i = m (tight_frame_mxdot_sqr, tight_frame_sum), prod_i (sqrt (2 pi) exp (<x, u_i>^2 / 2))^{c_i} = (2 pi)^{m/2} exp (|x|^2 / 2) is the inverse of the density gauss_pdf of gauss m with respect to lebesgue_rV m.
Main results
| Results | Statement |
|---|---|
The Brascamp-Lieb inequality in Lebesgue form (Ball's geometric form): 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 : R -> [0, +oo], \int prod_i F_i(<x, u_i>)^(c_i) dx <= prod_i (\int F_i)^(c_i) (lebesgue_rV m on the left, poweR powers). Proved from gauss_brascamp_lieb applied to F_i(t) sqrt (2 pi) exp (t^2 / 2), with the density gauss_pdf of gauss m. | |
The Gaussian form for measurable F_i : R -> [0, +oo]: \int prod_i F_i(<x, u_i>)^(c_i) dgauss_m <= prod_i (\int F_i dnormal_prob 0 1)^(c_i), in extended reals with poweR. From gauss_brascamp_lieb_ge0 applied to the truncations min (F_i, k): monotone convergence on the left (the product of the nondecreasing truncated factors converges to the product of the limits, with 0 * +oo = 0), monotonicity on the right. | |
The Gaussian form for measurable f_i with values in [0, K] (real integrals and powR), from gauss_brascamp_lieb_bounded (values in [delta, K], delta > 0) applied to f_i + 1/(k+1), as k -> oo. |
Declarations3 exported, 7 local
Context {R : realType}. Local Notation N := (@normal_prob R 0 1).
Let powR_sum (x : R) I (r : seq I) (P : pred I) (a : I -> R) : 0 < x -> x `^ (\sum_(i <- r | P i) a i) = \prod_(i <- r | P i) x `^ a i.
Used by 1 declaration in 1 file
- this file: brascamp_lieb
Let emeasurable_prod d (T : measurableType d) I (r : seq I) (h : I -> T -> \bar R) : (forall i, measurable_fun [set: T] (h i)) -> measurable_fun [set: T] (fun x => \prod_(i <- r) h i x)%E.
Used by 2 declarations in 1 file
- this file: gauss_brascamp_lieb, brascamp_lieb
Let lee_prod I (r : seq I) (P : pred I) (f g : I -> \bar R) : (forall i, P i -> 0 <= f i)%E -> (forall i, P i -> f i <= g i)%E -> (\prod_(i <- r | P i) f i <= \prod_(i <- r | P i) g i)%E.
Used by 2 declarations in 1 file
- this file: cvg_prod_nd, gauss_brascamp_lieb
Let cvg_powR_harmonic (a c : R) : 0 <= a -> 0 < c -> (a + harmonic k) `^ c @[k --> \oo] --> a `^ c.
(a + 1 / (k + 1))^c tends to a^c.
Used by 1 declaration in 1 file
- this file: gauss_brascamp_lieb_ge0
Let nd_le_lim (v : nat -> \bar R) (l : \bar R) : nondecreasing_seq v -> v @ \oo --> l -> forall k, (v k <= l)%E.
A nondecreasing sequence lies below its limit.
Used by 1 declaration in 1 file
- this file: cvg_prod_nd
Let cvg_prod_nd (I : Type) (r : seq I) (v : I -> nat -> \bar R) (l : I -> \bar R) : (forall i k, (0 <= v i k)%E) -> (forall i, nondecreasing_seq (v i)) -> (forall i, v i @ \oo --> l i) -> (fun k => \prod_(i <- r) v i k)%E @ \oo --> (\prod_(i <- r) l i)%E.
The product of finitely many nondecreasing nonnegative sequences tends to the product of the limits, with the convention 0 * +oo = 0.
Used by 1 declaration in 1 file
- this file: gauss_brascamp_lieb
Let cvg_poweR_mine (a : \bar R) (c : R) : (0 <= a)%E -> 0 < c -> ((mine a k%:R%:E) `^ c)%E @[k --> \oo] --> (a `^ c)%E.
min (a, k)^c tends to a^c for a in [0, +oo].
Used by 1 declaration in 1 file
- this file: gauss_brascamp_lieb
forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R] [f : 'I_n -> R -> R] [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 -> (forall i : 'I_n, measurable_fun [set: R] (f i)) -> (forall (i : 'I_n) (y : R), 0 <= 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
The Gaussian form for bounded nonnegative functions, from the bounded case applied to f + 1 / (k + 1).
The Gaussian form for measurable f_i with values in [0, K] (real integrals and powR), from gauss_brascamp_lieb_bounded (values in [delta, K], delta > 0) applied to f_i + 1/(k+1), as k -> oo.
Statement as written in the source
Lemma gauss_brascamp_lieb_ge0 m n (u : 'I_n -> 'rV[R]_m) (c : 'I_n -> R) (f : 'I_n -> R -> R) (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 -> (forall i, measurable_fun [set: R] (f i)) -> (forall i y, 0 <= f i y <= K) -> \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
forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R] [F : 'I_n -> R -> \bar 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 i : 'I_n, measurable_fun [set: R] (F i)) -> (forall (i : 'I_n) (t : R), (0%R <= F i t)%E) -> (\int[gauss m]_x \prod_i F i (mxdot x (u i)) `^ c i <= \prod_i (\int[normal_prob 0 1]_t F i t) `^ c i)%E
The Gaussian form of the Brascamp-Lieb inequality for measurable F_i : R -> [0, +oo], from the bounded case by monotone convergence along the truncations min (F_i, k).
The Gaussian form for measurable F_i : R -> [0, +oo]: \int prod_i F_i(<x, u_i>)^(c_i) dgauss_m <= prod_i (\int F_i dnormal_prob 0 1)^(c_i), in extended reals with poweR. From gauss_brascamp_lieb_ge0 applied to the truncations min (F_i, k): monotone convergence on the left (the product of the nondecreasing truncated factors converges to the product of the limits, with 0 * +oo = 0), monotonicity on the right.
Statement as written in the source
Theorem gauss_brascamp_lieb m n (u : 'I_n -> 'rV[R]_m) (c : 'I_n -> R) (F : 'I_n -> R -> \bar 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 -> (forall i, measurable_fun [set: R] (F i)) -> (forall i t, 0 <= F i t)%E -> (\int[gauss m]_x \prod_i F i (mxdot x (u i)) `^ c i <= \prod_i (\int[normal_prob 0 1]_t F i t) `^ c i)%E.
Used by 1 declaration in 1 file
- this file: brascamp_lieb
forall {R : realType} [m n : nat] [u : 'I_n -> 'rV_m] [c : 'I_n -> R] [F : 'I_n -> R -> \bar 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 i : 'I_n, measurable_fun [set: R] (F i)) -> (forall (i : 'I_n) (t : R), (0%R <= F i t)%E) -> (\int[lebesgue_rV m]_x \prod_i F i (mxdot x (u i)) `^ c i <= \prod_i (\int[lebesgue_measure]_t F i t) `^ c i)%E
The Brascamp-Lieb inequality in Lebesgue form (Ball's geometric form): 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 : R -> [0, +oo], \int prod_i F_i(<x, u_i>)^(c_i) dx <= prod_i (\int F_i)^(c_i) (lebesgue_rV m on the left, poweR powers). Proved from gauss_brascamp_lieb applied to F_i(t) sqrt (2 pi) exp (t^2 / 2), with the density gauss_pdf of gauss m.
Statement as written in the source
Theorem brascamp_lieb m n (u : 'I_n -> 'rV[R]_m) (c : 'I_n -> R) (F : 'I_n -> R -> \bar 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 -> (forall i, measurable_fun [set: R] (F i)) -> (forall i t, 0 <= F i t)%E -> (\int[lebesgue_rV m]_x \prod_i F i (mxdot x (u i)) `^ c i <= \prod_i (\int[lebesgue_measure]_t F i t) `^ c i)%E.
Used by 1 declaration in 1 file
- GaussianAnalysis.fourier.small_ball: brascamp_lieb_ge0