Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 3
Markov Chain Fundamentals
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
\[\mathcal E_P(f,g)=\frac12\sum_{x,y}\pi(x)P(x,y)(f(y)-f(x))(g(y)-g(x))\]
Pull this foundation forward before advanced spectral-independence proofs. Fix reversibility and whether the result concerns P^k or exp(t(P-I)); a positive relaxation gap is not an absolute-gap guarantee for a periodic discrete-time chain.
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
- §3.1 · Mixing Time and Total Variation Distance printed/PDF p. 19
- §3.2 · Reversibility printed/PDF p. 20
- §3.3 · Dirichlet Form and Variance printed/PDF p. 20
- §3.4 · Spectral Gap printed/PDF p. 21
- §3.5 · Approximate Tensorization of Variance printed/PDF p. 22
- §3.6 · Preliminaries printed/PDF p. 23
- §3.7 · Mixing Time Bounds via Spectral Gap printed/PDF p. 24