Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
Chapter 7 · Book pp. 189–213 · August 9, 2026 edition

High-Accuracy Samplers

Use accept/reject correction and conductance tools to obtain exact-target chains.

Begin with 7.1 Open this chapter in the canonical August 9 source ↗
Formal topologyOpen this chapter's Lean branches↗

Chapter route

This chapter develops proposal kernel, acceptance ratio, detailed balance, conductance. Its main destination is to connect the definitions below to the results that later chapters consume.

Core definitions

  • A rejection sampler accepts a proposal using a density-envelope ratio.
  • The Metropolis-Hastings filter corrects a proposal kernel through a reversible acceptance ratio.
  • Conductance measures the one-step flow across measurable cuts.
  • A warm start bounds the initial density ratio relative to stationarity.

Main results

  • The Metropolis-Hastings correction preserves the target through detailed balance.
  • Conductance and warmness convert local proposal quality into global mixing.
  • MALA obtains high-accuracy guarantees from both cold and warm initializations under different smoothing arguments.
  • Acceptance estimates determine the stable step-size and complexity regimes.

Contents

  1. 7.1Rejection SamplingBook p. 189
  2. 7.2The Metropolis-Hastings FilterBook p. 191
  3. 7.3An Overview of High-Accuracy SamplersBook p. 193
  4. 7.4Markov Chains in Discrete TimeBook p. 197
  5. 7.5Analysis of MALA for a Cold StartBook p. 203
  6. 7.6Analysis of MALA for a Warm StartBook p. 206
  7. 7.bibBibliographical NotesBook p. 209
  8. 7.exExercisesBook p. 211
Why is this chapter route valid?

Analytic contracts

  • 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.

Open boundaries

  • General accept/reject kernel
  • Conductance-to-mixing theorem
  • Cold-start MALA chain
View Lean formalization

These mappings are evidence links, not a claim that the entire chapter is formalized.

No declaration-level source block is mapped for this chapter yet.