Samplinglib mathematical lesson

Unpack the definition of positive log-concavity

AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity.logConcaveOn_iff · theorem · Teaching coverage

Read this first

Mathematical statement

For any real module E, set s⊆E and function f:E→ℝ, positive log-concavity on s is equivalent to strict positivity of f on s together with concavity of its logarithm on s.

\[\operatorname{LC}_s(f)\iff(\forall x\in s,\ 0<f(x))\land\operatorname{Concave}_s(\log f).\]

Lean statement · logConcaveOn_iff

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. ↔ asks for equivalence in both directions. Iff.rfl proves it because expanding the definition gives literally the same proposition.

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_iff {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ} :
    LogConcaveOn s f ↔
      (∀ x ∈ s, 0 < f x) ∧ ConcaveOn ℝ s (fun x => Real.log (f x))

Exact module and namespace context

Proof roadmap

1Expand the named predicate
The left side was defined to be exactly the conjunction on the right. Therefore both directions are the identity implication; no analytical argument or new log-concavity criterion is added.

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 → ℝ; no additional hypothesis.

{'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. Expand the named predicate

The left side was defined to be exactly the conjunction on the right. Therefore both directions are the identity implication; no analytical argument or new log-concavity criterion is added.

\[\operatorname{LC}_s(f)=(\text{positivity on }s)\land(\text{concavity of }\log f\text{ on }s).\]

Corresponding Lean step

Iff.rfl

Iff.rfl is reflexivity of an equivalence after expanding a definition.

Lean verification

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

Lean proof · logConcaveOn_iff

↔ asks for equivalence in both directions. Iff.rfl proves it because expanding the definition gives literally the same proposition.

Download module (.lean)

theorem logConcaveOn_iff {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {f : E → ℝ} :
    LogConcaveOn s f ↔
      (∀ x ∈ s, 0 < f x) ∧ ConcaveOn ℝ s (fun x => Real.log (f x)) :=
  Iff.rfl

Exact module and namespace context

Scope and omitted-condition boundaries

Definition-level interface only; not a new mathematical characterization by geometric means or densities.
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)

No direct Mathlib call recorded; see the Samplinglib parents.

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.

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