Brunn–Minkowski and Prékopa–Leindler inequalities

TheoremPrékopa–Leindler inequality#✓fully proved

Let \(n \ge 0\) and \(0 < t < 1\), and let \(f, g, h : \mathbb{R}^n \to [0, \infty]\) be Borel measurable functions on Euclidean space \(\mathbb{R}^n\) such that \(f(x)^{1-t} g(y)^t \le h((1-t)x + ty)\) for all \(x, y \in \mathbb{R}^n\). Then, with all integrals taken over \(\mathbb{R}^n\) against Lebesgue measure,

\[\Big(\int f(x)\,dx\Big)^{1-t} \Big(\int g(x)\,dx\Big)^{t} \le \int h(x)\,dx.\]

theorem prekopa_leindler
    {n : ℕ}
    [MeasurableSpace (EuclideanSpace ℝ (Fin n))]
    [BorelSpace (EuclideanSpace ℝ (Fin n))]
    {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1)
    {f g h : EuclideanSpace ℝ (Fin n) → ENNReal}
    (hf : Measurable f) (hg : Measurable g) (hh : Measurable h)
    (hfgh : ∀ x y : EuclideanSpace ℝ (Fin n),
      ENNReal.rpow (f x) (1 - t) * ENNReal.rpow (g y) t ≤
        h ((1 - t) • x + t • y)) :
    ENNReal.rpow (∫⁻ x, f x ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) (1 - t) *
      ENNReal.rpow (∫⁻ x, g x ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) t ≤
      ∫⁻ x, h x ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))

Sources

• A. Prékopa, Acta Sci. Math. 32 (1971), 301–316; H. J. Brascamp and E. Lieb, J. Funct. Anal. 22 (1976), 366–389, DOI 10.1016/0022-1236(76)90004-5.

Used by 1

Used byBrunn–Minkowski inequality

TheoremBrunn–Minkowski inequality#✓fully proved

Let \(n \ge 1\), let \(A\) and \(B\) be nonempty compact subsets of \(\mathbb{R}^n\), let \(A + B = \{a + b : a \in A,\ b \in B\}\) be their Minkowski sum, and let \(\mathrm{vol}\) denote Lebesgue measure on \(\mathbb{R}^n\). Then

\[\mathrm{vol}(A + B)^{1/n} \ge \mathrm{vol}(A)^{1/n} + \mathrm{vol}(B)^{1/n}.\]

public theorem brunn_minkowski
    {n : ℕ} (hn : 0 < n)
    [MeasurableSpace (EuclideanSpace ℝ (Fin n))]
    [BorelSpace (EuclideanSpace ℝ (Fin n))]
    {A B : Set (EuclideanSpace ℝ (Fin n))}
    (hA : IsCompact A) (hAne : A.Nonempty)
    (hB : IsCompact B) (hBne : B.Nonempty) :
    ENNReal.rpow ((volume : Measure (EuclideanSpace ℝ (Fin n))) ((A + B)))
        ((1 : ℝ) / (n : ℝ)) ≥
      ENNReal.rpow ((volume : Measure (EuclideanSpace ℝ (Fin n))) A)
        ((1 : ℝ) / (n : ℝ)) +
      ENNReal.rpow ((volume : Measure (EuclideanSpace ℝ (Fin n))) B)
        ((1 : ℝ) / (n : ℝ))

Sources

• H. Brunn, Über Ovale und Eiflächen (1887); H. Minkowski, Geometrie der Zahlen (1896); modern formulation R. J. Gardner, Bull. AMS 39 (2002), 355–406, DOI 10.1090/S0273-0979-02-00941-2.

Uses 1

Proof usesPrékopa–Leindler inequality

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.