The Prékopa–Leindler inequality

For a measure on a real module, Measure.HasPrekopaLeindler θ records the weighted Prékopa–Leindler inequality for measurable ℝ≥0∞-valued functions. Its pointwise hypothesis is imposed on the chosen measurable representatives, rather than only almost everywhere, so it is stable under taking sections.

The property tensorizes: if two measures have the Prékopa–Leindler property at the same weight, then their product measure has it as well. Tonelli's theorem first applies the inequality in the second variable and then applies it to the resulting marginal integrals in the first variable, so only the second factor needs to be s-finite. Iterating over the coordinates, a finite product of σ-finite measures with the property has it as well.

The property is also transported by measure-preserving maps which preserve the weighted affine combination. This makes tensorization usable after changing linear coordinates or projecting to a marginal.

Lebesgue measure on ℝ has the property for every weight 0 ≤ θ ≤ 1; the endpoints are monotonicity of the integral. The interior case rests on a version of the inequality for the minimum: if f and g have the same supremum and min (f x) (g y) ≤ h (c * x + d * y), then each superlevel set of h contains the weighted Minkowski sum of those of f and g, which are nonempty below the common supremum, so one-dimensional Brunn–Minkowski and the layer-cake formula give c ∫ f + d ∫ g ≤ ∫ h. Normalizing the suprema of bounded f and g to one and applying the weighted AM-GM inequality gives Prékopa–Leindler, and truncation removes the boundedness. Tensorization then gives the inequality for Lebesgue measure on ι → ℝ, and linear isometries transport it to every finite-dimensional real inner product space.

Applied once in the second variable, the inequality says that a marginal x ↦ ∫⁻ y, f (x, y) ∂ν of a log-concave function f is log-concave. For the indicator of a convex set this is Brunn's principle in log-concave form: the measures of the parallel slices of a convex set form a log-concave function, so for a symmetric convex set the central slice is the largest. This is the form in which Vaaler's cube-slicing theorem uses the inequality.

Main results

• MeasureTheory.Measure.HasPrekopaLeindler: the measurable extended-integral inequality.
• MeasureTheory.Measure.HasPrekopaLeindler.prod: tensorization over product measures.
• MeasureTheory.Measure.HasPrekopaLeindler.pi: tensorization over finite products.
• MeasureTheory.Measure.HasPrekopaLeindler.map: transport by a measure-preserving affine map.
• MeasureTheory.Measure.HasPrekopaLeindler.smul: the property is stable under scaling the measure at weights 0 ≤ θ ≤ 1.
• MeasureTheory.Measure.HasPrekopaLeindler.withDensity, MeasureTheory.Measure.HasPrekopaLeindler.restrict: log-concave densities and restriction to convex sets preserve the property.
• TauCeti.Real.mul_lintegral_add_mul_lintegral_le: the inequality for the minimum on ℝ.
• TauCeti.Real.hasPrekopaLeindler_volume: the Prékopa–Leindler inequality on ℝ.
• TauCeti.hasPrekopaLeindler_volume_pi, MeasureTheory.Measure.hasPrekopaLeindler_of_isAddHaarMeasure, TauCeti.hasPrekopaLeindler_volume: the inequality on ι → ℝ, for every additive Haar measure on a finite-dimensional real normed space, and for the volume of a finite-dimensional real inner product space.
• TauCeti.LogConcave.lintegral_prod_right, TauCeti.LogConcave.setLIntegral_prod_right: marginals of log-concave functions are log-concave.
• Convex.logConcave_measure_preimage_prodMk: the slice measures of a convex set are log-concave.
• Convex.measure_preimage_prodMk_le_measure_preimage_prodMk_zero: the central slice of a symmetric convex set is the largest.

References

• A. Prékopa, Logarithmic concave measures with application to stochastic programming, Acta Scientiarum Mathematicarum 32 (1971), 301–316.
• L. Leindler, On a certain converse of Hölder's inequality II, Acta Scientiarum Mathematicarum 33 (1972), 217–223.
• E. H. Lieb and M. Loss, Analysis, 2nd ed., AMS, 2001, Section 4.3.
• R. J. Gardner, The Brunn–Minkowski inequality, Bull. Amer. Math. Soc. 39 (2002), 355–405, for the one-dimensional level-set argument.
• Terence Tao, [The Brunn–Minkowski inequality for nilpotent groups] (https://terrytao.wordpress.com/2011/09/16/the-brunn-minkowski-inequality-for-nilpotent-groups/).
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press, 2006, Lemma C.3.4, for marginals of log-concave functions. The statements and proofs of the marginal results are adapted from the Apache-2.0 formalization in rwst/Subspace-Theorems (files ArithmeticHeights/LogConcave.lean and ArithmeticHeights/CubeSlicing.lean), by Ralf Stephan.

def MeasureTheory.Measure.HasPrekopaLeindler {E : Type u_1} [MeasurableSpace E] [AddCommMonoid E] [Module ℝ E] (mu : Measure E) (theta : ℝ) : Prop

A measure has the Prékopa–Leindler property at weight θ if every three measurable nonnegative extended-valued functions satisfying the pointwise weighted geometric-mean bound also satisfy the corresponding bound on their integrals.

The pointwise bound is deliberately imposed on the supplied measurable representatives. This is the form which tensorizes without choosing new representatives on individual sections.

theorem MeasureTheory.Measure.hasPrekopaLeindler_def {E : Type u_1} [MeasurableSpace E] [AddCommMonoid E] [Module ℝ E] (mu : Measure E) (theta : ℝ) : mu.HasPrekopaLeindler theta ↔ ∀ {f g h : E → ENNReal}, Measurable f → Measurable g → Measurable h → (∀ (x y : E), (f x).rpow (1 - theta) * (g y).rpow theta ≤ h ((1 - theta) • x + theta • y)) → (∫⁻ (x : E), f x ∂mu).rpow (1 - theta) * (∫⁻ (x : E), g x ∂mu).rpow theta ≤ ∫⁻ (x : E), h x ∂mu

The Prékopa–Leindler property unfolded into its measurable-function formulation.

theorem MeasureTheory.Measure.hasPrekopaLeindler_dirac {E : Type u_1} [MeasurableSpace E] [AddCommMonoid E] [Module ℝ E] (a : E) (theta : ℝ) : (dirac a).HasPrekopaLeindler theta

A Dirac mass has the Prékopa–Leindler property at every weight.

theorem MeasureTheory.Measure.HasPrekopaLeindler.map {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [MeasurableSpace F] [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] {mu : Measure E} {nu : Measure F} {theta : ℝ} (hmu : mu.HasPrekopaLeindler theta) (e : E → F) (he : MeasurePreserving e mu nu) (haffine : ∀ (x y : E), e ((1 - theta) • x + theta • y) = (1 - theta) • e x + theta • e y) : nu.HasPrekopaLeindler theta

Transport the Prékopa–Leindler property through a measure-preserving map which preserves the weighted affine combination.

theorem MeasureTheory.Measure.HasPrekopaLeindler.prod {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [MeasurableSpace F] [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] {mu : Measure E} {nu : Measure F} [SFinite nu] {theta : ℝ} (hmu : mu.HasPrekopaLeindler theta) (hnu : nu.HasPrekopaLeindler theta) : (mu.prod nu).HasPrekopaLeindler theta

Tensorization of Prékopa–Leindler. If mu and nu satisfy the inequality at the same weight, then so does their product measure.

theorem MeasureTheory.Measure.HasPrekopaLeindler.of_measurePreserving {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [MeasurableSpace F] [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] {mu : Measure E} {nu : Measure F} {theta : ℝ} (hnu : nu.HasPrekopaLeindler theta) (e : E ≃ᵐ F) (he : MeasurePreserving (⇑e) mu nu) (haffine : ∀ (x y : E), e ((1 - theta) • x + theta • y) = (1 - theta) • e x + theta • e y) : mu.HasPrekopaLeindler theta

Pull the Prékopa–Leindler property back along a measure-preserving measurable equivalence whose forward map preserves the weighted affine combination.

theorem MeasureTheory.Measure.HasPrekopaLeindler.pi {ι : Type u_3} [Fintype ι] {α : ι → Type u_4} [(i : ι) → MeasurableSpace (α i)] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → Module ℝ (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] {theta : ℝ} (h : ∀ (i : ι), (μ i).HasPrekopaLeindler theta) : (Measure.pi μ).HasPrekopaLeindler theta

Tensorization of Prékopa–Leindler over finite products. If σ-finite measures μ i on finitely many real modules all satisfy the inequality at the same weight, then so does their product measure.

theorem MeasureTheory.Measure.HasPrekopaLeindler.withDensity {E : Type u_1} [MeasurableSpace E] [AddCommMonoid E] [Module ℝ E] {mu : Measure E} {theta : ℝ} (hmu : mu.HasPrekopaLeindler theta) (hθ₀ : 0 ≤ theta) (hθ₁ : theta ≤ 1) {φ : E → ENNReal} (hφ : Measurable φ) (hlc : TauCeti.LogConcave φ) : (mu.withDensity φ).HasPrekopaLeindler theta

A log-concave density preserves Prékopa–Leindler. If mu has the Prékopa–Leindler property at a weight 0 ≤ θ ≤ 1 and φ is measurable and log-concave, then mu.withDensity φ has it as well. For instance, the Gaussian density exp (-π ‖x‖ ^ 2) is log-concave.

theorem MeasureTheory.Measure.HasPrekopaLeindler.smul {E : Type u_1} [MeasurableSpace E] [AddCommMonoid E] [Module ℝ E] {mu : Measure E} {theta : ℝ} (hmu : mu.HasPrekopaLeindler theta) (hθ₀ : 0 ≤ theta) (hθ₁ : theta ≤ 1) (c : ENNReal) : (c • mu).HasPrekopaLeindler theta

Scaling a measure preserves the Prékopa–Leindler property at a weight 0 ≤ θ ≤ 1: the inequality is homogeneous of degree one in the measure.

theorem MeasureTheory.Measure.HasPrekopaLeindler.restrict {E : Type u_1} [MeasurableSpace E] [AddCommMonoid E] [Module ℝ E] {mu : Measure E} {theta : ℝ} (hmu : mu.HasPrekopaLeindler theta) (hθ₀ : 0 ≤ theta) (hθ₁ : theta ≤ 1) {s : Set E} (hs : MeasurableSet s) (hsc : Convex ℝ s) : (mu.restrict s).HasPrekopaLeindler theta

The restriction of a measure with the Prékopa–Leindler property at a weight 0 ≤ θ ≤ 1 to a measurable convex set has the Prékopa–Leindler property as well.

theorem TauCeti.Real.mul_lintegral_add_mul_lintegral_le {f g h : ℝ → ENNReal} (hf : AEMeasurable f MeasureTheory.volume) (hg : AEMeasurable g MeasureTheory.volume) (hh : AEMeasurable h MeasureTheory.volume) (hfg : ⨆ (x : ℝ), f x = ⨆ (y : ℝ), g y) {c d : ℝ} (hmin : ∀ (x y : ℝ), min (f x) (g y) ≤ h (c * x + d * y)) : (ENNReal.ofReal c * ∫⁻ (x : ℝ), f x) + ENNReal.ofReal d * ∫⁻ (y : ℝ), g y ≤ ∫⁻ (z : ℝ), h z

Prékopa–Leindler inequality for the minimum on ℝ. If f and g have the same supremum and h (c * x + d * y) dominates min (f x) (g y) for all x and y, then c ∫ f + d ∫ g ≤ ∫ h. The coefficients may vanish, and the common supremum and the integrals may be infinite. A negative coefficient contributes nothing to the left side.

theorem TauCeti.Real.hasPrekopaLeindler_volume {θ : ℝ} (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : MeasureTheory.volume.HasPrekopaLeindler θ

The Prékopa–Leindler inequality on ℝ: Lebesgue measure has the Prékopa–Leindler property at every weight 0 ≤ θ ≤ 1.

theorem TauCeti.hasPrekopaLeindler_volume_pi (ι : Type u_1) [Fintype ι] {θ : ℝ} (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : MeasureTheory.volume.HasPrekopaLeindler θ

The Prékopa–Leindler inequality on ι → ℝ: Lebesgue measure on a finite power of ℝ has the Prékopa–Leindler property at every weight 0 ≤ θ ≤ 1.

theorem MeasureTheory.Measure.hasPrekopaLeindler_of_isAddHaarMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] {θ : ℝ} (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : μ.HasPrekopaLeindler θ

The Prékopa–Leindler inequality for Haar measure: every additive Haar measure on a finite-dimensional real normed space has the Prékopa–Leindler property at every weight 0 ≤ θ ≤ 1.

theorem TauCeti.hasPrekopaLeindler_volume (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {θ : ℝ} (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : MeasureTheory.volume.HasPrekopaLeindler θ

The Prékopa–Leindler inequality on a finite-dimensional real inner product space, such as EuclideanSpace ℝ (Fin n): its volume has the Prékopa–Leindler property at every weight 0 ≤ θ ≤ 1.

Marginals of log-concave functions

theorem TauCeti.LogConcave.lintegral_prod_right {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [AddCommMonoid E] [Module ℝ E] [MeasurableSpace F] [AddCommMonoid F] [Module ℝ F] {ν : MeasureTheory.Measure F} (hν : ∀ ⦃θ : ℝ⦄, 0 ≤ θ → θ ≤ 1 → ν.HasPrekopaLeindler θ) {f : E × F → ENNReal} (hf : Measurable f) (hlc : LogConcave f) : LogConcave fun (x : E) => ∫⁻ (y : F), f (x, y) ∂ν

Marginals of log-concave functions are log-concave (Prékopa; Bombieri–Gubler, Lemma C.3.4). If f : E × F → ℝ≥0∞ is measurable and log-concave and ν has the Prékopa–Leindler property at every weight, then x ↦ ∫⁻ y, f (x, y) ∂ν is log-concave. No measure on E and no finiteness of the integrals is needed.

theorem TauCeti.LogConcave.setLIntegral_prod_right {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [AddCommMonoid E] [Module ℝ E] [MeasurableSpace F] [AddCommMonoid F] [Module ℝ F] {ν : MeasureTheory.Measure F} (hν : ∀ ⦃θ : ℝ⦄, 0 ≤ θ → θ ≤ 1 → ν.HasPrekopaLeindler θ) {f : E × F → ENNReal} (hf : Measurable f) (hlc : LogConcave f) {s : Set F} (hs : MeasurableSet s) (hsc : Convex ℝ s) : LogConcave fun (x : E) => ∫⁻ (y : F) in s, f (x, y) ∂ν

Marginals over a convex set of log-concave functions are log-concave (Bombieri–Gubler, Lemma C.3.4). If f : E × F → ℝ≥0∞ is measurable and log-concave, s ⊆ F is measurable and convex, and ν has the Prékopa–Leindler property at every weight, then x ↦ ∫⁻ y in s, f (x, y) ∂ν is log-concave.

theorem Convex.logConcave_measure_preimage_prodMk {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [AddCommMonoid E] [Module ℝ E] [MeasurableSpace F] [AddCommMonoid F] [Module ℝ F] {ν : MeasureTheory.Measure F} (hν : ∀ ⦃θ : ℝ⦄, 0 ≤ θ → θ ≤ 1 → ν.HasPrekopaLeindler θ) {s : Set (E × F)} (hs : MeasurableSet s) (hsc : Convex ℝ s) : TauCeti.LogConcave fun (x : E) => ν (Prod.mk x ⁻¹' s)

Brunn's principle, in log-concave form. For a measurable convex set s ⊆ E × F and a measure ν with the Prékopa–Leindler property at every weight, the measure of the slices, x ↦ ν (Prod.mk x ⁻¹' s), is log-concave.

theorem Convex.measure_preimage_prodMk_le_measure_preimage_prodMk_zero {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [AddCommGroup E] [Module ℝ E] [MeasurableSpace F] [AddCommGroup F] [Module ℝ F] {ν : MeasureTheory.Measure F} [MeasurableNeg F] [ν.IsNegInvariant] (hν : ∀ ⦃θ : ℝ⦄, 0 ≤ θ → θ ≤ 1 → ν.HasPrekopaLeindler θ) {s : Set (E × F)} (hs : MeasurableSet s) (hsc : Convex ℝ s) (hneg : ∀ p ∈ s, -p ∈ s) (x : E) : ν (Prod.mk x ⁻¹' s) ≤ ν (Prod.mk 0 ⁻¹' s)

The central slice of a symmetric convex set is the largest. For a measurable convex set s ⊆ E × F with -s = s and a negation-invariant measure ν with the Prékopa–Leindler property at every weight, every slice Prod.mk x ⁻¹' s has measure at most that of the central slice Prod.mk 0 ⁻¹' s.