7.3 · Book p. 193 · PDF p. 205
An Overview of High-Accuracy Samplers
Organizes high-accuracy samplers by proposal, correction, initialization, and metric-conversion requirements.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward The Metropolis-Hastings correction preserves the target through detailed balance. The declaration-level source map is intentionally left inside the formalization layer until exact theorem anchors have been audited.
Why is this valid?
Chapter-level validity conditions
- Kernel measurability and exceptional zero-density cases must be defined.
- Detailed balance is a measure identity, not merely a pointwise density calculation.
- Cold-start arguments require smoothing or explicit initialization bounds.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.