Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d

Cold start to high accuracy: the producer–consumer contract

Composition view of SPHMC Theorem 1.3, not a third paper or an ASTIS novelty claim.

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

Paper, notation and source conventions

Smoothed Picard Hamiltonian Monte Carlo

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

Source: 2609.06906v1 · 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

Compose through a proxy, with an explicit TV budget

Source: 2609.06906v1 · 2609.06905v1. SPHMC Theorem 1.3 and its proof in Section 7.2; PBPS Theorem 4.3 / Corollary 4.4

Open this theorem in the interactive research workspace

Statement

Given the supplied small-gradient reference point, warm-start generation followed by Proximal BPS yields the stated TV accuracy and expected gradient cost. Algorithmic order is HighAccuracyEngine after WarmStartGenerator.

  • The common setting; \(\|\nabla V(x_{\mathrm{ref}})\|\le\sqrt{\alpha d}\); \(0<\varepsilon<1/4\).
  • Use one measurable implemented probability kernel K for both the actual input law and its comparison law.
  • The PBPS input certificate uses the same normalized target, order-2 Renyi convention and gradient oracle. Its source warmness bound is \(\Delta\), not \(\Delta\) squared; SPHMC Theorem 7.2 reparameterizes that symbol.
\[\operatorname{TV}(\widehat\pi,\pi)\le\varepsilon,\qquad\mathbb E Q_\nabla=O\!\left(\kappa^{7/6}d^{1/6}\log^9\frac{e\kappa d}{\varepsilon}+\sqrt\kappa d^{1/4}\log^{11/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 · 4 steps

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

  1. Produce the implementable law and retain its witness

    \[\operatorname{TV}(\mu,\mu^\dagger)\le\varepsilon/2,\qquad R_2(\mu^\dagger\Vert\pi)\le1/4\]

    The stronger Theorem 7.1(ii), with its accuracy parameter set to 1/2, supplies this witness. We run the next algorithm on \(\mu\), not on the existential \(\mu\)-dagger.

    Source: 2609.06906v1 · 2609.06905v1. SPHMC Section 7.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.

  2. Apply TV data processing to the same implemented kernel

    \[\operatorname{TV}(\mu K,\mu^\dagger K)\le\operatorname{TV}(\mu,\mu^\dagger)\le\varepsilon/2\]

    For a measurable event A, the probability-kernel function x ↦ K(x,A) lies in [0,1]. The layer-cake identity writes its integral against the difference of the two probability laws as an integral of event differences, each bounded by TV. Taking the supremum over A proves the inequality without assuming a density for \(\mu\).

    Source: 2609.06906v1 · 2609.06905v1. SPHMC Section 7.2; ASTIS expansion of the data-processing step

    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.

  3. Use the warm theorem only on the witness

    \[\operatorname{TV}(\mu K,\pi)\le\operatorname{TV}(\mu K,\mu^\dagger K)+\operatorname{TV}(\mu^\dagger K,\pi)\le\varepsilon\]

    The witness satisfies the warm hypothesis with budget 1. The kernel's warm-start error is \(\varepsilon\)/2; the triangle inequality adds, rather than multiplies, the two errors.

    Source: 2609.06906v1 · 2609.06905v1. SPHMC Theorem 1.3 proof

    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.

  4. Transfer accuracy and cost by different arguments

    \[\mathbb E(Q_{\rm warm}+Q_{\rm engine})=\mathbb E Q_{\rm warm}+\mathbb E Q_{\rm engine}\]

    TV proximity alone cannot bound an unbounded query count. PBPS uses a fixed iteration budget, capped proximal solves, bounded candidate-event intensity and uniformly controlled expected RGO queries after a residual check. Port the conditional cost bound for the actual input before using linearity of expectation; do not borrow only the proxy's expected cost.

    Source: 2609.06906v1 · 2609.06905v1. PBPS Algorithm 2 and (4.18); SPHMC (7.1) and Section 7.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.

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

The source theorem is known; every new local formal edge here remains red. Neither a generic Wasserstein-to-Renyi conversion nor a certified category/functor is claimed.

3. Verified work

No declaration-level publication is attached to this page yet. A source proof route is not a Lean verification.

Compare proof mechanisms and prerequisites

Reusable prerequisites · What changes in the proof?