Smoothed Picard HMC

Smoothing, Picard dynamics and the proxy warm start.

Main paper results remain open in Lean. Verified building blocks are listed separately below.

Paper, notation and source conventions

Smoothed Picard Hamiltonian Monte Carlo

Source: 2609.06906v1. Pinned source version

\[d\ge1,\quad V\in C^2(\mathbb R^d),\quad 0<\alpha I\preceq\nabla^2V(x)\preceq\beta I,\quad \kappa=\beta/\alpha,\quad \pi(dx)=Z^{-1}e^{-V(x)}dx\]

The Hessian inequalities hold at every point; \(\alpha\) and \(\beta\) are positive real numbers. Separate Hessian-to-chord and Gibbs-integrability proofs support the compiled normalized PBPS augmentation certificate: positive Gibbs integral, probability and exact product-volume joint density. Consult linked cells for independent-review and admission states. Conditional kernels, the sampling process and its guarantees remain separate.
\(\operatorname{TV}(P,Q)\) means sup over measurable events of \(|P(A)-Q(A)|\). For probability laws with densities it is half their \(L^1\) distance.
\(R_2(P\Vert Q)=\log\int\left(\frac{dP}{dQ}\right)^2\,dQ\) when P is absolutely continuous with respect to Q, and infinity otherwise. The PBPS paper writes \(D_2\) and calls the target \(\mu\); here the common target is \(\pi\).
Expected oracle queries are not worst-case runtime. Reference-point preparation, proximal access and gradient-only reductions must be charged under the particular theorem's model.

1. Main statements

RED · source theorem known · local proof open

Low-accuracy W2 guarantee

Source: 2609.06906v1. SPHMC Theorem 1.1; Algorithm 3.2; Section 4.5; Appendix D

Open this theorem in the interactive research workspace

Statement

Given a reference point with small gradient, the source algorithm outputs a probability law satisfying the displayed normalized Wasserstein error. This theorem counts gradient and proximal queries; gradient-only implementation is a separate reduction.

The common \(C^2\) strong-convexity/smoothness setting.
\(0<\varepsilon\le1\); a supplied \(x_{\mathrm{ref}}\) satisfies \(\|\nabla V(x_{\mathrm{ref}})\|\le\sqrt{\alpha d}\).
Use the source algorithm and its parameter choices, not an arbitrary Picard or HMC discretization.

\[\sqrt\alpha W_2(\widehat\pi,\pi)\le\varepsilon,\qquad \mathbb E Q_{\nabla,\mathrm{prox}}=O\!\left[\left(\kappa^2+\kappa^{7/6}d^{1/6}\varepsilon^{-1/3}\right)\log^4\frac{e\kappa d}{\varepsilon}\right]\]

Lean statement — not formalized yet

A future declaration must bind the probability laws, normalization, regularity, source algorithm and oracle model explicitly. The formula is a source theorem contract, not Lean code.

No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.

Proof architecture and calculations · 3 steps

This is a source-linked proof route, not a complete reconstruction of all cited lemmas. The dependencies below remain separate formalization tasks.

Smooth the density
\[e^{-V_\eta}=e^{-V}*\mathcal N(0,\eta I),\qquad \nabla V_\eta(y)=\mathbb E[\nabla V(X)\mid X+\sqrt\eta G=y]\]
This is not the Gaussian average of V. Differentiation under the integral and a specified conditional-law version justify the score identity. The implementable score estimator has bias as well as variance; it is not assumed exactly unbiased.
Source: 2609.06906v1. Section 3.1, (3.1)–(3.2); Section 4.1
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Integrate the smoothed Hamiltonian equation
\[X_t=X_0+tP_0-\int_0^t(t-s)\nabla V_\eta(X_s)\,ds\]
Picard iteration approximates the trajectory, while Chebyshev–Lobatto quadrature approximates its integrals. Smoothing regularity, quadrature remainder and stochastic score error are separate inputs to the local-error estimate.
Source: 2609.06906v1. Sections 3.2, 4.2–4.4; Appendix B
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Budget all three errors
\[W_2(\widehat\pi,\pi)\le W_2(\widehat\pi,\pi_\eta)+W_2(\pi_\eta,\pi)\]
The first term includes iteration and numerical errors; the second is the smoothing bias. Finite second moments and the exact-kernel contraction must be supplied before using this triangle inequality.
Source: 2609.06906v1. Section 4.5; Appendix C.3
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.

Lean proof — not formalized yet

Formalization will first match the named technology interfaces, then assemble this source theorem. No placeholder proof or source-cited wrapper has been added.

No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.

Strict boundary

No Wq, Renyi warmness, exact stationarity of a discretization, or cost-free proximal oracle follows from this \(W_2\) statement.

Further source statements · 1

RED · source theorem known · local proof open

An implementable law near a Renyi-warm proxy

Source: 2609.06906v1. SPHMC Theorem 1.2; Theorem 7.1(ii); Sections 5–6

Open this theorem in the interactive research workspace

Statement

For every allowed \(\delta\) the algorithm produces the actual law below. A second, existential comparison law is close in TV and has bounded order-2 Renyi divergence. The comparison law need not be directly sampled.

The common setting and the same reference-point bound as Theorem 1.1.
0 < \(\delta\) < 1/2.
The recursive generator uses higher-moment smoothed sampling and terminal RGO implementation; this is not a general \(W_2\)-to-Renyi implication.

\[\exists\widehat\pi_\delta^\dagger:\quad \operatorname{TV}(\widehat\pi_\delta,\widehat\pi_\delta^\dagger)\le\delta,\quad R_2(\widehat\pi_\delta^\dagger\Vert\pi)\le1,\qquad \mathbb E Q_\nabla=O\!\left(\kappa^{7/6}d^{1/6}\log^9\frac{e\kappa d}{\delta}\right)\]

Lean statement — not formalized yet

A future declaration must bind the probability laws, normalization, regularity, source algorithm and oracle model explicitly. The formula is a source theorem contract, not Lean code.

No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.

Proof architecture and calculations · 3 steps

This is a source-linked proof route, not a complete reconstruction of all cited lemmas. The dependencies below remain separate formalization tasks.

Turn a moment bound into a nearby bounded-displacement coupling
\[W_p(P,Q)\le r\quad\Longrightarrow\quad\exists P^\dagger:\ \operatorname{TV}(P,P^\dagger)\le\delta,\quad W_\infty(P^\dagger,Q)\le r\delta^{-1/p}\]
For \(p\ge2\) and finite p-moments, replace a coupled sample by its partner on the event where displacement exceeds \(r\delta^{-1/p}\). Markov's inequality bounds that event; measurability and coupling attainment must be justified.
Source: 2609.06906v1. Lemma 6.2
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Regularize both laws before measuring divergence
\[R_q(P^\dagger*\gamma_\tau\Vert Q*\gamma_\tau)\le\frac{qW_p(P,Q)^2}{2\tau\delta^{2/p}},\qquad q>1,\quad\tau>0\]
A Gaussian reverse-transport bound applies after convolution. Recursive conditional/RGO updates then recover the desired unsmoothed target; deleting that recursion would change the theorem.
Source: 2609.06906v1. Lemma 6.3(ii); Theorems 6.1 and 6.5
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Track the moving conditional target and oracle bill
\[(A^+)^{-1}=A^{-1}+a^{-1},\qquad u^+=A^+(u/A+y/a)\]
Completing the square closes the RGO family under another RGO. The recursive stages and outer proximal sampler improve conditioning; the \(\kappa\)-squared setup term from Theorem 1.1 is not silently discarded.
Source: 2609.06906v1. Lemma 6.4; Sections 6.3–6.4 and 7.1
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.

Lean proof — not formalized yet

Formalization will first match the named technology interfaces, then assemble this source theorem. No placeholder proof or source-cited wrapper has been added.

No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.

Strict boundary

Only the proxy has the displayed Renyi certificate. Genuine Renyi warmness of the actual output requires the stronger W_psi2 input in the separate source theorem.

3. What has been verified?

130 source-mapped declarations; 119 independently reviewed. These are building blocks, not completed paper results.

Browse statements and their mathematical proofs

Actual affine normalized Gibbs transport

Actual affine normalized Gibbs transport

1. Main statements

Low-accuracy W2 guarantee

Statement

Smooth the density

Integrate the smoothed Hamiltonian equation

Budget all three errors

Strict boundary

An implementable law near a Renyi-warm proxy

Statement

Turn a moment bound into a nearby bounded-displacement coupling

Regularize both laws before measuring divergence

Track the moving conditional target and oracle bill

Strict boundary

3. What has been verified?