The Prékopa–Leindler inequality

Following Terence Tao's blog post on the Brunn–Minkowski inequality, this file proves the Prékopa–Leindler inequality on ℝⁿ (with n = d + 1). The proof proceeds by reducing to the one-dimensional case via the layer-cake formula and then induction on the dimension.

theorem brunn_minkowski_1d_compact {A B C : Set ℝ} (h : A + B ⊆ C) (hA_nonempty : A.Nonempty) (hA_compact : IsCompact A) (hB_nonempty : B.Nonempty) (hB_compact : IsCompact B) : MeasureTheory.volume A + MeasureTheory.volume B ≤ MeasureTheory.volume C

Brunn–Minkowski in one dimension for compact sets.

theorem brunn_minkowski_1d_infinite {A B C : Set ℝ} (ha : MeasureTheory.volume A = ⊤) (hb : B.Nonempty) (hc : A + B ⊆ C) : MeasureTheory.volume A + MeasureTheory.volume B ≤ MeasureTheory.volume C

Brunn–Minkowski in one dimension when one of the sets has infinite volume.

theorem brunn_minkowski_1d {A B C : Set ℝ} (h : A + B ⊆ C) (hA_nonempty : A.Nonempty) (hA_measurable : MeasurableSet A) (hB_nonempty : B.Nonempty) (hB_measurable : MeasurableSet B) : MeasureTheory.volume A + MeasureTheory.volume B ≤ MeasureTheory.volume C

Brunn–Minkowski in one dimension for measurable sets.

theorem vol_superlevelset_measurable (f : ℝ → ENNReal) : Measurable fun (t : ℝ) => MeasureTheory.volume {x : ℝ | ENNReal.ofReal t ≤ f x}

The volume of the superlevel set {x | t ≤ f x} is measurable in t.

theorem layercake {f : ℝ → ENNReal} (hf_measurable : Measurable f) : ∫⁻ (x : ℝ), f x = ∫⁻ (t : ℝ) in Set.Ioi 0, MeasureTheory.volume {x : ℝ | ENNReal.ofReal t ≤ f x}

The layer-cake formula for ENNReal-valued functions on ℝ.

theorem lintegral_eq_vol_superlevelset_lintegral_01 {f : ℝ → ENNReal} (hf_bound : f ≤ 1) (hf_measurable : Measurable f) : ∫⁻ (x : ℝ), f x = ∫⁻ (t : ℝ) in Set.Ioo 0 1, (fun (t : ℝ) => MeasureTheory.volume {x : ℝ | ENNReal.ofReal t ≤ f x}) t

Layer-cake formula on (0, 1) for functions bounded by 1.

theorem weighted_amgm {θ a b : ℝ} (hθ : 0 < θ ∧ θ < 1) (ha : 0 ≤ a) (hb : 0 ≤ b) : ((1 - θ) ^ (1 - θ) * θ ^ θ)⁻¹ * a ^ (1 - θ) * b ^ θ ≤ a + b

A weighted AM–GM inequality.

theorem prekopa_leindler_1d_normalized {θ : ℝ} {f g h : ℝ → ENNReal} (hθ : 0 < θ ∧ θ < 1) (hf_measurable : Measurable f) (hf_sup1 : iSup f = 1) (hg_measurable : Measurable g) (hg_sup1 : iSup g = 1) (hh_measurable : Measurable h) (hfgh : ∀ (x y : ℝ), f x ^ (1 - θ) * g y ^ θ ≤ h (x + y)) : ENNReal.ofReal ((1 - θ) ^ (1 - θ) * θ ^ θ)⁻¹ * (∫⁻ (x : ℝ), f x) ^ (1 - θ) * (∫⁻ (x : ℝ), g x) ^ θ ≤ ∫⁻ (x : ℝ), h x

Prékopa–Leindler in one dimension assuming sup norm 1.

theorem prekopa_leindler_1d_bounded {θ : ℝ} {f g h : ℝ → ENNReal} (hθ : 0 < θ ∧ θ < 1) (hf_measurable : Measurable f) (hf_bounded : iSup f ≠ ⊤) (hg_measurable : Measurable g) (hg_bounded : iSup g ≠ ⊤) (hh_measurable : Measurable h) (hfgh : ∀ (x y : ℝ), f x ^ (1 - θ) * g y ^ θ ≤ h (x + y)) : ENNReal.ofReal ((1 - θ) ^ (1 - θ) * θ ^ θ)⁻¹ * (∫⁻ (x : ℝ), f x) ^ (1 - θ) * (∫⁻ (x : ℝ), g x) ^ θ ≤ ∫⁻ (x : ℝ), h x

Prékopa–Leindler in one dimension assuming bounded sup norm. This removes the sup norm 1 assumption of prekopa_leindler_1d_normalized by scaling.

theorem prekopa_leindler_1d {θ : ℝ} {f g h : ℝ → ENNReal} (hθ : 0 < θ ∧ θ < 1) (hf_measurable : Measurable f) (hg_measurable : Measurable g) (hh_measurable : Measurable h) (hfgh : ∀ (x y : ℝ), f x ^ (1 - θ) * g y ^ θ ≤ h (x + y)) : ENNReal.ofReal ((1 - θ) ^ (1 - θ) * θ ^ θ)⁻¹ * (∫⁻ (x : ℝ), f x) ^ (1 - θ) * (∫⁻ (x : ℝ), g x) ^ θ ≤ ∫⁻ (x : ℝ), h x

Prékopa–Leindler in one dimension. This removes the boundedness assumption of prekopa_leindler_1d_bounded using an approximation argument.

theorem lintegral_fin1 (F : (Fin 1 → ℝ) → ENNReal) : ∫⁻ (v : Fin 1 → ℝ), F v = ∫⁻ (x : ℝ), F fun (x_1 : Fin 1) => x

Lebesgue integral over Fin 1 → ℝ rewritten as an integral over ℝ.

def append {d : ℕ} (x : Fin d → ℝ) (t : Fin 1 → ℝ) : Fin (d + 1) → ℝ

Append a single coordinate to a vector to get a vector with one more coordinate.

Equations

• append x t i = if h : ↑i < d then x ⟨↑i, h⟩ else t default

theorem append_measurable {d : ℕ} (x : Fin d → ℝ) : Measurable (append x)

append x is measurable in its second argument.

theorem append_measurable' {d : ℕ} (t : Fin 1 → ℝ) : Measurable fun (x : Fin d → ℝ) => append x t

append · t is measurable in its first argument.

theorem append_linear {d : ℕ} (x1 y1 : Fin (d + 1) → ℝ) (x y : Fin 1 → ℝ) : append x1 x + append y1 y = append (x1 + y1) (x + y)

append distributes over addition.

def fix {d : ℕ} (F : (Fin (d + 1) → ℝ) → ENNReal) (x : Fin d → ℝ) : (Fin 1 → ℝ) → ENNReal

Turn a function F : ℝ^{d+1} → ENNReal into a function ℝ^1 → ENNReal by fixing the first d components to x.

Equations

• fix F x = F ∘ append x

theorem fix_measurable {d : ℕ} {F : (Fin (d + 1) → ℝ) → ENNReal} (hF : Measurable F) (x : Fin d → ℝ) : Measurable (fix F x)

fix of a measurable function is measurable.

theorem fix_apply {d : ℕ} (F : (Fin (d + 1) → ℝ) → ENNReal) (x : Fin d → ℝ) (y : Fin 1 → ℝ) : fix F x y = F (append x y)

Application form of fix.

theorem lintegral_fix_eq_lmarginal {d : ℕ} (F : (Fin (d + 2) → ℝ) → ENNReal) (x1 : Fin (d + 1) → ℝ) : ∫⁻ (y : Fin 1 → ℝ), fix F x1 y = (∫⋯∫⁻_{⟨d + 1, ⋯⟩}, F ∂fun (x : Fin (d + 2)) => MeasureTheory.volume) (append x1 default)

The integral of fix F x1 over Fin 1 → ℝ equals an lmarginal of F.

theorem lintegral_fix_lintegral_eq_lintegral {d : ℕ} {f : (Fin (d + 2) → ℝ) → ENNReal} (hf_measurable : Measurable f) : ∫⁻ (x : Fin (d + 1) → ℝ) (t : Fin 1 → ℝ), fix f x t = ∫⁻ (x : Fin (d + 2) → ℝ), f x

Iterated integral of fix f recovers the integral of f.

def PLConditions (n : ℕ) (θ : ℝ) (f g h : (Fin n → ℝ) → ENNReal) : Prop

The hypotheses of the Prékopa–Leindler inequality bundled together.

Equations

• PLConditions n θ f g h = (0 < θ ∧ θ < 1 ∧ Measurable f ∧ Measurable g ∧ Measurable h ∧ ∀ (x y : Fin n → ℝ), f x ^ (1 - θ) * g y ^ θ ≤ h (x + y))

theorem prekopa_leindler_1d_fin1 {θ : ℝ} {f g h : (Fin 1 → ℝ) → ENNReal} (hθfgh : PLConditions 1 θ f g h) : ENNReal.ofReal ((1 - θ) ^ (1 - θ) * θ ^ θ)⁻¹ * (∫⁻ (x : Fin 1 → ℝ), f x) ^ (1 - θ) * (∫⁻ (x : Fin 1 → ℝ), g x) ^ θ ≤ ∫⁻ (x : Fin 1 → ℝ), h x

Prékopa–Leindler for Fin 1 → ℝ (a small wrapper around prekopa_leindler_1d).

theorem prekopa_leindler {d : ℕ} {θ : ℝ} {f g h : (Fin (d + 1) → ℝ) → ENNReal} (hθfgh : PLConditions (d + 1) θ f g h) : ENNReal.ofReal ((1 - θ) ^ ((↑d + 1) * (1 - θ)) * θ ^ ((↑d + 1) * θ))⁻¹ * (∫⁻ (x : Fin (d + 1) → ℝ), f x) ^ (1 - θ) * (∫⁻ (x : Fin (d + 1) → ℝ), g x) ^ θ ≤ ∫⁻ (x : Fin (d + 1) → ℝ), h x

The Prékopa–Leindler inequality in arbitrary dimension, proved by induction over the dimension.