Samplinglib mathematical lesson

A positive strongly convex potential attains its minimum

AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexMinimizer.exists_isMinOn_and_gradient_eq_zero · theorem · Teaching coverage

Read this first

Mathematical statement

There is a point p that minimizes V globally, and the genuine gradient of V vanishes at p.

\[\exists p\in E:\quad V(p)\le V(x)\ \forall x\in E,\qquad \nabla V(p)=0.\]

Lean statement · exists_isMinOn_and_gradient_eq_zero

The theorem requires positive modulus and finite dimension. It uses Differentiable rather than a totalized fderiv equality as its regularity witness.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem exists_isMinOn_and_gradient_eq_zero
    {V : E → ℝ} {m : ℝ} (hm : 0 < m)
    (hV : Differentiable ℝ V)
    (hsc : StrongConvexOn (Set.univ : Set E) m V) :
    ∃ p : E, IsMinOn V Set.univ p ∧ gradient V p = 0

Exact module and namespace context

Proof roadmap

1Expose quadratic growth
Apply the compiled first-order model at the origin. The linear gradient term is the only possible negative contribution.
2Choose a compact search ball
Cauchy-Schwarz shows that outside radius two times the origin-gradient norm divided by m, the quadratic term absorbs the linear term.
3Attain the global minimum
The closed ball of radius R is compact in finite dimension. Continuity gives a minimizer p in the ball. Its value is no larger than V(0), while every point outside has value at least V(0), so p is globally minimizing.
4Use Fermat's theorem
A differentiable function has zero derivative at a local minimum; in an inner-product space this is exactly zero gradient.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space.
V is genuinely differentiable on all of E.
V is strongly convex on all of E with strictly positive modulus m.

Mathematical proof

1. Expose quadratic growth

Apply the compiled first-order model at the origin. The linear gradient term is the only possible negative contribution.

\[V(x)\ge V(0)+\langle\nabla V(0),x\rangle+\frac m2\|x\|^2.\]

Corresponding Lean step

StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn supplies the inequality from genuine differentiability.

2. Choose a compact search ball

Cauchy-Schwarz shows that outside radius two times the origin-gradient norm divided by m, the quadratic term absorbs the linear term.

\[R=\frac{2\|\nabla V(0)\|}{m},\quad \|x\|>R\Longrightarrow V(x)\ge V(0).\]

Corresponding Lean step

abs_real_inner_le_norm and positivity justify the comparison without dividing by a possibly zero norm.

3. Attain the global minimum

The closed ball of radius R is compact in finite dimension. Continuity gives a minimizer p in the ball. Its value is no larger than V(0), while every point outside has value at least V(0), so p is globally minimizing.

\[p\in\overline B(0,R),\quad V(p)\le V(0)\le V(x)\quad(x\notin\overline B(0,R)).\]

Corresponding Lean step

isCompact_closedBall.exists_isMinOn supplies p; a ball-membership split promotes the restricted minimum to Set.univ.

4. Use Fermat's theorem

A differentiable function has zero derivative at a local minimum; in an inner-product space this is exactly zero gradient.

\[DV(p)=0\quad\Longleftrightarrow\quad\nabla V(p)=0.\]

Corresponding Lean step

IsLocalMin.fderiv_eq_zero closes the genuine first-order condition.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · exists_isMinOn_and_gradient_eq_zero

The Lean proof implements the coercive-ball argument directly, reusing the ASTIS first-order strong-convexity theorem and Mathlib compactness/Fermat APIs.

Download module (.lean)

theorem exists_isMinOn_and_gradient_eq_zero
    {V : E → ℝ} {m : ℝ} (hm : 0 < m)
    (hV : Differentiable ℝ V)
    (hsc : StrongConvexOn (Set.univ : Set E) m V) :
    ∃ p : E, IsMinOn V Set.univ p ∧ gradient V p = 0 := by
  let g : E := gradient V 0
  let R : ℝ := 2 * ‖g‖ / m
  have hR : 0 ≤ R := by
    dsimp only [R]
    positivity
  have hfirst (x : E) :
      V 0 + inner ℝ g x + m / 2 * ‖x‖ ^ 2 ≤ V x := by
    simpa only [g, sub_zero] using
      StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn hsc
        (fun z _ ↦ (hV z).hasGradientAt) (x := 0) (y := x)
        (Set.mem_univ _) (Set.mem_univ _)
  have houtside {x : E} (hx : R < ‖x‖) : V 0 ≤ V x := by
    have hxpos : 0 < ‖x‖ := lt_of_le_of_lt hR hx
    have hscale : 2 * ‖g‖ < m * ‖x‖ := by
      dsimp only [R] at hx
      have hs := (div_lt_iff₀ hm).mp hx
      simpa [mul_comm] using hs
    have hinner : -(‖g‖ * ‖x‖) ≤ inner ℝ g x :=
      (abs_le.mp (abs_real_inner_le_norm g x)).1
    have hquad : ‖g‖ * ‖x‖ ≤ m / 2 * ‖x‖ ^ 2 := by
      nlinarith [mul_pos hm hxpos]
    linarith [hfirst x]
  have hzero : (0 : E) ∈ closedBall 0 R := by
    simp [hR]
  obtain ⟨p, hpBall, hpMinBall⟩ :=
    (isCompact_closedBall (0 : E) R).exists_isMinOn
      ⟨0, hzero⟩ hV.continuous.continuousOn
  have hpMin : IsMinOn V Set.univ p := by
    intro x _
    by_cases hxBall : x ∈ closedBall (0 : E) R
    · exact hpMinBall hxBall
    · have hx : R < ‖x‖ := by
        simpa [mem_closedBall, dist_eq_norm] using hxBall
      exact (hpMinBall hzero).trans (houtside hx)
  refine ⟨p, hpMin, ?_⟩
  simp [gradient, (hpMin.isLocalMin Filter.univ_mem).fderiv_eq_zero]

end AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexMinimizer

Exact module and namespace context

Scope and omitted-condition boundaries

This is a finite-dimensional existence and first-order optimality theorem. It does not normalize a Gibbs law, prove concentration, or construct a sampling algorithm.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn

Mathlib API called (external library)

isCompact_closedBall
IsCompact.exists_isMinOn
abs_real_inner_le_norm
IsLocalMin.fderiv_eq_zero

Mathematical sources

Smoothed Picard Hamiltonian Monte Carlo, Lemma 4.16 proof, PDF p.22 — ASTIS expands the omitted existence justification for the minimizer selected in the proof.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.