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

Convexity of a absolute-linear potential

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

Statement

On the real line ℝ, let a,b∈ℝ with a≥0. Then V=a|x|+b is convex on the entire space. There is no sign restriction on b.

\[V=a|x|+b,\qquad\operatorname{Convex}_{ℝ}(V)\quad(a\ge0).\]

All objects and hypotheses

  • The ambient scalar field and state space are ℝ with their usual additive/module structures.
  • a,b : ℝ; ha : 0≤a; b is arbitrary.
  • {'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. Start with the convex base function

The existing absolute-value theorem gives convexity of U(x)=|x| on the whole space.

\[U(\lambda x+\theta y)\le\lambda U(x)+\theta U(y).\]
Corresponding Lean step

convexOn_univ_abs

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

2. Multiply by a nonnegative coefficient

Since a≥0, multiplying the convexity inequality by a preserves its direction. This proves convexity of aU.

\[aU(\lambda x+\theta y)\le\lambda aU(x)+\theta aU(y).\]
Corresponding Lean step

have h := convexOn_univ_abs.smul ha

The .smul API scales an inequality; its nonnegative scalar hypothesis is what preserves the inequality direction.

3. Add the constant offset

Add b to both sides and use λ+θ=1 to distribute b as λb+θb. The result is the convexity inequality for V=aU+b.

\[aU(\lambda x+\theta y)+b\le\lambda(aU(x)+b)+\theta(aU(y)+b).\]
Corresponding Lean step

simpa only [smul_eq_mul] using h.add_const b

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

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. This declaration proves a convexity property of a real-valued potential. Its nonnegative scaling and constant addition is the exact transformation used in the source, rather than a Hessian argument requiring extra smoothness.

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 convexOn_univ_const_mul_abs_add {a b : ℝ} (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set ℝ) (fun x : ℝ => a * |x| + b)

Exact module and namespace context

Lean proof · convexOn_univ_const_mul_abs_add

This declaration proves a convexity property of a real-valued potential. Its nonnegative scaling and constant addition is the exact transformation used in the source, rather than a Hessian argument requiring extra smoothness.

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 convexOn_univ_const_mul_abs_add {a b : ℝ} (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set ℝ) (fun x : ℝ => a * |x| + b) := by
  have h := convexOn_univ_abs.smul ha
  change ConvexOn ℝ Set.univ ((fun x : ℝ => a * |x|) + fun _ => b)
  simpa only [smul_eq_mul] using h.add_const b

/-- The Gibbs shape of a nonnegative absolute-linear real potential is
log-concave. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • Only convexity is established. Coefficient a=0 is allowed; strong convexity, coercivity and integrability do not follow from this result.
  • 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)

  • ConvexOn.smul
  • ConvexOn.add_const
  • smul_eq_mul

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.