Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

Planned local formalization

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.

Common setting and conventions

\[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.
  • TV(P,Q) means sup over measurable events of |P(A)-Q(A)|. For probability laws with densities it is half their L1 distance.
  • R_2(P||Q)=log integral (dP/dQ)^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.

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

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; ||grad V(x_ref)|| <= sqrt(alpha d); 0 < epsilon < 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

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

  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

  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 epsilon/2; the triangle inequality adds, rather than multiplies, the two errors.

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

  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

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.

Expand reusable prerequisites and next packets →