Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
Current Progress · SampleWiki detailed view

SampleWiki dependency and audit detail

This preserves the detailed dependency-first preparation path. The unified dashboard remains the coordination surface for all collaborators.

← Unified Current Progress · Open SampleWiki

Formalization progress

Source audit and Lean progress

Theorem audit, mathematical dependencies, and Lean completion are tracked separately.

9exact theorem audits
21primary theorem audits pending
4literature-open cases
34mathematical cases
Dependency-first formalization route
Phase A · active in parallel

Common Chewi Chapter 1 interfaces

  1. Finish the Chapter 1.1 Ito/SDE/Markov-process route already owned by the existing Chapter 1 branches.
  2. Reuse the Chapter 1.2-1.3 semigroup, carre-du-champ, transport, and Wasserstein roots from the existing foundation lane.
  3. Add a regularity-aware relative-Fisher interface and KL/Fisher dissipation.
  4. Close Chewi Theorem 1.4.5 and its Fisher-Wasserstein first-order consequence.
Phase B · next shared spine

Proximal-sampler analytic spine

  1. Chewi Theorem 8.3.1 simultaneous f-divergence flow.
  2. Forward/backward heat-flow specializations and W2 contraction/time reversal.
  3. Chewi Theorem 8.4.1 ideal proximal sampler under log-concavity.
  4. Chewi Theorems 8.5.1/8.5.2 and Corollary 8.6.3.
Phase C · after shared Chapter 1 roots

Classical LMC / ULD / MALA roots

  1. Chewi 4.2.7, 4.3.6, 4.3.11.
  2. Chewi 5.3.17, 6.1.2, 6.3.2.
  3. Chewi 7.3.5 and 7.6.5.
Phase D · blocked by B

Frontier proximal/FORS implementation

  1. Chen-Chewi-Daskalakis-Rakhlin Theorem G.1, with inherited RGO-error tracking made explicit.
Phase E · blocked by A/C plus path-law interfaces

Exact ULD / FORS

  1. Girsanov path density and FORS estimator.
  2. Single-step Renyi error and error composition.
  3. Chen-Chewi-Rakhlin-Zhang Theorem 3.2.
Phase F · blocked by A/E

Non-log-concave Fisher frontier

  1. Chewi Theorem 11.2.1 and Fisher convexity/averaging.
  2. High-accuracy RGO reduction (Theorem 6.1 in the FORS paper).
  3. Chen-Chewi-Rakhlin-Zhang Theorem 6.2.
  4. Chewi 11.4.3/11.4.4 lower bounds after an oracle-complexity interface exists.
Phase G · later shared oracle lane

Stochastic and finite-sum oracle results

  1. Formalize the stochastic-gradient/finite-sum oracle model first.
  2. Then Chewi 10.1.2/10.1.3 and the COLT 2026 upper/lower bounds.
Phase H · later geometry lane

Weak-smooth and mirror geometry

  1. Formalize Bregman/mirror geometry and reuse the Chapter 1 Ito formula.
  2. Then Chewi 10.3.28 and the weak-smooth frontier cases.
Phase I · later oracle/geometry lane

Convex-body membership-oracle branch

  1. Build convex-body and membership-query interfaces.
  2. Then Kook-Zhang and Kook-Vempala warm-start/annealing results.
Case audit index
Convex body + membership oracle
Log-smooth + PI or LSI
Weakly smooth log-concave
Log-concave + log-smooth
Smooth non-log-concave + Fisher accuracy
Stochastic and finite-sum oracles
Strongly log-concave + log-smooth