A quadratic envelope from one midpoint

1. At \(m=(x_0+x)/2\), strong convexity gives \[V(m)\le\tfrac12V(x_0)+\tfrac12V(x)-\tfrac k8\|x-x_0\|^2.\] The factor \(k/8\) comes from \((k/2)(1/2)(1/2)\).

2. Global minimality gives \(V(x_0)\le V(m)\). Combine the two inequalities and multiply by 2 to obtain \(V(x_0)+\tfrac k4\|x-x_0\|^2\le V(x)\). No derivative or limit was used.

3. This midpoint calculation proves the k/4 envelope, not the sharper k/2 constant. Obtaining a sharper result needs another argument; it must not be credited to this calculation.

4. The envelope alone is not a normalization theorem. One sufficient route assumes \(k>0\), a finite-dimensional Euclidean space with Lebesgue reference measure and measurable V, then compares \(exp(-V)\) with an integrable Gaussian and separately checks positivity of the normalizer. These are conditions for that route, not necessary conditions for every Gibbs normalization: on \(\mathbb{R}\), V(x)=|x| is convex with \(k=0\) and \(exp(-|x|)\) has integral 2.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity
import Mathlib.Analysis.Convex.Strong

open Set

example
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {V : E → ℝ} {k : ℝ} (hV : StrongConvexOn (Set.univ : Set E) k V)
    (x₀ : E) (hx₀ : IsMinOn V (Set.univ : Set E) x₀) :
    ∀ x : E, V x₀ + (k / 4) * ‖x - x₀‖ ^ 2 ≤ V x := by
  intro x
  have hx₀_min : ∀ y : E, V x₀ ≤ V y := isMinOn_univ_iff.mp hx₀
  have hmid_min : V x₀ ≤ V ((1 / 2 : ℝ) • x₀ + (1 / 2 : ℝ) • x) := hx₀_min _
  have hstrong :=
    hV.2 (by simp : x₀ ∈ (Set.univ : Set E)) (by simp : x ∈ (Set.univ : Set E))
      (by norm_num : 0 ≤ (1 / 2 : ℝ)) (by norm_num : 0 ≤ (1 / 2 : ℝ))
      (by norm_num : (1 / 2 : ℝ) + (1 / 2 : ℝ) = 1)
  have hstrong' :
      V ((1 / 2 : ℝ) • x₀ + (1 / 2 : ℝ) • x) ≤
        (1 / 2 : ℝ) * V x₀ + (1 / 2 : ℝ) * V x - (k / 8) * ‖x - x₀‖ ^ 2 := by
    rw [norm_sub_rev x₀ x] at hstrong
    convert hstrong using 1
    · simp [smul_eq_mul]
      ring_nf
  have hle := hmid_min.trans hstrong'
  nlinarith

1. States the convention and obtains the midpoint correction k/8 exactly. (1 point)
2. Uses the exposed global minimizer at the midpoint. (1 point)
3. Rearranges to k/4 without silently upgrading it to k/2 or assuming differentiability. (1 point)
4. Separates the quadratic envelope from Gibbs integrability and normalization. (1 point)

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity
import Mathlib.Analysis.Convex.Strong

open Set

example
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {V : E → ℝ} {k : ℝ} (hV : StrongConvexOn (Set.univ : Set E) k V)
    (x₀ : E) (hx₀ : IsMinOn V (Set.univ : Set E) x₀) :
    ∀ x : E, V x₀ + (k / 4) * ‖x - x₀‖ ^ 2 ≤ V x := by
  -- Replace this comment with your proof.

Download task template

StrongConvexOn contains a convex-domain component and a two-point inequality; hV.2 selects the latter. IsMinOn on univ is expanded to compare the minimizer with every point. The midpoint coefficients are checked by norm_num, the squared distance is rewritten symmetrically, and nlinarith performs the final scalar rearrangement.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity
import Mathlib.Analysis.Convex.Strong

open Set

example
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {V : E → ℝ} {k : ℝ} (hV : StrongConvexOn (Set.univ : Set E) k V)
    (x₀ : E) (hx₀ : IsMinOn V (Set.univ : Set E) x₀) :
    ∀ x : E, V x₀ + (k / 4) * ‖x - x₀‖ ^ 2 ≤ V x := by
  intro x
  have hx₀_min : ∀ y : E, V x₀ ≤ V y := isMinOn_univ_iff.mp hx₀
  have hmid_min : V x₀ ≤ V ((1 / 2 : ℝ) • x₀ + (1 / 2 : ℝ) • x) := hx₀_min _
  have hstrong :=
    hV.2 (by simp : x₀ ∈ (Set.univ : Set E)) (by simp : x ∈ (Set.univ : Set E))
      (by norm_num : 0 ≤ (1 / 2 : ℝ)) (by norm_num : 0 ≤ (1 / 2 : ℝ))
      (by norm_num : (1 / 2 : ℝ) + (1 / 2 : ℝ) = 1)
  have hstrong' :
      V ((1 / 2 : ℝ) • x₀ + (1 / 2 : ℝ) • x) ≤
        (1 / 2 : ℝ) * V x₀ + (1 / 2 : ℝ) * V x - (k / 8) * ‖x - x₀‖ ^ 2 := by
    rw [norm_sub_rev x₀ x] at hstrong
    convert hstrong using 1
    · simp [smul_eq_mul]
      ring_nf
  have hle := hmid_min.trans hstrong'
  nlinarith

Download runnable reference