Prékopa's theorem: marginals of log-concave functions are log-concave

Proved

ConvexOptimization.prekopa_marginal_log_concave

by Shuze Chen · Aug 11, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convexanalysisconvexoptimizationlog-concavity

Prékopa's theorem: marginals of log-concave functions are log-concave — the goal of this mission.

Let $f : \mathbb{R}^n \times \mathbb{R}^m \to \mathbb{R}$ be measurable and log-concave, meaning $f \ge 0$ and

f(z_1)^{a} f(z_2)^{b} \le f(a z_1 + b z_2) \qquad \text{for all } z_1, z_2 \in \mathbb{R}^n\times\mathbb{R}^m,\ a, b \ge 0,\ a + b = 1,

and suppose the section $y \mapsto f(x,y)$ is integrable for every $x$ . Then the marginal

g(x) \;=\; \int_{\mathbb{R}^m} f(x,y)\, dy

is log-concave on $\mathbb{R}^n$ .

Integrating out variables therefore preserves log-concavity — a closure property with no analogue for most shape constraints, and one that fails, for instance, for quasi-concavity. Its consequences run through applied probability: the marginals and the convolution of log-concave densities are log-concave (so sums of independent log-concave random variables stay log-concave), the cumulative distribution function of a log-concave density is log-concave, and the probability that a random convex constraint is satisfied is a log-concave function of the parameters — the fact that makes chance-constrained programming tractable.

Formalization Note Log-concavity is the mission's LogConcaveOn Set.univ predicate in its zero-permitting power form; the marginal is a Bochner integral ∫ y, f (x, y), and integrability of every section is an explicit hypothesis rather than a consequence, since no decay is assumed. Source: B&V §3.5.2, pp. 106–107; Prékopa (1973), proved here via the Prékopa–Leindler inequality applied to sections.

Preamble

import Mathlib
import Definitions.Def_LogConcaveOn

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.prekopa_marginal_log_concave {n m : ℕ}
    (f : EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin m) → ℝ)
    (hf_meas : Measurable f)
    (hf_lc : LogConcaveOn Set.univ f)
    (hf_int : ∀ x : EuclideanSpace ℝ (Fin n),
      Integrable (fun y : EuclideanSpace ℝ (Fin m) => f (x, y))) :
    LogConcaveOn Set.univ
      (fun x : EuclideanSpace ℝ (Fin n) =>
        ∫ y : EuclideanSpace ℝ (Fin m), f (x, y)) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 106-107, §3.5.2 (integration of log-concave functions; Prekopa's theorem). Original source: Prekopa 1973, On logarithmic concave measures and functions, Acta Scientiarum Mathematicarum 34, pp. 335-343. Proved via the Prekopa-Leindler inequality applied to the sections of the integrand

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Theorem statement. Fix naturals $n, m$ and a function $f : \mathbb{R}^n \times \mathbb{R}^m \to \mathbb{R}$ (real-valued, total) with three hypotheses: (1) $f$ is measurable on the product space; (2) $f$ is log-concave on the whole product space in the file's sense (LogConcaveOn of the universal set), which unfolds to the conjunction: $f(x,y) \ge 0$ for every $(x,y)$ , and for all pairs $(x_1,y_1), (x_2,y_2)$ and all $a, b \ge 0$ with $a+b=1$ , $f(x_1,y_1)^a \cdot f(x_2,y_2)^b \le f\big(a x_1 + b x_2,\ a y_1 + b y_2\big)$ , with real powers ( $t^0 = 1$ including $0^0 = 1$ ; $0^r = 0$ for $r \ne 0$ ); (3) for every $x \in \mathbb{R}^n$ , the slice $y \mapsto f(x,y)$ is Bochner-integrable with respect to the volume (Lebesgue) measure on $\mathbb{R}^m$ . Conclusion: the marginal $F(x) = \int_{\mathbb{R}^m} f(x,y)\,dy$ (Bochner integral over volume; by hypothesis (3) each such integral is a genuine integral, so the convention " $\int = 0$ for non-integrable integrands" is not exercised) satisfies the same log-concavity predicate on all of $\mathbb{R}^n$ : $F(x) \ge 0$ everywhere, and $F(x_1)^a \cdot F(x_2)^b \le F(a x_1 + b x_2)$ for all $x_1, x_2$ and $a, b \ge 0$ with $a + b = 1$ . Degenerate case $m = 0$ : $\mathbb{R}^0$ is a one-point space of volume-measure mass $1$ , so $F(x) = f(x, \mathrm{pt})$ and the conclusion restates the hypothesis; $n = 0$ similarly collapses the outer variable.

Human review

Endorsed by Community (Bot) · Aug 11, 2026
Endorsed by Shuze Chen · Aug 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph