ASTIS mathematical exposition

Log-concavity of a two-point difference-quadratic Gibbs shape

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

Statement

On the Cartesian product E×E of a real normed vector space E with itself, let a,b∈ℝ with a≥0. For the potential V=a‖x-y‖²+b, the function exp(−V) is strictly positive and log-concave on the whole product space.

\[V=a\|x-y\|^2+b,\qquad\operatorname{LC}_{E\times E}(e^{-V})\quad(a\ge0).\]

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
a,b : ℝ; ha : 0≤a; no sign condition on b.

{'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. Supply the already-proved convex potential

The corresponding potential theorem establishes convexity of V with exactly the supplied a≥0 and the same unrestricted b.

\[\operatorname{Convex}_{E\times E}(V).\]

Corresponding Lean step

convexOn_univ_const_mul_norm_fst_sub_snd_sq_add (E := E) (a := a) (b := b) ha

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

2. Use exponential positivity and the log identity

The generic convex-potential theorem says exp(−V)>0 and log(exp(−V))=−V. Negating the convex potential gives a concave logarithm, so the theorem applies directly.

\[e^{-V}>0,\qquad\log(e^{-V})=-V\text{ is concave}.\]

Corresponding Lean step

simpa using logConcaveOn_exp_neg_of_convexOn
  (convexOn_univ_const_mul_norm_fst_sub_snd_sq_add (E := E) (a := a) (b := b) ha)

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 · logConcaveOn_exp_neg_pair_sub_quadratic_norm

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. simpa only aligns the specialized formula with the generic Gibbs-shape theorem. The argument is reuse of the convex-potential result, not a new integration or differential calculation.

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_pair_sub_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (ha : 0 ≤ a) :
    LogConcaveOn (Set.univ : Set (E × E))
      (fun z : E × E => Real.exp (-(a * ‖z.1 - z.2‖ ^ 2 + b)))

Exact module and namespace context

Lean proof · logConcaveOn_exp_neg_pair_sub_quadratic_norm

simpa only aligns the specialized formula with the generic Gibbs-shape theorem. The argument is reuse of the convex-potential result, not a new integration or differential calculation.

theorem logConcaveOn_exp_neg_pair_sub_quadratic_norm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (ha : 0 ≤ a) :
    LogConcaveOn (Set.univ : Set (E × E))
      (fun z : E × E => Real.exp (-(a * ‖z.1 - z.2‖ ^ 2 + b))) := by
  simpa using logConcaveOn_exp_neg_of_convexOn
    (convexOn_univ_const_mul_norm_fst_sub_snd_sq_add (E := E) (a := a) (b := b) ha)

/-- Positive multiples of two-point quadratic Gibbs kernel shapes are log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The conclusion is log-concavity of a function shape. No normalizing integral, probability law or executable kernel is constructed.
The word kernel in surrounding names refers to a two-point function, not a ProbabilityTheory.Kernel or a Markov property.
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)

No direct Mathlib call recorded; see the ASTIS 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.
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.