Midpoint Langevin
Dimension-dependent upper bounds and separate oracle lower bounds.
Main paper results remain open in Lean. Verified building blocks are listed separately below.
Suggested reading order
- Read exact v1 source and the full assumptions below; source informal overview does not replace precise main theorem contracts.
- Keep deterministic Heun/exponential midpoint and randomized/Poisson methods as separate kernels.
- Inspect exact source Section3/4 upper bounds and Section5/6 lower bounds/initialization; source proofs remain open in Lean.
- Reusable Gaussian/transport/convexity background belongs to existing canonical shared nodes, only genuinely relevant textbook chapters; no blanket seven-route mapping.
Paper, notation and source conventions
Sharp dimensional analysis of midpoint methods for Langevin sampling
Source: 2610.06308v1. Pinned source version
- 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
Deterministic guarantees: source Theorem1.1 (informal)
Source: 2610.06308v1. Theorem1.1; precise Theorems3.1/4.1 and source Section2 algorithms
Open this theorem in the interactive research workspace
Statement
For \(0<\varepsilon\le\sqrt d/2\), Heun initialized at the unique minimizer \(x_\star\) reaches \(\sqrt{\alpha}\,W_2\le\varepsilon\) with the displayed gradient-query bound. Exponential midpoint with \(\text{friction }2\sqrt{\beta}\), \(X_0=x_\star\) and independent \(P_0\sim\mathcal N(0,I_d)\) has the second bound for its position law. \(\widetilde O\) suppresses logarithms. This faithfully restates the labelled informal theorem; exact schedules/universal constants of3.1/4.1 remain separate source obligations.
- \(d\ge1\), V globally \(C^2\) on real d-space, \(0\prec\alpha I\preceq\nabla^2 V(x)\preceq\beta I\) at every x; \(\kappa=\beta/\alpha\); normalized target \(\pi\) proportional \(e^{-V}\).
- No bounds on third or higher derivatives are assumed. \(W_2\) is true Wasserstein distance; accuracy is \(\sqrt{\alpha}\,W_2\).
- Use the actual source midpoint algorithms in Section2, not an arbitrary integrator or abstract-error certificate.
- \(0<\varepsilon\le\sqrt d/2\). Heun starts at \(x_\star\); exponential midpoint has \(X_0=x_\star\), independent standard Gaussian momentum and \(\text{friction }2\sqrt{\beta}\).
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 · 2 steps
This is a source-linked proof route, not a complete reconstruction of all cited lemmas. The dependencies below remain separate formalization tasks.
Preserve the genuine transition and stationary error
\[\nu_N^{\rm H}=\nu_0^{\rm H}(K_h^{\rm H})^N,\quad\boldsymbol\nu_N^{\rm E}=\boldsymbol\nu_0^{\rm E}(K_h^{\rm E})^N,\quad\nu_N^{\rm E}=(\boldsymbol\nu_N^{\rm E})_x,\quad\pi_h^{\rm E}=(\boldsymbol\pi_h^{\rm E})_x;\qquad W_2(\nu_N,\pi)\le W_2(\nu_N,\pi_h)+W_2(\pi_h,\pi).\]Heun uses the position Markov kernel \(K_h^H\). Exponential midpoint uses the true position-momentum kernel \(K_h^E\) and its phase-space law; \(\nu_N^E\) and \(\pi_h^E\) are position marginals before the position \(W_2\) triangle inequality. The position marginal is not assumed Markov. Actual invariant laws and finite-step contraction must be proved, not supplied as oracle premises.
Source: 2610.06308v1. Sections2-4; AppendicesA/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.
Use cancellation under only C2 Hessian bounds
\[\alpha I\preceq\nabla^2V\preceq\beta I.\]Heun uses a discrete Poisson corrector, Malliavin–Stein and Gaussian smoothing. Exponential midpoint uses weighted negative-Sobolev divergence cancellation and transport. Missing regularity details must be supplied without adding higher derivative bounds to the source theorem.
Source: 2610.06308v1. AppendicesA/B/E
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
Source-pinned phase3 plan only; no new midpoint Lean theorem, actual kernel, invariant bias, schedule, convergence or complexity certificate is claimed.
Further source statements · 1
RED · source theorem known · local proof open
Stationary and finite-iteration lower bounds: source Theorem1.2 (informal)
Source: 2610.06308v1. Theorem1.2/Table1; Proposition5.1,Theorem5.2,Propositions5.3/6.1/6.2,Corollary6.3
Open this theorem in the interactive research workspace
Statement
For each Table1 method and every sufficiently small normalized step h, there is a strongly convex smooth target of bounded condition number and a position initialization with expected potential gap at most C*d. For every sufficiently small \(\varepsilon\), attaining \(\sqrt\alpha\,W_2(\text{position law after }N\text{ steps},\pi)\le\varepsilon\) requires the Table1 lower-bound number of queries up to logarithms. For underdamped methods the initial momentum is independent standard Gaussian. This is the source-labelled informal overview; stationary bias and finite-iteration claims keep their separate precise source contracts.
- \(d\ge1\), V globally \(C^2\) on real d-space, \(0\prec\alpha I\preceq\nabla^2 V(x)\preceq\beta I\) at every x; \(\kappa=\beta/\alpha\); normalized target \(\pi\) proportional \(e^{-V}\).
- No bounds on third or higher derivatives are assumed. \(W_2\) is true Wasserstein distance; accuracy is \(\sqrt{\alpha}\,W_2\).
- Use the actual source midpoint algorithms in Section2, not an arbitrary integrator or abstract-error certificate.
- Existential target and initialization, bounded condition number, sufficiently small normalized h and \(\varepsilon\); \(\mathbb E[V(X_0)-V(x_\star)]\le C d\). Underlying momentum is standard Gaussian and independent of X0.
- Poisson midpoint uses at least2 grid points and constant expected gradients per batch. Exact stationary/finitestep quantifiers and source constants remain in the named precise results.
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 · 2 steps
This is a source-linked proof route, not a complete reconstruction of all cited lemmas. The dependencies below remain separate formalization tasks.
Keep deterministic bias and finite initialization distinct
\[\mathbb E[V(X_0)-V(x_\star)]\le Cd.\]Oscillatory targets yield the deterministic Heun obstruction; Gaussian/anisotropic Gaussian targets give exponential-midpoint bounds. Stationary bias alone does not establish every finite-step initialization claim.
Source: 2610.06308v1. Section5; Corollary6.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.
Track shared randomized covariance fluctuations
\[X\mid\mathcal H\sim\mathcal N(0,\Sigma(\mathcal H)).\]For the actual randomized methods, shared quadrature choices induce common covariance fluctuations. The source Section6 calculations and finite-step passage must be formalized under their actual randomness; independent coordinates must not be invented unconditionally.
Source: 2610.06308v1. Section6; AppendixD
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
Source-pinned phase3 plan only; neither a lower-bound oracle certificate nor finite-step proof is claimed. Upper-bound and hardness lanes stay separate until method/accuracy/initialization/query contracts match.
3. Verified work
No declaration-level publication is attached to this page yet. A source proof route is not a Lean verification.