ASTIS mathematical exposition

Absolute value is convex on the real line

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

Statement

The function x↦|x| is convex on all of ℝ: for any real x,y and any nonnegative real weights λ,θ summing to one, |λx+θy|≤λ|x|+θ|y|.

\[\operatorname{Convex}_{\mathbb R}(x\mapsto|x|),\qquad|\lambda x+\theta y|\le\lambda|x|+\theta|y|\quad(\lambda,\theta\ge0,\ \lambda+\theta=1).\]

All objects and hypotheses

The ambient scalar field and state space are ℝ with their usual additive/module structures.
There are no explicit parameters or hypotheses; the ambient space and scalars are ℝ.

{'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. Identify absolute value with the real norm

For a real number, its norm is its absolute value. Thus the requested function is exactly the norm on the real normed vector space ℝ.

\[|x|=\|x\|_{\mathbb R}.\]

Corresponding Lean step

change ConvexOn ℝ Set.univ (norm : ℝ → ℝ)

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

2. Reuse norm convexity

The norm triangle inequality and homogeneity give ‖λx+θy‖≤‖λx‖+‖θy‖=λ‖x‖+θ‖y‖ for nonnegative weights. The whole real line is convex, so Mathlib's norm-convexity theorem proves the result.

\[|\lambda x+\theta y|\le|\lambda x|+|\theta y|=\lambda|x|+\theta|y|.\]

Corresponding Lean step

exact convexOn_univ_norm

The final call supplies the named existing result after matching its parameters with this statement.

Lean statement · convexOn_univ_abs

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. change only rewrites the real absolute-value function as the equal norm function. The existing norm theorem supplies the complete convexity proof.

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_abs :
    ConvexOn ℝ (Set.univ : Set ℝ) (fun x : ℝ => |x|)

Exact module and namespace context

Lean proof · convexOn_univ_abs

change only rewrites the real absolute-value function as the equal norm function. The existing norm theorem supplies the complete convexity proof.

theorem convexOn_univ_abs :
    ConvexOn ℝ (Set.univ : Set ℝ) (fun x : ℝ => |x|) := by
  change ConvexOn ℝ Set.univ (norm : ℝ → ℝ)
  exact convexOn_univ_norm

/-- Nonnegative absolute-linear real potentials are convex. -/

Exact module and namespace context

Scope and omitted-condition boundaries

This is convexity, not differentiability at the origin or strict convexity.
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_univ_norm

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