Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

A convex potential gives a log-concave Gibbs shape

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

Statement

Let E be a real module, s⊆E, and V:E→ℝ convex on s. Then x↦exp(−V(x)) is positive log-concave on s.

\[\operatorname{Convex}_s(V)\Longrightarrow\operatorname{LC}_s(e^{-V}),\qquad\log(e^{-V(x)})=-V(x).\]

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, V : E → ℝ, hV : ConvexOn ℝ s V; this includes convexity of s.
  • {'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. Exponential values are strictly positive

The real exponential is positive at every real argument, so exp(−V(x)) is positive on s without any lower or upper bound on V.

\[\exp(-V(x))>0.\]
Corresponding Lean step

refine ⟨fun _ _ => Real.exp_pos _, ?_⟩

The two components requested here are the exact clauses of the predicate, not extra hypotheses.

2. Identify the logarithm and negate convexity

Negating the convexity inequality for V makes −V concave. Since log(exp(−V(x)))=−V(x), this is exactly concavity of the logarithm of the Gibbs shape.

\[V(ax+by)\le aV(x)+bV(y)\Longrightarrow a[-V(x)]+b[-V(y)]\le -V(ax+by)=\log(e^{-V(ax+by)}).\]
Corresponding Lean step

exact hV.neg.congr fun _ _ => by simp

The congr operation transfers the geometric property to a function equal on the domain; all needed log identities are justified at positive arguments.

Lean statement · logConcaveOn_exp_neg_of_convexOn

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. hV.neg reuses the sign-reversal theorem; congr replaces equal functions on s, using log_exp. The exponential is a shape function, not yet a probability density.

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_exp_neg_of_convexOn {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {V : E → ℝ} (hV : ConvexOn ℝ s V) :
    LogConcaveOn s (fun x => Real.exp (-V x))

Exact module and namespace context

Lean proof · logConcaveOn_exp_neg_of_convexOn

hV.neg reuses the sign-reversal theorem; congr replaces equal functions on s, using log_exp. The exponential is a shape function, not yet a probability density.

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_exp_neg_of_convexOn {E : Type*} [AddCommMonoid E] [Module ℝ E]
    {s : Set E} {V : E → ℝ} (hV : ConvexOn ℝ s V) :
    LogConcaveOn s (fun x => Real.exp (-V x)) := by
  refine ⟨fun _ _ => Real.exp_pos _, ?_⟩
  exact hV.neg.congr fun _ _ => by simp

/-- A positive multiple of the Gibbs shape of a convex potential is
log-concave.  This is the convex-analytic part of normalized Gibbs-density
bookkeeping; the measure/integral normalization proof is a separate leaf. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • Integrability, a positive finite partition function, normalization and sampling are not conclusions.
  • This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • Real.exp_pos
  • ConvexOn.neg
  • ConcaveOn.congr
  • Real.log_exp

Mathematical sources

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