Convexity of a shifted quadratic-norm potential

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

Statement

On a real normed vector space E, let a,b∈ℝ with a≥0 and fix m∈E. Then V=a‖x-m‖²+b is convex on the entire space. There is no sign restriction on b.

All objects and hypotheses

• E : Type* with [NormedAddCommGroup E] and [NormedSpace ℝ E]. No finite-dimensionality, completeness or inner-product structure is required.
• a,b : ℝ; ha : 0≤a; b is arbitrary.
• m : E is an arbitrary fixed center.

• {'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

let shift : E →ᵃ[ℝ] E :=
  { toFun := fun x => x - m
    linear := LinearMap.id
    map_vadd' := by intro p v; simp [sub_eq_add_neg, add_assoc] }

have h := (convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha).comp_affineMap shift
change ConvexOn ℝ Set.univ ((fun x : E => a * ‖x‖ ^ 2 + b) ∘ shift)
exact h

theorem convexOn_univ_const_mul_norm_sub_sq_add
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (m : E) (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => a * ‖x - m‖ ^ 2 + b)

theorem convexOn_univ_const_mul_norm_sub_sq_add
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {a b : ℝ} (m : E) (ha : 0 ≤ a) :
    ConvexOn ℝ (Set.univ : Set E) (fun x : E => a * ‖x - m‖ ^ 2 + b) := by
  let shift : E →ᵃ[ℝ] E :=
    { toFun := fun x => x - m
      linear := LinearMap.id
      map_vadd' := by
        intro p v
        simp [sub_eq_add_neg, add_assoc] }
  have h :=
    (convexOn_univ_const_mul_norm_sq_add (E := E) (a := a) (b := b) ha).comp_affineMap
      shift
  change ConvexOn ℝ Set.univ
    ((fun x : E => a * ‖x‖ ^ 2 + b) ∘ shift)
  exact h

/-- The Gibbs shape of a shifted nonnegative quadratic norm potential is log-concave. -/

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.