Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. ASTIS supplies the omitted finite-dimensional minimizer argument and composes it with the q=2 proof edge.
In the proof of Lemma 4.16 the authors select a minimizer x-star of the positively strongly convex potential, use its zero gradient, and then establish the initialization estimate. ASTIS expands the omitted existence argument and removes the extra critical-point premise from the already compiled q=2 squared-cost conclusion. The all-q concentration part of the source lemma remains separate.
Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.
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.
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.
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.
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
Source assumptions versus formal assumptions
Finite-dimensional minimizer existence and zero gradient only; no Gibbs law, concentration or transport conclusion.
Encoder–denoiser: source-reviewed · implicit-assumption-exposed
Detected semantic differences
- assumptions: The source omits the minimizer-existence argument; Lean isolates it under differentiability and positive whole-space strong convexity. — Independent source review classification: source-implicit-prerequisite; nonblocking.
- domains: Lean permits every finite-dimensional real inner-product space rather than only a chosen R^d coordinate model. — Independent source review classification: coordinate-free-generalization; nonblocking.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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.
Samplinglib mathematical lesson
The SPHMC q=2 initialization bound with no supplied critical point
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialGibbsPhaseTransportUnconditional.initial_gibbs_phase_transport_q2_of_hessian_bounds · theorem · Teaching coverage
Read this first
Mathematical statement
For the actual normalized Gibbs law, its Gaussian smoothing and standard-Gaussian momentum, the q=2 squared M-kappa transport initialization cost is at most 5 kappa d, with the minimizer derived rather than assumed.
\[W_{2,M_\kappa}^{2}(\delta_{x_{\rm ref}}\otimes\gamma,(\pi*\mathsf N(0,\eta I))\otimes\gamma)\le5\kappa d,\qquad\kappa=1/\alpha.\]
Lean statement · initial_gibbs_phase_transport_q2_of_hessian_bounds
The formal statement has exactly the previous q=2 conclusion but no p parameter or gradient-zero premise. Coordinate-free finite-dimensional E and eta=0 remain valid generalizations.
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.
theorem initial_gibbs_phase_transport_q2_of_hessian_bounds
{U : E → ℝ} {α η : ℝ≥0} (hα : 0 < α) (hαone : α ≤ 1)
(hU : ContDiff ℝ 2 U)
(hH : ∀ x v : E,
(α : ℝ) * ‖v‖ ^ 2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
fderiv ℝ (fderiv ℝ U) x v v ≤ ‖v‖ ^ 2)
(xref : E) (href : ‖gradient U xref‖ ^ 2 ≤
(α : ℝ) * (Module.finrank ℝ E : ℝ)) (hη : η ≤ 1) :
let μ := (volume : Measure E).tilted (fun x ↦ -U x)
let πη := gaussianSmoothing μ (Real.sqrt η)
PhaseMetric.phaseWassersteinSq (1 / (α : ℝ))
((Measure.dirac xref).prod (stdGaussian E))
(πη.prod (stdGaussian E)) ≤
ENNReal.ofReal (5 * (1 / (α : ℝ)) * (Module.finrank ℝ E : ℝ))
Exact module and namespace context
Proof roadmap
- 1Convert Hessian curvature to strong convexity
The genuine C2 Hessian lower bound implies whole-space strong convexity with the same alpha.
- 2Construct the source minimizer
Positive strong convexity and differentiability supply a global minimizer p with zero gradient; p is not added as a theorem hypothesis.
- 3Apply the verified numerical transport chain
The constructed critical point is fed to the already verified Gibbs moment, smoothing and identical-momentum coupling theorem.
Full assumptions and notation
All objects and hypotheses
- E is a finite-dimensional complete real inner-product Borel space.
- U is C2 with alpha I ≤ Hessian U ≤ I and 0 < alpha ≤ 1.
- The reference point has squared gradient norm at most alpha times dimension.
- The smoothing variance eta lies in [0,1].
Mathematical proof
1. Convert Hessian curvature to strong convexity
The genuine C2 Hessian lower bound implies whole-space strong convexity with the same alpha.
\[D^2U(x)\succeq\alpha I\Longrightarrow U\text{ is }\alpha\text{-strongly convex}.\]
Corresponding Lean step
HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower performs the affine-line argument.
2. Construct the source minimizer
Positive strong convexity and differentiability supply a global minimizer p with zero gradient; p is not added as a theorem hypothesis.
\[\exists p:\ U(p)=\min U,\quad\nabla U(p)=0.\]
Corresponding Lean step
StrongConvexMinimizer.exists_isMinOn_and_gradient_eq_zero discharges the hidden source step.
3. Apply the verified numerical transport chain
The constructed critical point is fed to the already verified Gibbs moment, smoothing and identical-momentum coupling theorem.
\[\nabla U(p)=0\Longrightarrow W_{2,M_\kappa}^{2}(\mu_0,\Pi_\eta)\le5\kappa d.\]
Corresponding Lean step
InitialGibbsPhaseTransport.initial_gibbs_phase_transport_q2 supplies the actual normalized measures and constant.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · initial_gibbs_phase_transport_q2_of_hessian_bounds
The proof composes the genuine Hessian-to-strong-convexity bridge, the new minimizer theorem and the independently verified conditional q=2 theorem.
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.
theorem initial_gibbs_phase_transport_q2_of_hessian_bounds
{U : E → ℝ} {α η : ℝ≥0} (hα : 0 < α) (hαone : α ≤ 1)
(hU : ContDiff ℝ 2 U)
(hH : ∀ x v : E,
(α : ℝ) * ‖v‖ ^ 2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
fderiv ℝ (fderiv ℝ U) x v v ≤ ‖v‖ ^ 2)
(xref : E) (href : ‖gradient U xref‖ ^ 2 ≤
(α : ℝ) * (Module.finrank ℝ E : ℝ)) (hη : η ≤ 1) :
let μ := (volume : Measure E).tilted (fun x ↦ -U x)
let πη := gaussianSmoothing μ (Real.sqrt η)
PhaseMetric.phaseWassersteinSq (1 / (α : ℝ))
((Measure.dirac xref).prod (stdGaussian E))
(πη.prod (stdGaussian E)) ≤
ENNReal.ofReal (5 * (1 / (α : ℝ)) * (Module.finrank ℝ E : ℝ)) := by
have hsc : StrongConvexOn (Set.univ : Set E) (α : ℝ) U :=
HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower hU
(fun x v ↦ (hH x v).1)
obtain ⟨p, _, hp⟩ := StrongConvexMinimizer.exists_isMinOn_and_gradient_eq_zero
(show (0 : ℝ) < α by exact hα) (hU.differentiable (by norm_num)) hsc
exact InitialGibbsPhaseTransport.initial_gibbs_phase_transport_q2
hα hαone hU hH p xref hp href hη
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialGibbsPhaseTransportUnconditional
Exact module and namespace context
Source assumptions versus formal assumptions
The q=2 squared-cost component only; no all-q concentration, Picard dynamics, output accuracy, cost or complete main theorem.
Encoder–denoiser: source-reviewed · lean-weakened-conclusion
Detected semantic differences
- conclusion: The theorem proves only the squared q=2 bound, not the source's every-q initialization inequality. — Independent source review classification: scoped-q2-specialization; nonblocking.
- constant_dependencies: The factor 5 is an ASTIS numerical consequence of the q=2 moment chain, not a constant printed in Lemma 4.16. — Independent source review classification: derived-explicit-constant; nonblocking.
- domains: The formalization permits eta=0 and coordinate-free finite-dimensional real inner-product spaces beyond the paper's positive-eta R^d algorithmic setting. — Independent source review classification: valid-endpoint-and-coordinate-generalization; nonblocking.
- assumptions: No minimizer is supplied: positive C2 Hessian curvature gives strong convexity, compactness yields a minimizer, and differentiability gives zero gradient. — Independent source review classification: internal-minimizer-discharged; nonblocking.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
Scope and omitted-condition boundaries
- This closes the minimizer-existence gap in the q=2 component of Lemma 4.16. The source's q>2 concentration, the Picard kernel, final accuracy and query complexity are still not proved.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
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.