Samplinglib
Lean gate passed 2026-08-19T06:04:36.257124+00:00 · 77184245109a
Depth 02

Rigorous Details

This layer answers the question a phrase such as “by approximation” leaves open: exactly which hypotheses make the step legal?

Measure and representatives

  • Measurability and strong measurability are stated for the actual codomain.
  • Almost-everywhere representatives are fixed before applying pointwise calculus.
  • Normalization, absolute continuity, and zero-density conventions are explicit.

Integrals and limits

  • Every Bochner integral has a proved Integrable hypothesis.
  • Dominating functions are independent of the limiting parameter and integrable.
  • Tonelli, Fubini, and interchange of limits identify their exact hypotheses.

Calculus and support

  • Genuine differentiability is separated from totalized fderiv values.
  • Support, topological support, and compact support are not interchanged.
  • Cutoff-gradient and main-term limits are proved as independent edges.

Operators and stochastic laws

  • A formal differential expression is not a closed generator.
  • Core symmetry is not automatically symmetry on the generator domain.
  • Stationary densities, stationary solutions, and invariant semigroup laws remain distinct.
Audit by chapter

Hidden mathematical contracts

Chapter 1 · The Langevin Diffusion in Continuous Time
  • The weighted integration-by-parts identity first needs compactly supported test functions or a justified cutoff limit.
  • Pointwise exhaustion of a cutoff does not imply convergence of its gradient term under an integral.
  • A totalized Fréchet derivative equal to zero outside a support set does not assert differentiability there.
  • The score-weighted source field must be integrable before dominated convergence can be applied.
  • Formal symmetry, a closed generator on a stated domain, stationarity, and invariance are separate claims.
Open chapter detail layer →
Chapter 2 · Functional Inequalities
  • State whether Hessian inequalities hold everywhere, almost everywhere, or in a weak convex-analytic sense.
  • Track normalization and absolute continuity whenever a potential is used to define a probability law.
  • Keep localization inputs separate from the one-dimensional inequality they reduce to.
Open chapter detail layer →
Chapter 3 · Additional Topics in Stochastic Analysis
  • Quadratic-variation limits require an explicit convergence mode and partition scheme.
  • A stochastic exponential needs measurability and integrability conditions before it defines a change of law.
  • Finite-dimensional cylinder identities are not automatically path-space Girsanov theorems.
Open chapter detail layer →
Chapter 4 · Analysis of Langevin Monte Carlo
  • The coupled processes must be constructed on one filtered probability space.
  • Path-space laws and filtration-adapted drift differences must be explicit.
  • Optimization analogies do not replace stochastic existence or integrability assumptions.
Open chapter detail layer →
Chapter 5 · Faster Low-Accuracy Samplers
  • Invariant phase-space laws require both position and momentum normalization.
  • Hypocoercive estimates mix position and velocity norms; coercivity is not pointwise in the position coordinate alone.
  • Exact Hamiltonian flow and numerical integrators must not be conflated.
Open chapter detail layer →
Chapter 6 · Convergence in Rényi Divergence
  • The interpolated chain must be adapted and have the same diffusion coefficient as the comparison process.
  • Moment estimates must be established before integrating local drift error.
  • Step-size restrictions and all dimension/condition-number constants must be retained.
Open chapter detail layer →
Chapter 7 · High-Accuracy Samplers
  • Kernel measurability and exceptional zero-density cases must be defined.
  • Detailed balance is a measure identity, not merely a pointwise density calculation.
  • Cold-start arguments require smoothing or explicit initialization bounds.
Open chapter detail layer →
Chapter 8 · The Proximal Sampler
  • Both conditional distributions require finite, measurable normalizing constants.
  • Marginal preservation follows from Tonelli/Fubini only after nonnegativity and measurability are established.
  • An oracle specification must state whether samples are exact or approximate.
Open chapter detail layer →
Chapter 9 · Lower Bounds for Sampling
  • The oracle transcript and algorithmic randomization must be represented explicitly.
  • Pairwise divergence bounds need the exact observation law.
  • The hard family must remain inside the stated target class.
Open chapter detail layer →
Chapter 10 · Structured Sampling
  • Stochastic-gradient unbiasedness and variance bounds are conditional statements with a specified filtration or kernel.
  • Coordinate schedules, coordinate-dependent step sizes, and anisotropic norms must be measurable and retained in constants.
  • Mirror maps need an open effective domain, invertible gradient map, and boundary/nonexplosion control for the transformed diffusion.
  • Oracle error, discretization error, and continuous-time convergence remain separate terms.
Open chapter detail layer →
Chapter 11 · Non-Log-Concave Sampling
  • Relative Fisher information needs an absolutely continuous law and a chosen score representative.
  • Entropy dissipation must be justified for the actual process and function domain, not only calculated formally.
  • Randomized-time output requires measurability of the time-indexed law and Fisher-information integrand.
  • Finite-time discretization and score-error bounds must specify the law under which every squared error is integrated.
  • Small Fisher information is a stationarity certificate, not automatically small total variation or rapid multimodal mixing.
Open chapter detail layer →
Chapter 12 · Diffusion Generative Models
  • A score is defined only with respect to a chosen density and representative.
  • Reverse-time formulas require time-marginal regularity and a precise filtration statement.
  • An L2 score approximation under one law cannot silently be used under another law.
Open chapter detail layer →

No promotion by prose

A complete explanation can document a red node, but it does not make the node blue. Blue status is reserved for an ASTIS-owned declaration resolved in the source Registry and covered by the local Lean build gate.