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.

Download module (.lean)

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.

Download module (.lean)

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

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)

ContDiff.differentiable

Mathematical sources

Smoothed Picard Hamiltonian Monte Carlo, Lemma 4.16, PDF p.22 — The source selects a minimizer internally; ASTIS now constructs it from the printed curvature assumptions.

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