Log-concavity with the explicit quadratic prefactor

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

Statement

Let E be a finite-dimensional real normed vector space and set d=dimℝE; let a,b∈ℝ with a>0. Put V=a‖x‖²+b and Z=exp(−b)(π/a)^(d/2). Then the explicitly scaled function Z⁻¹ exp(−V) is positive log-concave on E. The theorem proves only this shape property; despite the existing declaration's name, it supplies no equality between Z and an integral.

All objects and hypotheses

• E : Type* with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]. There is no inner-product, measurable-space or measure parameter.
• a,b : ℝ; ha : 0<a, with b arbitrary.
• d denotes Module.finrank ℝ E, cast to ℝ in the real exponent d/2. No inner-product structure, measure or volume normalization is a parameter.

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

have hZpos : 0 < Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2) := by
  exact mul_pos (Real.exp_pos _) (Real.rpow_pos_of_pos (div_pos Real.pi_pos ha) _)

ha.le
(inv_pos.mpr hZpos)

exact logConcaveOn_const_mul_exp_neg_quadratic_norm (E := E) (a := a) (b := b)
  ha.le (inv_pos.mpr hZpos)

theorem logConcaveOn_explicit_quadratic_normalized_density
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {a b : ℝ} (ha : 0 < a) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E =>
        (Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2))⁻¹ *
          Real.exp (-(a * ‖x‖ ^ 2 + b)))

theorem logConcaveOn_explicit_quadratic_normalized_density
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {a b : ℝ} (ha : 0 < a) :
    LogConcaveOn (Set.univ : Set E)
      (fun x : E =>
        (Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2))⁻¹ *
          Real.exp (-(a * ‖x‖ ^ 2 + b))) := by
  have hZpos : 0 < Real.exp (-b) * (Real.pi / a) ^ ((Module.finrank ℝ E : ℝ) / 2) := by
    exact mul_pos (Real.exp_pos _) (Real.rpow_pos_of_pos (div_pos Real.pi_pos ha) _)
  exact logConcaveOn_const_mul_exp_neg_quadratic_norm (E := E) (a := a) (b := b)
    ha.le (inv_pos.mpr hZpos)

/-- Shifted nonnegative quadratic norm potentials are convex. -/

Scope and omitted-condition boundaries

• No measure, integral, total mass, or normalized-probability conclusion appears in the actual Lean statement.
• The norm is arbitrary; it is not assumed to be Euclidean. The expression e⁻ᵇ(π/a)^(d/2) is therefore not certified here as a partition function for that norm or for any chosen measure.
• This documentation adds no Lean theorem, compilation evidence, source-equivalence verdict, or new source-fidelity certification.