Log-concave functions

A function f : E → ℝ≥0∞ on a real vector space is log-concave if f x ^ a * f y ^ b ≤ f (a • x + b • y) whenever 0 ≤ a, 0 ≤ b and a + b = 1. For a positive real-valued function this says exactly that its logarithm is concave (TauCeti.logConcave_ofReal_exp_iff), while the value 0 allowed by ℝ≥0∞ makes the indicator of a convex set log-concave.

Taking values in ℝ≥0∞ is what makes the notion stable under integration: the marginal x ↦ ∫⁻ y, f (x, y) ∂ν of a log-concave function is log-concave whenever ν satisfies the Prékopa–Leindler inequality, with no finiteness hypothesis on the integrals (TauCeti.LogConcave.lintegral_prod_right, in TauCeti.MeasureTheory.Integral.PrekopaLeindler). Marginals of this kind are the measures of the slices of a convex body, and are the objects of Vaaler's cube-slicing theorem.

Main definitions

• TauCeti.LogConcave f: the function f : E → ℝ≥0∞ is log-concave.

Main results

• TauCeti.logConcave_ofReal_exp_iff: x ↦ exp (g x) is log-concave if and only if g is concave.
• TauCeti.logConcave_ofReal_exp_neg_mul_sq_norm: the Gaussian x ↦ exp (-c ‖x‖ ^ 2) is log-concave.
• TauCeti.logConcave_indicator_iff: the indicator of a set at a nonzero value is log-concave if and only if the set is convex.
• TauCeti.LogConcave.convex_support, TauCeti.LogConcave.convex_ge, TauCeti.LogConcave.convex_gt: the support and the superlevel sets of a log-concave function are convex.
• TauCeti.LogConcave.mul, TauCeti.LogConcave.comp_linearMap: products and linear substitutions preserve log-concavity.
• TauCeti.LogConcave.apply_le_apply_zero: an even log-concave function is largest at the origin.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press, 2006, Definition C.3.1 and Remark C.3.2.

The definition and the convexity statements are adapted from the Apache-2.0 formalization of Vaaler's theorem in rwst/Subspace-Theorems (file ArithmeticHeights/LogConcave.lean), by Ralf Stephan.

def TauCeti.LogConcave {E : Type u_1} [AddCommMonoid E] [Module ℝ E] (f : E → ENNReal) : Prop

A function f : E → ℝ≥0∞ on a real vector space is log-concave if f x ^ a * f y ^ b ≤ f (a • x + b • y) for all x, y and all weights 0 ≤ a, 0 ≤ b with a + b = 1. For positive real-valued f this says that Real.log ∘ f is concave.

theorem TauCeti.logConcave_def {E : Type u_1} [AddCommMonoid E] [Module ℝ E] {f : E → ENNReal} : LogConcave f ↔ ∀ ⦃x y : E⦄ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f x ^ a * f y ^ b ≤ f (a • x + b • y)

theorem TauCeti.LogConcave.rpow_mul_rpow_le {E : Type u_1} [AddCommMonoid E] [Module ℝ E] {f : E → ENNReal} (hf : LogConcave f) {x y : E} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : f x ^ a * f y ^ b ≤ f (a • x + b • y)

The defining inequality of a log-concave function.

theorem TauCeti.LogConcave.ge_on_segment' {E : Type u_1} [AddCommMonoid E] [Module ℝ E] {f : E → ENNReal} (hf : LogConcave f) {x y : E} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : min (f x) (f y) ≤ f (a • x + b • y)

The minimum of two values of a log-concave function is at most its value at any convex combination of the two points.

theorem TauCeti.LogConcave.convex_ge {E : Type u_1} [AddCommMonoid E] [Module ℝ E] {f : E → ENNReal} (hf : LogConcave f) (r : ENNReal) : Convex ℝ {x : E | r ≤ f x}

Every superlevel set of a log-concave function is convex.

theorem TauCeti.LogConcave.convex_gt {E : Type u_1} [AddCommMonoid E] [Module ℝ E] {f : E → ENNReal} (hf : LogConcave f) (r : ENNReal) : Convex ℝ {x : E | r < f x}

Every strict superlevel set of a log-concave function is convex.

theorem TauCeti.LogConcave.convex_support {E : Type u_1} [AddCommMonoid E] [Module ℝ E] {f : E → ENNReal} (hf : LogConcave f) : Convex ℝ (Function.support f)

The support of a log-concave function is convex (Bombieri–Gubler, Remark C.3.2).

theorem TauCeti.LogConcave.mul {E : Type u_1} [AddCommMonoid E] [Module ℝ E] {f g : E → ENNReal} (hf : LogConcave f) (hg : LogConcave g) : LogConcave (f * g)

A product of log-concave functions is log-concave.

theorem TauCeti.LogConcave.comp_linearMap {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] {f : E → ENNReal} (hf : LogConcave f) (L : F →ₗ[ℝ] E) : LogConcave (f ∘ ⇑L)

Composing a log-concave function with a linear map gives a log-concave function.

theorem TauCeti.LogConcave.apply_le_apply_zero {G : Type u_3} [AddCommGroup G] [Module ℝ G] {f : G → ENNReal} (hf : LogConcave f) (hfe : Function.Even f) (x : G) : f x ≤ f 0

An even log-concave function is largest at the origin. Applied to the measures of the parallel slices of a symmetric convex body, this says that the central slice is the largest.

theorem TauCeti.logConcave_const {E : Type u_1} [AddCommMonoid E] [Module ℝ E] (c : ENNReal) : LogConcave fun (x : E) => c

A constant function is log-concave.

theorem Convex.logConcave_indicator {E : Type u_1} [AddCommMonoid E] [Module ℝ E] {s : Set E} (hs : Convex ℝ s) (c : ENNReal) : TauCeti.LogConcave (s.indicator fun (x : E) => c)

The indicator of a convex set is log-concave, at any value.

theorem TauCeti.logConcave_indicator_iff {E : Type u_1} [AddCommMonoid E] [Module ℝ E] {s : Set E} {c : ENNReal} (hc : c ≠ 0) : LogConcave (s.indicator fun (x : E) => c) ↔ Convex ℝ s

The indicator of a set at a nonzero value is log-concave if and only if the set is convex.

theorem TauCeti.logConcave_ofReal_exp_iff {E : Type u_1} [AddCommMonoid E] [Module ℝ E] {g : E → ℝ} : (LogConcave fun (x : E) => ENNReal.ofReal (Real.exp (g x))) ↔ ConcaveOn ℝ Set.univ g

A function x ↦ exp (g x) is log-concave if and only if g is concave.

theorem TauCeti.logConcave_ofReal_exp_neg_mul_sq_norm {G : Type u_3} [SeminormedAddCommGroup G] [NormedSpace ℝ G] {c : ℝ} (hc : 0 ≤ c) : LogConcave fun (x : G) => ENNReal.ofReal (Real.exp (-c * ‖x‖ ^ 2))

The Gaussian x ↦ exp (-c ‖x‖ ^ 2) on a real normed space is log-concave for 0 ≤ c.