p · Potential smoothness
The available regularity and constants Lp. A smaller local remainder need not change the diffusion's mixing geometry.
New companion frontiers
Smoothed Picard HMC, Proximal BPS, and their proxy-stable composition: two source cases, one shared proof route; local formalization remains open.
Read the frontier theorems and proof graph → · Reusable proof technology →
Research route · Optimisation × Sampling
What does higher-order smoothness buy for sampling?
A contract-driven research program, not a claim that this literature is empty and not a completed Lean theorem.
Four orders, four different questions.
Let V be a potential on Euclidean space, with target π proportional to exp(−V). A first controlled class has αI ≼ ∇²V ≼ βI and a Lipschitz p-th derivative, measured in operator norm. Here α > 0 is the strong-convexity constant and β bounds the Hessian.
\[\|D^p V(x)-D^p V(y)\|_{\mathrm{op}}\leq L_p\|x-y\|.\]
q · Oracle information
The highest derivative the algorithm may query: gradients, Hessians or higher tensors. Extra regularity does not grant extra oracle access.
k · Dynamical order
The chosen extended-state Langevin system. Auxiliary variables are not derivative queries; preserve the intended positional marginal.
r · Approximation accuracy
The local error exponent and its metric; weak error, strong error and invariant-measure bias are different contracts.
What is already known—and what we will audit.
Mou et al. analyze a high-order Langevin construction, including smoothness-dependent regimes. Shen–Lee improve discretization with randomized midpoint under strong convexity and Lipschitz gradients. Dang et al. study higher-order Langevin dynamics. These are different mechanisms; source-by-source theorem audits must precede any rate table or claim of novelty.
Our first question holds the oracle fixed and changes regularity. The second allows richer oracles and charges their full cost. The third keeps regularity fixed and changes the stochastic integrator. Only then should we explore weaker curvature, manifolds or non-log-concave targets.
First reusable target: local error → global sampling error.
Let P_h be an exact Markov evolution with invariant π and W₂ contraction factor a = exp(−αh), where h > 0 and α > 0. Let K_h be the numerical kernel and μ_j = μ_0 K_h^j. Suppose all laws have finite second moments and, along this orbit, W₂(μ_j K_h, μ_j P_h) ≤ C h^(r+1), with a uniform C. The triangle inequality gives the following proposed reusable interface:
\[e_{j+1}\leq a e_j+C h^{r+1},\qquad e_N\leq a^N e_0+C h^{r+1}\frac{1-a^N}{1-a},\quad e_j=W_2(\mu_j,\pi).\]
This elementary implication is a target for reuse/audit, not new research or a Lean closure. The difficult task is proving the local bound with controlled moments and the right invariant target, then determining its dependence on p, q, k, dimension d and the requested error ε. Moment-dependent local constants must be bounded along the whole numerical orbit.
The exact-flow contract and the numerical-analysis contract remain separate. Do not infer a usable r directly from p. Charge N oracle calls multiplied by per-step derivative, tensor, linear-algebra and auxiliary-variable costs; parallel rounds are a separate budget.
Upper and lower bounds: complementary, not one forced proof route.
Upper-bound lane: Taylor remainders → stochastic integration/moments → stable kernel and invariant target → contraction/mixing → cost-aware accuracy.
SampleWiki lower-bound lane: admissible hard distributions → oracle transcripts → indistinguishability or testing → reduction and query lower bound. Its proof need not use the high-order integrator.
Compare only matched contracts: potential class and regularity constants; q-th derivative versus stochastic oracle; warm/cold starts; KL/TV/W₂ normalization; adaptive randomized access; success probability; total work versus parallel depth. A statistical OT sample size is not automatically a sampling query budget.
Shared probability, data-processing and discrepancy lemmas may be reused. A hardness transfer between fields requires an explicit simulation and error/cost transformation. No current plan presumes the unknown lower bound matches the upper bound.
Acceptance and stopping boundaries
A publishable advance must either reuse an exact existing theorem, add a genuinely missing compiled lemma with consumers, prove a cost-aware improvement under a fixed comparison contract, or expose a typed obstruction/counterexample. An alternative proof, new diagram or additional assumption alone is not a new sampling complexity result.
Dependency-ready shared work queue · ASTIS Harness and independent verification
Primary starting sources
- Mou et al., High-Order Langevin Diffusion Yields an Accelerated MCMC Algorithm: JMLR 22(42), 2021; high-order diffusion and smoothness-dependent guarantees
- Shen–Lee, The Randomized Midpoint Method for Log-Concave Sampling: Strong convexity and Lipschitz gradient; randomized discretization
- Dang et al., High-Order Langevin Monte Carlo Algorithms: Higher-order dynamics; splitting and accurate integration
- Liu–Chewi, A proximal gradient algorithm for composite log-concave sampling: Composite target and restricted Gaussian oracle
- Nitanda–Wu–Suzuki, Convex Analysis of the Mean Field Langevin Dynamics: Entropy sandwich, proximal Gibbs distribution, PL/quadratic-growth counterparts and LSI-based decay
- Chatterji et al., Oracle Lower Bounds for Stochastic Gradient Sampling Algorithms: Oracle-information model and sampling lower bounds
Literature entry points checked 5 September 2026; this is not an exhaustive novelty search.