One-dimensional Prékopa–Leindler inequality (lower-integral form)

Proved

ConvexOptimization.prekopa_leindler_one_dimensional

by Yifan Hong · Aug 14, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convexanalysisconvexoptimizationlog-concavitymeasure-theory

Let $0 < \lambda < 1$ , and let $f,g,h : \mathbb{R} \to [0,+\infty]$ be measurable. Assume that for every $x,y \in \mathbb{R}$ ,

f(x)^{1-\lambda}g(y)^{\lambda} \le h((1-\lambda)x+\lambda y).

Then their lower Lebesgue integrals satisfy

\left(\int f\right)^{1-\lambda}\left(\int g\right)^{\lambda} \le \int h.

This is the extended-nonnegative, lower-integral form of the one-dimensional Prékopa–Leindler inequality, allowing both function values and integrals to be $+\infty$ .

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.prekopa_leindler_one_dimensional
    (l : ℝ) (hl0 : 0 < l) (hl1 : l < 1)
    (f g h : EuclideanSpace ℝ (Fin 1) → ℝ≥0∞)
    (hf : Measurable f) (hg : Measurable g) (hh : Measurable h)
    (hple : ∀ x y : EuclideanSpace ℝ (Fin 1),
      f x ^ (1 - l) * g y ^ l ≤ h ((1 - l) • x + l • y)) :
    (∫⁻ x, f x) ^ (1 - l) * (∫⁻ x, g x) ^ l ≤ ∫⁻ x, h x := by sorry

Source

Richard J. Gardner, The Brunn-Minkowski Inequality: A Survey with Proofs, https://faculty.gardner.wwu.edu/gorizia12.pdf, Theorem 4.1 (pp. 6-8), together with the lower-integral extension described in András Prékopa, Logarithmic concave measures with applications to stochastic programming, https://rutcor.rutgers.edu/Prekopa/pdf/SCIENT2.pdf, equations (2.1)-(2.2) and the surrounding extended-integral convention.

View graph