Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Absolute value is convex on the real line

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

Read this first

Mathematical 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).\]
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.

Download module (.lean)
theorem convexOn_univ_abs :
    ConvexOn ℝ (Set.univ : Set ℝ) (fun x : ℝ => |x|)

Exact module and namespace context

Proof roadmap

  1. 1Identify 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 ℝ.

  2. 2Reuse 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.

Full assumptions and notation

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 verification

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

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.

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 convexOn_univ_abs :
    ConvexOn ℝ (Set.univ : Set ℝ) (fun x : ℝ => |x|) := by
  change ConvexOn ℝ Set.univ (norm : ℝ → ℝ)
  exact convexOn_univ_norm

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.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • convexOn_univ_norm

    Mathematical sources

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