Documentation

LeanPool.CCDN.ArithmeticHeights.PrekopaLeindler

Modified for Lean/Mathlib 4.35.0: rename the real-weight AM-GM lemma to avoid a new Mathlib declaration.

The Prékopa–Leindler inequality #

Let a, b > 0 with a + b = 1 and let f, g, h be measurable ℝ≥0∞-valued functions on a real vector space carrying a measure, subject to

f x ^ a * g y ^ b ≤ h (a • x + b • y) for all x, y.

The Prékopa–Leindler inequality says that then

(∫⁻ f) ^ a * (∫⁻ g) ^ b ≤ ∫⁻ h.

It is the reverse of Hölder's inequality, it contains the Brunn–Minkowski inequality, and it is the one analytic ingredient Bombieri–Gubler import rather than prove in their treatment of Vaaler's cube-slicing theorem (their Lemma C.3.3, quoted from Prékopa). Mathlib has neither this inequality nor Brunn–Minkowski nor log-concavity, so this file starts from the one-dimensional Brunn–Minkowski inequality for sets.

Main definitions #

Main results #

Implementation notes #

⚠ The ℝ≥0∞ codomain and the hypothesis form of the statement remove every side condition. Bombieri–Gubler state C.3.3 with r t := ⨆ {f x * g y | a • x + b • y = t} on the right, and Prékopa's own erratum records that this sup-convolution is only guaranteed to be Lebesgue measurable. Taking h as given, with f x ^ a * g y ^ b ≤ h (a • x + b • y) as a hypothesis, avoids that question entirely; and because ∫⁻ is defined for every measurable ℝ≥0∞-valued function, there is no integrability hypothesis either. Every statement below is therefore hypothesis-free beyond measurability.

⚠ Prékopa–Leindler tensorizes, so the induction is on a product and not on coordinates. HasPrekopaLeindler.prod is Tonelli applied twice — integrate out the second factor to get three functions on the first, whose hypothesis is the original one read at (x₁, x₂) and (y₁, y₂) — and it mentions neither ℝ nor any dimension. So the n-dimensional theorem is the one-dimensional one, this closure property, and transport along a linear measure-preserving equivalence: hasPrekopaLeindler_pi is three lines. That is why the file is written around a predicate rather than around ℝ ^ n.

⚠ All the geometry is in one dimension, and it is Brunn–Minkowski for sets. After normalizing f and g to have supremum 1, the level sets {f > t} and {g > t} are nonempty for 0 < t < 1 and satisfy a • {f > t} + b • {g > t} ⊆ {h > t}; the inequality then follows from volume s + volume t ≤ volume (s + t) on ℝ and the layer cake formula. The Brunn–Minkowski step is proved for compact sets by translating s by sInf t and t by sSup s — the two translates lie in s + t and meet in a single point — and extended to measurable sets by inner regularity.

⚠ The normalization is what forces the truncation. The level-set argument needs ⨆ f finite and nonzero; ⨆ f = ∞ is a genuine case, since an unbounded function can have a finite integral. The general statement is therefore obtained from the bounded one by replacing f with min f (n + 1) and letting n → ∞, which needs (⨆ n, u n) ^ p = ⨆ n, u n ^ p for p > 0 — ENNReal.iSup_rpow below, which is ENNReal.orderIsoRpow and nothing more.

References #

A. Prékopa, On logarithmic concave measures and functions, Acta Sci. Math. 34 (1973), Theorem 3. This is the statement below, and it is the single step Bombieri–Gubler import.

E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Lemma C.3.3, in the appendix that proves Vaaler's cube-slicing theorem. Their C.3.4 — the log-concavity of a marginal — is in ArithmeticHeights.LogConcave, and is the only consumer of this file inside the roadmap.

This is Layer 4.5 (infrastructure) of the ArithmeticHeights roadmap.

source
theorem ENNReal.geom_mean_le_arith_mean2_weighted_real_weights {w₁ w₂ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂) (hw : w₁ + w₂ = 1) (p₁ p₂ : ENNReal) :
p₁ ^ w₁ * p₂ ^ w₂ ≤ ENNReal.ofReal w₁ * p₁ + ENNReal.ofReal w₂ * p₂

Weighted AM–GM in ℝ≥0∞, for two terms: the ℝ≥0∞-valued companion of NNReal.geom_mean_le_arith_mean2_weighted, stated with real weights because the exponents of ENNReal.rpow are real.

source
theorem ENNReal.iSup_rpow {ι : Sort u_1} (u : ι → ENNReal) {p : ℝ} (hp : 0 < p) :
(⨆ (i : ι), u i) ^ p = ⨆ (i : ι), u i ^ p

Raising to a positive real power commutes with suprema in ℝ≥0∞, because it is an order isomorphism.

source
theorem Real.volume_add_volume_le_volume_add {s t : Set ℝ} (hs : MeasurableSet s) (ht : MeasurableSet t) (hsne : s.Nonempty) (htne : t.Nonempty) :
MeasureTheory.volume s + MeasureTheory.volume t ≤ MeasureTheory.volume (s + t)

The one-dimensional Brunn–Minkowski inequality. For nonempty measurable sets s, t ⊆ ℝ, volume s + volume t ≤ volume (s + t). The sumset need not be measurable: volume is applied to it as an outer measure.

source
theorem MeasureTheory.lintegral_eq_lintegral_measure_ofReal_lt {α : Type u_1} [MeasurableSpace α] (μ : Measure α) [SFinite μ] {f : α → ENNReal} (hf : Measurable f) :
∫⁻ (x : α), f x ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {x : α | ENNReal.ofReal t < f x}

The layer cake formula for ℝ≥0∞-valued functions. Mathlib's Layercake file states this for real-valued functions; the ℝ≥0∞ form is what the Prékopa–Leindler proof needs, since the level sets there may well have infinite measure.

source
theorem Real.prekopaLeindler {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) {f g h : ℝ → ENNReal} (hf : Measurable f) (hg : Measurable g) (hh : Measurable h) (key : ∀ (x y : ℝ), f x ^ a * g y ^ b ≤ h (a • x + b • y)) :
(∫⁻ (x : ℝ), f x) ^ a * (∫⁻ (y : ℝ), g y) ^ b ≤ ∫⁻ (z : ℝ), h z

The Prékopa–Leindler inequality on ℝ.

source
def HasPrekopaLeindler {E : Type u_1} [MeasurableSpace E] [AddCommGroup E] [Module ℝ E] (μ : MeasureTheory.Measure E) :
Prop

HasPrekopaLeindler μ says that the Prékopa–Leindler inequality holds for the measure μ on the real vector space E: whenever f x ^ a * g y ^ b ≤ h (a • x + b • y) pointwise, with a, b > 0 and a + b = 1, the same inequality holds for the integrals.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem hasPrekopaLeindler_real :
    HasPrekopaLeindler MeasureTheory.volume

    Prékopa–Leindler holds for Lebesgue measure on ℝ.

    source
    theorem HasPrekopaLeindler.prod {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [AddCommGroup E] [Module ℝ E] [MeasurableSpace F] [AddCommGroup F] [Module ℝ F] {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure F} [MeasureTheory.SFinite ν] (hE : HasPrekopaLeindler μ) (hF : HasPrekopaLeindler ν) :
    HasPrekopaLeindler (μ.prod ν)

    Prékopa–Leindler tensorizes. Integrating out the second factor turns the hypothesis on E × F into the hypothesis on E for the three marginals, and Tonelli's theorem identifies the marginals' integrals with the original ones.

    source
    theorem HasPrekopaLeindler.of_measurePreserving {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [AddCommGroup E] [Module ℝ E] [MeasurableSpace F] [AddCommGroup F] [Module ℝ F] {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure F} (e : E ≃ₗ[ℝ] F) (he : MeasureTheory.MeasurePreserving (⇑e) μ ν) (hsymm : Measurable ⇑e.symm) (hF : HasPrekopaLeindler ν) :
    HasPrekopaLeindler μ

    Prékopa–Leindler transports along a measure-preserving linear equivalence.

    source
    theorem hasPrekopaLeindler_pi (n : ℕ) :
    HasPrekopaLeindler MeasureTheory.volume

    The Prékopa–Leindler inequality on Fin n → ℝ, by induction on n off hasPrekopaLeindler_real, HasPrekopaLeindler.prod and the measure-preserving linear equivalence (Fin (n + 1) → ℝ) ≃ₗ[ℝ] ℝ × (Fin n → ℝ).

    source
    theorem hasPrekopaLeindler_euclideanSpace (n : ℕ) :
    HasPrekopaLeindler MeasureTheory.volume

    The Prékopa–Leindler inequality on EuclideanSpace ℝ (Fin n), the space Layer 4.5 states cube slicing on.