ASTIS mathematical exposition

Sublevel sets of the negative-log potential are convex

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

Statement

Let E be a real module, f:E→ℝ positive log-concave on s⊆E, and r∈ℝ any threshold. The set of x∈s with −log f(x)≤r is convex.

\[\operatorname{LC}_s(f)\Longrightarrow\{x\in s:-\log f(x)\le r\}\text{ is convex}\quad(r\in\mathbb R).\]

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.
r : ℝ is arbitrary, with no sign restriction.

{'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

1. Use the convex negative-log potential

The preceding result gives a convex function V=−log f on s.

\[V(ax+by)\le aV(x)+bV(y).\]

Corresponding Lean step

hf.convexOn_neg_log

The identifiers refer to the assumptions or previously proved facts described in this step; the full original proof below supplies their exact context.

2. Bound a convex combination of two sublevel points

If V(x),V(y)≤r and a,b≥0 sum to one, then their weighted potential bound is at most ar+br=r. Convexity of s keeps the combination in s. This is precisely the sublevel-set theorem bundled as quasiconvexity.

\[V(ax+by)\le aV(x)+bV(y)\le ar+br=r.\]

Corresponding Lean step

hf.convexOn_neg_log.quasiconvexOn r

The identifiers refer to the assumptions or previously proved facts described in this step; the full original proof below supplies their exact context.

Lean statement · convex_sublevel_neg_log

Braces name inputs Lean can infer, and bracketed classes state the ambient structures listed above. The assumptions before the final colon are inputs; the expression after it is the exact property this declaration establishes. quasiconvexOn says every sublevel set is convex. Applying it to r selects the desired set.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem LogConcaveOn.convex_sublevel_neg_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (r : ℝ) :
    Convex ℝ {x ∈ s | - Real.log (f x) ≤ r}

Exact module and namespace context

Lean proof · convex_sublevel_neg_log

quasiconvexOn says every sublevel set is convex. Applying it to r selects the desired set.

theorem LogConcaveOn.convex_sublevel_neg_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) (r : ℝ) :
    Convex ℝ {x ∈ s | - Real.log (f x) ≤ r} :=
  hf.convexOn_neg_log.quasiconvexOn r

Exact module and namespace context

Scope and omitted-condition boundaries

The set is restricted to s; no claim about sublevels outside the given domain.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn.convexOn_neg_log

Mathlib API called (external library)

ConvexOn.quasiconvexOn

Mathematical sources

Existing ASTIS declaration and exact proof — Directly read current local source; no Lean edit or fresh build.
Existing curated module card — Local API/source-boundary memory; not independent primary textbook verification.
ConvexOn.quasiconvexOn — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.