Log-concave functions, and the log-concavity of a marginal

A function f with values in ℝ≥0∞ is log-concave if

f x ^ a * f y ^ b ≤ f (a • x + b • y) for all x, y and all a, b > 0 with a + b = 1,

which for a positive real-valued function says exactly that log ∘ f is concave. The two facts about log-concave functions that Vaaler's cube-slicing theorem needs are here: the set where such a function is nonzero is convex, and a marginal of a log-concave function over a convex set is log-concave. The second is Bombieri–Gubler's Lemma C.3.4, and it is the only consumer of the Prékopa–Leindler inequality inside the roadmap.

Main definitions

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

Main results

• LogConcave.convex_support: {x | f x ≠ 0} is convex (Bombieri–Gubler, Remark C.3.2).
• LogConcave.convex_lt: every strict superlevel set {x | c < f x} is convex.
• logConcave_indicator: the indicator of a convex set, at any value, is log-concave.
• LogConcave.mul: a product of log-concave functions is log-concave.
• LogConcave.setLIntegral_prod_right: Bombieri–Gubler, Lemma C.3.4. If f is a log-concave function on E × F and A ⊆ F is convex and measurable, then x ↦ ∫⁻ y in A, f (x, y) is log-concave on E, provided Prékopa–Leindler holds on F.

Implementation notes

⚠ Log-concavity is stated for ℝ≥0∞-valued functions, not for the book's nonnegative real ones. The functions that C.3.4 and C.3.7 apply it to are measures of slices — y ↦ vol (B ∩ A_y) in Bombieri–Gubler's own induction step — so ℝ≥0∞ is where they naturally live, and there the statement carries no finiteness hypothesis at all. Bombieri–Gubler have to say "if the integral is always finite" in C.3.4; here that hypothesis is absent. The codomain supplies nonnegativity and permits infinite values.

⚠ 0 ^ a = 0 for a > 0 is what makes the characteristic function of a convex set log-concave, with no case distinction beyond membership, and that is the whole of Bombieri–Gubler's step from C.3.3 to C.3.4: their f i y = χ_A y * f (x i, y) is log-concave because a product of log-concave functions is, and χ_A is log-concave because A is convex. The proof of LogConcave.setLIntegral_prod_right below inlines that product rather than forming it, since the Prékopa–Leindler hypothesis is checked pointwise anyway.

⚠ C.3.4 needs nothing of E but that it is a real vector space. There is no measure on E, no finite-dimensionality, and no measurability hypothesis on the marginal: log-concavity is a pointwise statement in x, and the Prékopa–Leindler inequality is applied on F alone, once for each pair x₁, x₂.

References

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

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

def LogConcave {E : Type u_1} [AddCommGroup 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 a, b > 0 summing to 1; for positive real-valued f this says that log ∘ f is concave.

Equations

• LogConcave f = ∀ (a b : ℝ), 0 < a → 0 < b → a + b = 1 → ∀ (x y : E), f x ^ a * f y ^ b ≤ f (a • x + b • y)

theorem LogConcave.convex_support {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ENNReal} (hf : LogConcave f) : Convex ℝ {x : E | f x ≠ 0}

The set where a log-concave function is nonzero is convex (Bombieri–Gubler, Remark C.3.2).

theorem LogConcave.convex_lt {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ENNReal} (hf : LogConcave f) (c : ENNReal) : Convex ℝ {x : E | c < f x}

Every strict superlevel set of a log-concave function is convex. This is what makes the layer-cake decomposition of a log-concave density a superposition of convex symmetric sets, which is the form Bombieri–Gubler's Lemma C.3.7 consumes.

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

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

theorem LogConcave.mul {E : Type u_1} [AddCommGroup 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 LogConcave.setLIntegral_prod_right {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [AddCommGroup E] [Module ℝ E] [MeasurableSpace F] [AddCommGroup F] [Module ℝ F] {ν : MeasureTheory.Measure F} (hF : HasPrekopaLeindler ν) {f : E × F → ENNReal} (hf : Measurable f) (hlc : LogConcave f) {A : Set F} (hA : MeasurableSet A) (hAc : Convex ℝ A) : LogConcave fun (x : E) => ∫⁻ (y : F) in A, f (x, y) ∂ν

Bombieri–Gubler, Lemma C.3.4: a marginal of a log-concave function over a convex set is log-concave. If f : E × F → ℝ≥0∞ is measurable and log-concave and A ⊆ F is convex and measurable, then x ↦ ∫⁻ y in A, f (x, y) ∂ν is log-concave on E, for any measure ν on F satisfying the Prékopa–Leindler inequality.