Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

StrongConvexMinimizer: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. A positive strongly convex potential attains its minimum
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

  1. 1Expose quadratic growth

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

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

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

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

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 := 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

Mathlib API called (external library)

  • isCompact_closedBall
  • IsCompact.exists_isMinOn
  • abs_real_inner_le_norm
  • IsLocalMin.fderiv_eq_zero

Mathematical sources

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