Samplinglib mathematical lesson

Squared norms are convex on real normed spaces

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

Read this first

Mathematical statement

Let E be any real normed vector space; finite dimension, completeness, an inner product and strict convexity of the norm are not assumed. Then x↦‖x‖² is convex on all of E.

\[\|\lambda x+\theta y\|^2\le\lambda\|x\|^2+\theta\|y\|^2\qquad(x,y\in E,\ \lambda,\theta\ge0,\ \lambda+\theta=1).\]

Lean statement · convexOn_univ_norm_sq

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. The Lean proof uses a and b for the weights called λ and θ here. hnorm, hsq and hjensen are the three successive numerical bounds. nlinarith checks the scalar identity under a+b=1; the mathematical reason is the nonnegative term ab(‖x‖−‖y‖)².

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_norm_sq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => ‖x‖ ^ 2)

Exact module and namespace context

Proof roadmap

1The whole domain is convex
The domain is E itself, so every convex combination stays in it. Only the function inequality remains.
2Bound the norm of a convex combination
Use the triangle inequality followed by norm homogeneity. Nonnegative weights have absolute value equal to themselves, yielding an upper bound L=λ‖x‖+θ‖y‖.
3Square the inequality using nonnegativity
Both the norm and L are nonnegative. Squaring is order-preserving on nonnegative reals, so the squared norm is at most L².
4Bound the square of the scalar weighted average
With u=‖x‖ and v=‖y‖, the condition λ+θ=1 gives an exact difference identity. Its right side is nonnegative, so L²≤λu²+θv². The code proves this identity algebraically; it does not assume convexity of the squared norm being established.
5Combine the two bounds
Transitivity of the squared-norm bound and the scalar weighted-square bound gives precisely the convexity inequality.

Full assumptions and notation

All objects and hypotheses

E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
No hypotheses besides the ambient normed real vector-space structures. The proof considers arbitrary x,y and λ,θ≥0 with λ+θ=1.

{'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. The whole domain is convex

The domain is E itself, so every convex combination stays in it. Only the function inequality remains.

\[\lambda x+\theta y\in E.\]

Corresponding Lean step

refine ⟨convex_univ, ?_⟩
intro x _ y _ a b ha hb hab

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

2. Bound the norm of a convex combination

Use the triangle inequality followed by norm homogeneity. Nonnegative weights have absolute value equal to themselves, yielding an upper bound L=λ‖x‖+θ‖y‖.

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

Corresponding Lean step

have hnorm : ‖a • x + b • y‖ ≤ a * ‖x‖ + b * ‖y‖ := by
  calc
    ‖a • x + b • y‖ ≤ ‖a • x‖ + ‖b • y‖ := norm_add_le _ _
    _ = a * ‖x‖ + b * ‖y‖ := by
      rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]

The rewrites identify equal expressions in the displayed mathematical calculation; they do not introduce extra assumptions.

3. Square the inequality using nonnegativity

Both the norm and L are nonnegative. Squaring is order-preserving on nonnegative reals, so the squared norm is at most L².

\[0\le\|\lambda x+\theta y\|\le L\Longrightarrow\|\lambda x+\theta y\|^2\le L^2.\]

Corresponding Lean step

have hnonneg := add_nonneg (mul_nonneg ha (norm_nonneg _)) (mul_nonneg hb (norm_nonneg _))
have hsq := (sq_le_sq₀ (norm_nonneg _) hnonneg).2 hnorm

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

4. Bound the square of the scalar weighted average

With u=‖x‖ and v=‖y‖, the condition λ+θ=1 gives an exact difference identity. Its right side is nonnegative, so L²≤λu²+θv². The code proves this identity algebraically; it does not assume convexity of the squared norm being established.

\[\lambda u^2+\theta v^2-(\lambda u+\theta v)^2=\lambda\theta(u-v)^2\ge0.\]

Corresponding Lean step

have hdiff_nonneg := mul_nonneg (mul_nonneg ha hb) (sq_nonneg (‖x‖ - ‖y‖))
-- hident proves the displayed equality by nlinarith [hab]; hjensen follows by nlinarith.

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

5. Combine the two bounds

Transitivity of the squared-norm bound and the scalar weighted-square bound gives precisely the convexity inequality.

\[\|\lambda x+\theta y\|^2\le L^2\le\lambda\|x\|^2+\theta\|y\|^2.\]

Corresponding Lean step

exact hsq.trans hjensen

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_norm_sq

The Lean proof uses a and b for the weights called λ and θ here. hnorm, hsq and hjensen are the three successive numerical bounds. nlinarith checks the scalar identity under a+b=1; the mathematical reason is the nonnegative term ab(‖x‖−‖y‖)².

Download module (.lean)

theorem convexOn_univ_norm_sq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => ‖x‖ ^ 2) := by
  refine ⟨convex_univ, ?_⟩
  intro x _ y _ a b ha hb hab
  have hnorm : ‖a • x + b • y‖ ≤ a * ‖x‖ + b * ‖y‖ := by
    calc
      ‖a • x + b • y‖ ≤ ‖a • x‖ + ‖b • y‖ := norm_add_le _ _
      _ = a * ‖x‖ + b * ‖y‖ := by
        rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]
  have hnonneg : 0 ≤ a * ‖x‖ + b * ‖y‖ :=
    add_nonneg (mul_nonneg ha (norm_nonneg _)) (mul_nonneg hb (norm_nonneg _))
  have hsq : ‖a • x + b • y‖ ^ 2 ≤ (a * ‖x‖ + b * ‖y‖) ^ 2 := by
    exact (sq_le_sq₀ (norm_nonneg _) hnonneg).2 hnorm
  have hjensen : (a * ‖x‖ + b * ‖y‖) ^ 2 ≤ a * ‖x‖ ^ 2 + b * ‖y‖ ^ 2 := by
    have hdiff_nonneg : 0 ≤ a * b * (‖x‖ - ‖y‖) ^ 2 := by
      exact mul_nonneg (mul_nonneg ha hb) (sq_nonneg _)
    have hident :
        a * ‖x‖ ^ 2 + b * ‖y‖ ^ 2 - (a * ‖x‖ + b * ‖y‖) ^ 2 =
          a * b * (‖x‖ - ‖y‖) ^ 2 := by
      nlinarith [hab]
    nlinarith
  exact hsq.trans hjensen

Exact module and namespace context

Scope and omitted-condition boundaries

No strict or strong convexity is concluded. A general norm need not arise from an inner product.
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)

convex_univ
norm_add_le
norm_smul
Real.norm_of_nonneg
norm_nonneg
add_nonneg
mul_nonneg
sq_le_sq₀
sq_nonneg

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.
norm_smul — Exact inspected Mathlib definition or theorem used by this exposition.
Real.norm_of_nonneg — Exact inspected Mathlib definition or theorem used by this exposition.
sq_le_sq₀ — Exact inspected Mathlib definition or theorem used by this exposition.
Existing usage in Tests.Basic — Read-only source example; no test was run.
convex_univ — Exact local Mathlib declaration anchor.

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