Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
Discrete Sampling · Source section 9

Methods for Establishing 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

01

Source audit

Definitions, theorems, assumptions, proof route, and exact anchors.

02

Upstream alignment

Search PMF/measure/kernel, finite matrix, conditional probability, variance and entropy APIs before adding route-local definitions.

03

Frontier Cells

Only genuinely missing mathematical edges become theorem-sized tasks.

04

Graph placement

Dependencies, consumers, cross-library bridges, and reusable shared interfaces.

arXiv:2307.13826v4 · printed/PDF p. 57 ↗

This page establishes a stable source route and truth boundary; it does not claim a completed formalization.

Mathematical orientation

\[\sup_{\tau\text{ feasible}}\lambda_{\max}(\Psi_{\mu^\tau})\leq\eta\]

Treat correlation decay, zero-freeness, coupling independence and relaxation-time methods as different sufficient routes. Specify model, degree, boundary conditions and all pinnings; one covariance calculation is insufficient.

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. §9.1 · Preliminaries printed/PDF p. 57
  2. §9.1.1 · Hard-core model printed/PDF p. 57
  3. §9.1.2 · Tree-uniqueness threshold printed/PDF p. 57
  4. §9.1.3 · Spectral independence printed/PDF p. 58
  5. §9.1.4 · Relating influences and occupancy ratios printed/PDF p. 59
  6. §9.2 · Spectral Independence via Correlation Decay printed/PDF p. 60
  7. §9.2.1 · Proof approach printed/PDF p. 60
  8. §9.2.2 · Self-avoiding walk tree printed/PDF p. 61
  9. §9.2.3 · Bounding influences on trees printed/PDF p. 64
  10. §9.3 · Spectral Independence via Zero-Freeness printed/PDF p. 69
  11. §9.3.1 · Some preliminaries printed/PDF p. 69
  12. §9.3.2 · Proof approach printed/PDF p. 70
  13. §9.3.3 · Proofs printed/PDF p. 70
  14. §9.4 · Spectral Independence via Coupling Independence printed/PDF p. 72
  15. §9.5 · Optimal relaxation time implies SI printed/PDF p. 76
  16. §9.5.1 · Contractive coupling implies relaxation time printed/PDF p. 77

← Previous · Book contents · Next →

Shared route · Conceptual bridges