Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 1
Introduction
Stable source-facing chapter environment inside the shared Samplinglib reader.
scaffoldsource mapFull source closure not claimed
Planned route
Source → theorem map → reusable Lean nodes
Upstream alignment
Search PMF/measure/kernel, finite matrix, conditional probability, variance and entropy APIs before adding route-local definitions.
Frontier Cells
Only genuinely missing mathematical edges become theorem-sized tasks.
Graph placement
Dependencies, consumers, cross-library bridges, and reusable shared interfaces.
Mathematical orientation
\[\pi(\sigma)=Z^{-1}w(\sigma),\qquad Z=\sum_{\tau\in\Omega}w(\tau)\]
Start with finite support and normalization, then audit the single-site conditional update. One update chooses one site; stationarity alone is not a mixing theorem. The binary hard-core example is not all spin systems.
This is ASTIS orientation, not a verbatim theorem or completed Lean proof. Pin each source theorem, hypotheses and clock before claiming a Frontier Cell.
Section source map
- §1.1 · Setting printed/PDF p. 4
- §1.2 · Running example: Hard-core Model printed/PDF p. 4
- §1.3 · Glauber dynamics/Gibbs sampler printed/PDF p. 5
- §1.4 · Key Definitions: Spectral Independence and the Influence Matrix printed/PDF p. 7
- §1.5 · Main Results: Fast Mixing via Spectral Independence printed/PDF p. 9
- §1.6 · Application: Hard-core Model printed/PDF p. 11
- §1.7 · Methods for Establishing Spectral Independence printed/PDF p. 13
- §1.8 · Matroids and Trickle-Down Theorem printed/PDF p. 13