Proximal BPS

High accuracy from a warm start: process, invariant kernels and convergence.

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

Paper, notation and source conventions

Accelerated High-Accuracy Sampling from a Warm Start via the Proximal Bouncy Particle Sampler

Source: 2609.06905v1. 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

Optimized expected gradient complexity

Source: 2609.06905v1. PBPS Corollary 4.4, (4.19)–(4.20); Theorem 4.3, (4.8)–(4.9)

Open this theorem in the interactive research workspace

Statement

With universal positive tuning constants, run the implementable algorithm with the source parameter choices. Its output is \(\varepsilon\)-close to the target in TV and has the following expected gradient-query bound. No fixed worst-case running-time claim is made.

The common setting; an input probability law \(\mu_0\) with \(R_2(\mu_0\Vert\pi)\le\Delta\), where \(\Delta\ge1\).
\(0<\varepsilon<1/4\); query access to \(\nabla V\) and a sample from \(\mu_0\).
Choose L and \(\eta\) below and the iteration, resampling, error and solver budgets in source (4.8)–(4.9). The constants \(c_{\mathrm{opt}}\) and \(K_{\mathrm{opt}}\) are universal, not arbitrary user choices.

\[\begin{gathered}L=\Delta+\log\frac{K_{\rm opt}d\kappa}{\varepsilon},\quad\eta=\frac{c_{\rm opt}}{\beta(\sqrt{dL}+L)},\quad\operatorname{TV}(\mathcal L(\widehat X),\pi)\le\varepsilon,\\\mathbb E Q_\nabla\le K_{\rm opt}\sqrt\kappa(d+L)^{1/4}L^{3/4}\left(\Delta+\log\frac4\varepsilon\right)\log(\kappa L).\end{gathered}\]

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 · 4 steps

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

Augment, then reflect the auxiliary variable
\[\pi_\eta(dx,dy)=\pi(dx)\mathcal N(x,\eta I)(dy),\qquad (x,y)\mapsto(x,2x-y)\]
Gaussian symmetry preserves the augmented law under this reflection. It differs from velocity reflection at a bounce. A conditional half-turn and occasional RGO resampling form the ideal transition; they are not independent ordinary Gibbs redraws at every step.
Source: 2609.06905v1. Proposition 2.1; (3.11); Proposition 3.4
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.
Use discrete hypocoercivity, not a reversible gap shortcut
\[f=\mathbb E[f\mid Y]+(f-\mathbb E[f\mid Y]),\qquad\chi^2(\nu_0\mathcal K^{JN}\Vert\pi_\eta)\le e^{-J}\chi^2(\nu_0\Vert\pi_\eta)\]
The source chooses \(\eta\), \(\rho\) and a block length N as in Theorem 3.5. Conditional resampling damps the fluctuation; reflection couples it to the conditional mean. A modified L2 energy and half-turn operator bounds are essential. The local unrefreshed process alone need not mix.
Source: 2609.06905v1. Theorem 3.5; Appendices B–C
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.
Keep implementation mismatch separate from ideal mixing
\[\mathbb P(\widehat X\ne X_T^{\rm id})\le3Ta=\varepsilon/2,\qquad\operatorname{TV}(\mathcal L(\widehat X),\pi)\le\varepsilon/2+\varepsilon/2\]
Solver failure, approximate RGO draws and capped bounce rates each consume an error budget a. Lifted Renyi control bounds bad events along the ideal chain; a coupling union bound transfers its convergence to the implemented output.
Source: 2609.06905v1. Theorem 4.3, (4.14)–(4.18)
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.
Balance localization against block length
\[(\alpha\eta)^{-1/2}=\sqrt{\kappa/c_{\rm opt}}(\sqrt{dL}+L)^{1/2}\]
Substitute the chosen \(\eta\) into the iteration bound and charge proximal solves, RGO calls and candidate bounce queries. Retaining L prevents a hidden warmness or precision dependence from disappearing into the dimension exponent.
Source: 2609.06905v1. Corollary 4.4, (4.21)–(4.23)
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

This is the discrete augmented Proximal BPS algorithm with curved conditional flights. It is not vanilla continuous-time BPS, and its acceleration does not follow just from invariance or an algebraic reflection identity.

3. What has been verified?

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

Browse statements and their mathematical proofs

Actual centered original-gradient Poincare

Actual centered original-gradient Poincare

1. Main statements

Optimized expected gradient complexity

Statement

Augment, then reflect the auxiliary variable

Use discrete hypocoercivity, not a reversible gap shortcut

Keep implementation mismatch separate from ideal mixing

Balance localization against block length

Strict boundary

3. What has been verified?