Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 6
Optimal Mixing Time for Glauber from Spectral Independence
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
\[\operatorname{Ent}_\pi(r)=\sum_x\pi(x)r(x)\log r(x),\qquad \sum_x\pi(x)r(x)=1\]
Distinguish variance factorization, entropy factorization, log-Sobolev and modified log-Sobolev inequalities. The reference measure and clock determine constants; converting a relaxation bound into mixing needs its own theorem.
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
- §6.1 · Uniform Block Dynamics printed/PDF p. 37
- §6.2 · Improved Random Walk Theorem printed/PDF p. 37
- §6.3 · Fast Mixing of Uniform Block Dynamics printed/PDF p. 38
- §6.4 · Shattering printed/PDF p. 38
- §6.5 · Optimal Relaxation Time of Glauber: Proof of Theorem 1.5 printed/PDF p. 39
- §6.6 · Improved Random Walk Theorem: Proof of Theorem 6.1 printed/PDF p. 41
- §6.7 · Proofs of Basic Facts for Dirichlet Form and Variance printed/PDF p. 43
- §6.8 · Optimal Mixing Time via Entropy Decay printed/PDF p. 45