Squared norms are convex on real normed spaces

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

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.

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

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 := add_nonneg (mul_nonneg ha (norm_nonneg _)) (mul_nonneg hb (norm_nonneg _))
have hsq := (sq_le_sq₀ (norm_nonneg _) hnonneg).2 hnorm

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.

theorem convexOn_univ_norm_sq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => ‖x‖ ^ 2)

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

/-- Nonnegative quadratic norm potentials are convex. -/

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.