/- 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.