Samplinglib
Lean gate passed 2026-08-19T05:09:39.794721+00:00 · 644be936998e
Progress without invented percentages

Progress and Roadmap

Milestones are categorical and evidence-backed. “Compiled” applies to local declarations. “Partial” or “blocked” records the mathematical route, including unformalized hypotheses and theorem assembly.

flowchart LR
  Local["Local declaration status"]:::header
  Route["Mathematical route status"]:::header

  LCompiled["Compiled<br/>current Lean gate"]:::compiled
  LPartial["Partial<br/>gate absent or interface only"]:::partial
  LStated["Stated / incomplete<br/>placeholder or contract"]:::stated
  LExternal["External dependency<br/>not ASTIS-owned"]:::external

  RPartial["Partial<br/>some evidence leaves"]:::partial
  RBlocked["Blocked<br/>named mathematical boundary"]:::blocked
  RPlanned["Planned<br/>mapped downstream route"]:::planned

  Local --> LCompiled
  Local --> LPartial
  Local --> LStated
  Local --> LExternal
  Route --> RPartial
  Route --> RBlocked
  Route --> RPlanned
  LCompiled -. does not imply .-> RPartial
  LCompiled -. does not imply .-> RBlocked

  classDef header fill:#172033,stroke:#172033,color:#ffffff,stroke-width:2px;
  classDef compiled fill:#dcecff,stroke:#155eef,color:#172033,stroke-width:2px;
  classDef partial fill:#fff2c7,stroke:#9a6700,color:#172033,stroke-width:1.5px;
  classDef stated fill:#ffead5,stroke:#b54708,color:#172033,stroke-width:1.5px;
  classDef external fill:#ece6ff,stroke:#6938ef,color:#172033,stroke-width:1.5px;
  classDef blocked fill:#ffe5e5,stroke:#c92a2a,color:#172033,stroke-width:2px;
  classDef planned fill:#eef3f9,stroke:#627086,color:#172033,stroke-width:1.5px;
The status graph distinguishes compiled leaves, partial theorem packages, blockers, plans, and external dependencies.

Milestone ledger

Chapter 1

Log-concavity and normalized Gibbs measures

CompiledPartial

The repository has local definitions and reusable leaves for positive log-concavity, Gibbs densities, finite nonzero normalization, and selected convex-potential consequences.

LogConcaveOngibbsDensityENNRealisProbabilityMeasure_withDensity_normalized_gibbslogConcaveOn_normalized_gibbsDensityENNReal_toReal_of_convexOn

Open boundary

  • The full coercivity-to-normalizability hierarchy used across the textbook is incomplete.
  • Prekopa-Leindler and Brunn-Minkowski are not locally formalized.
Chapter 1

Langevin generator and finite-dimensional weighted-divergence display

CompiledPartial

Coordinate, basis, gradient, Laplacian, and weighted-divergence identities compile locally. They establish the formal differential expression, not the operator domain or invariant law.

finiteEuclidean_langevinGenerator_coordinateDisplaycoordinateDivergence_expNeg_fderivCoordinateField_langevinGenerator_display_of_differentiableAtintegrable_expNeg_langevinGenerator_rhs_of_contDiff_of_hasCompactSupport

Open boundary

  • Closed generator and semigroup domain semantics.
Chapter 1

Whole-space weighted integration by parts and Gibbs invariance

PartialPartial

Whole-space weighted IBP, an explicit C_c^2 generator-core contract, normalized-Gibbs annihilation on that core, and an abstract semigroup/domain-to-invariance bridge compile locally. The actual Langevin semigroup does not preserve compact support, so the concrete domain extension or a uniqueness route remains open.

radialSmoothCutoff_tendsto_onetendsto_integral_radialSmoothCutoff_comp_toLp_smulintegrable_expNeg_langevinGenerator_rhs_comp_toLp_of_contDiff_of_hasCompactSupporttendsto_setIntegral_expNeg_norm_ge_comp_toLp_of_lintegral_expNeg_ne_topintegral_coordinateDivergence_wrapped_eq_zero_of_contDiff_of_hasCompactSupportintegral_expNeg_langevinGenerator_rhs_eq_zero_of_contDiff_of_hasCompactSupportCoreContractintegral_operator_normalizedGibbs_eq_zero_on_compactlySupportedC2isInvariantOn_of_integral_generator_eq_zero

Open boundary

  • Construct the concrete Langevin semigroup contract and extend Gibbs generator-mean zero from C_c^2 to a semigroup-stable domain, or prove an equivalent martingale-problem/Fokker-Planck uniqueness theorem.
Chapter 2

Poincare, log-Sobolev, transport, and dissipation

PartialPartial

Scalar KL/Fisher/Dirichlet algebra and selected log-Sobolev handoffs compile, while the analytic inequality packages and preservation hierarchy remain incomplete.

lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar

Open boundary

  • General Poincare and log-Sobolev theorem interfaces.
  • Tensorization, perturbation, transport, concentration, and isoperimetry packages.
Chapter 3

Probability kernels and conditional expectation representatives

CompiledPartial

ASTIS has exact almost-everywhere bridges between Mathlib conditional distributions, conditional-expectation kernels, mapped kernels, and selected Bochner-integral fields.

condDistribAeEqCondExpKernelMapcondDistribIntegralIntegrable

Open boundary

  • A general stochastic-process filtration and adaptedness layer.
  • Source-specific representative choices still have to be justified at each consumer.
Chapter 3

Girsanov, Doob transforms, and path-space change of measure

CompiledPartial

Finite-dimensional Gaussian cylinder likelihood and measure identities compile and provide a base case. The continuous Brownian path-space theorem has not been packaged.

finiteGaussianGirsanovCylinderMeasure_eq_withDensity

Open boundary

  • Filtered probability spaces, adapted drift, stochastic exponential, and Novikov-style conditions.
  • Brownian path-space Radon-Nikodym identity, Doob transform, and Follmer drift.
Chapter 4

Continuous Langevin process to discrete sampling algorithms

Stated/incompletePlanned

SDE and sampler contract records exist, but full LMC interpolation, convergence, stability, and error theorems are not local compiled theorem packages.

ItoDiffusionContractFokkerPlanckContractEulerMaruyamaContract

Open boundary

  • Euler/LMC transition kernel and interpolation construction.
  • Strong or weak approximation error and convergence assembly.
Chapter 5

Accelerated, high-accuracy, proximal, structured, and generative-model routes

PlannedPlanned

Chapters 5-12 are mapped as downstream consumers of shared measure, functional-inequality, stochastic-process, and discretization roots.

No local theorem evidence is claimed.

Open boundary

  • Sampler-specific kernels and correctness theorems.
  • Rate proofs with constants matching the textbook.
  • Lower-bound oracle models and diffusion-model score-error interfaces.
Chapter shared

External Lean and textbook dependencies

External/upstream dependencyPartial

Mathlib, cited textbooks, papers, and audited Lean repositories are proof sources and port references. They are never represented as ASTIS-local certificates until an owned declaration compiles.

No local theorem evidence is claimed.

Open boundary

  • Each imported idea needs an exact source theorem, license check, API comparison, and local ownership decision.