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

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.convex_superlevel · theorem · Teaching coverage

Statement

Let E be a real module, f:E→ℝ positive log-concave on s⊆E, and c∈ℝ. Then S_c={x∈s:c≤f(x)} is convex. No positivity assumption on c is needed.

All objects and hypotheses

• E : Type* with [AddCommMonoid E] and [Module ℝ E]. These are the exact algebraic ambient structures; no topology, norm, measure or finite-dimensionality is assumed.
• s : Set E, f : E → ℝ, hf : LogConcaveOn s f.
• c : ℝ arbitrary. In the proof x,y∈S_c and a,b≥0 with a+b=1; set z=ax+by.

• {'term': 'Positive log-concavity', 'text': 'LC_s(f) means strict positivity of f at every point of s and concavity of log f on the convex domain s. No zero-valued points are included in this convention.', 'formula': '\\operatorname{LC}_s(f)\\iff(\\forall x\\in s,\\ f(x)>0)\\land\\operatorname{Concave}_s(\\log f).'}
• {'term': 'Convex combinations and Jensen inequalities', 'text': 'Throughout, x,y lie in the stated domain; λ,θ are nonnegative real weights with λ+θ=1. The Lean code often names these weights a,b, independently of the a,b coefficients in specialized potentials.', 'formula': 'z=\\lambda x+\\theta y,\\quad \\lambda,\\theta\\ge0,\\quad\\lambda+\\theta=1;\\qquad V(z)\\le\\lambda V(x)+\\theta V(y)\\text{ for convex }V.'}
• {'term': 'Geometry, not probability normalization', 'text': 'The module proves shapes and convexity properties of real-valued functions. It has no reference measure in its declarations. In particular, names containing normalized_density do not themselves prove normalization, and the quadratic prefactor is not certified as the integral of an arbitrary norm-based shape.', 'formula': '\\operatorname{LC}(Z^{-1}e^{-V})\\quad\\text{does not assert}\\quad Z=\\int e^{-V}\\,d\\mu\\quad\\text{or}\\quad \\int Z^{-1}e^{-V}\\,d\\mu=1.'}

Mathematical proof

by_cases hc : c ≤ 0
· intro x hx y hy a b ha hb hab
  have hmid_s := hf.convex_domain hx.1 hy.1 ha hb hab
  exact ⟨hmid_s, le_of_lt (lt_of_le_of_lt hc (hf.pos (x := a • x + b • y) hmid_s))⟩

have hcpos : 0 < c := lt_of_not_ge hc
have hmid_s := hf.convex_domain hx.1 hy.1 ha hb hab
have hlogx := Real.log_le_log hcpos hx.2
have hlogy := Real.log_le_log hcpos hy.2

have hweighted := add_le_add (mul_le_mul_of_nonneg_left hlogx ha) (mul_le_mul_of_nonneg_left hlogy hb)
-- hconst uses a+b=1; hfloor rewrites this weighted bound.

have hconc : a * Real.log (f x) + b * Real.log (f y) ≤ Real.log (f (a • x + b • y)) := by
  simpa [smul_eq_mul] using hf.concaveOn_log.2 hx.1 hy.1 ha hb hab

theorem LogConcaveOn.convex_superlevel {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (c : ℝ) :
    Convex ℝ {x ∈ s | c ≤ f x}

theorem LogConcaveOn.convex_superlevel {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (c : ℝ) :
    Convex ℝ {x ∈ s | c ≤ f x} := by
  by_cases hc : c ≤ 0
  · intro x hx y hy a b ha hb hab
    have hmid_s := hf.convex_domain hx.1 hy.1 ha hb hab
    exact ⟨hmid_s, le_of_lt (lt_of_le_of_lt hc (hf.pos (x := a • x + b • y) hmid_s))⟩
  · have hcpos : 0 < c := lt_of_not_ge hc
    intro x hx y hy a b ha hb hab
    have hmid_s := hf.convex_domain hx.1 hy.1 ha hb hab
    refine ⟨hmid_s, ?_⟩
    have hlogx : Real.log c ≤ Real.log (f x) :=
      Real.log_le_log hcpos hx.2
    have hlogy : Real.log c ≤ Real.log (f y) :=
      Real.log_le_log hcpos hy.2
    have hweighted :
        a * Real.log c + b * Real.log c ≤
          a * Real.log (f x) + b * Real.log (f y) :=
      add_le_add (mul_le_mul_of_nonneg_left hlogx ha) (mul_le_mul_of_nonneg_left hlogy hb)
    have hconst : a * Real.log c + b * Real.log c = Real.log c := by
      calc
        a * Real.log c + b * Real.log c = (a + b) * Real.log c := by ring
        _ = Real.log c := by rw [hab]; ring
    have hfloor : Real.log c ≤ a * Real.log (f x) + b * Real.log (f y) := by
      simpa [hconst] using hweighted
    have hconc :
        a * Real.log (f x) + b * Real.log (f y) ≤
          Real.log (f (a • x + b • y)) := by
      simpa [smul_eq_mul] using hf.concaveOn_log.2 hx.1 hy.1 ha hb hab
    exact (Real.log_le_log_iff hcpos (hf.pos (x := a • x + b • y) hmid_s)).mp
      (hfloor.trans hconc)

/-- Positive log-concave functions are quasiconcave: all superlevel sets are convex. -/

Scope and omitted-condition boundaries

• This is non-strict convexity of domain-restricted superlevels; no strict concavity, boundedness or compactness is asserted.
• This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.