Samplinglib mathematical lesson

Read the concavity of the logarithm

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

Read this first

Mathematical statement

Let E be a real module and f:E→ℝ positive log-concave on s⊆E. Then x↦log f(x) is concave on s, including convexity of the domain.

\[\operatorname{LC}_s(f)\Longrightarrow\operatorname{Concave}_s(\log f).\]

Lean statement · concaveOn_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. hf.2 projects the second half of the definition. ConcaveOn itself records both the domain and its Jensen inequality.

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.

Download module (.lean)

theorem LogConcaveOn.concaveOn_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) :
    ConcaveOn ℝ s (fun x => Real.log (f x))

Exact module and namespace context

Proof roadmap

1Extract the second defining clause
The second component of positive log-concavity is already the requested concavity statement. Return it unchanged.

Full assumptions and notation

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.

{'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. Extract the second defining clause

The second component of positive log-concavity is already the requested concavity statement. Return it unchanged.

\[a\log f(x)+b\log f(y)\le\log f(ax+by)\quad(x,y\in s,\ a,b\ge0,\ a+b=1).\]

Corresponding Lean step

hf.2

The .2 field is the concavity component already stored in the supplied hypothesis.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · concaveOn_log

hf.2 projects the second half of the definition. ConcaveOn itself records both the domain and its Jensen inequality.

Download module (.lean)

theorem LogConcaveOn.concaveOn_log {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ}
    (hf : LogConcaveOn s f) :
    ConcaveOn ℝ s (fun x => Real.log (f x)) :=
  hf.2

Exact module and namespace context

Scope and omitted-condition boundaries

Projection only; no new concavity theorem is proved.
This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.LogConcaveOn

Mathlib API called (external library)

ConcaveOn

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.
ConcaveOn — Exact inspected Mathlib definition or theorem used by this exposition.

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