Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d
Markov Chain Monte Carlo · external extension shelf

OpenAI Math routes for Markov Chain Monte Carlo

These routes are placed beside the chapters that can explain or consume them. They do not alter the primary source's chapter numbering, and they remain external until a reviewed ASTIS adapter or theorem compiles.

Back to Markov Chain Monte Carlo All seven libraries

Extended chapters

  • E1 — Metric geometry of Markov chains (Samplinglib extension; not a source-text chapter)
  • E2 — Discrete chains beyond the source text (Samplinglib extension; not a source-text chapter)
8 mapped routes

Chapter and extension placement

Comparator-backed upstream endpointOpenAI Math result 238

Binary-sweep contraction and mixing

A discrete finite-chain theorem; no Langevin/SDE interpretation is inferred.

Samplinglib placement

  • Markov Chain Monte Carlo: Chapter 2, Extended E2: Discrete chains beyond the source text — Reversible-chain contraction belongs to the method view, with discrete state explicit.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)
  • OAI.binary_sweep_contraction_and_mixing
Comparator-backed, partial familyOpenAI Math result 238

Conditional information under coordinate sweeps

Conditional-information endpoints do not by themselves prove the entire Thorp mixing family.

Samplinglib placement

  • Markov Chain Monte Carlo: Chapter 2, Extended E2: Discrete chains beyond the source text — Systematic scans are an MCMC mechanism, but this route is a card-shuffle source theorem.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)
  • OAI.CoordinateSweeps.conditional_main
  • OAI.CoordinateSweeps.all_grid_moment
Comparator-backed upstream endpointOpenAI Math result 131

Rapid mixing of graph switches

Connectivity, spectral/comparison estimates and TV mixing remain separate proof obligations.

Samplinglib placement

  • Markov Chain Monte Carlo: Chapter 2, Extended E2: Discrete chains beyond the source text — The switch chain is a reversible MCMC case study.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)
  • OAI.Problem315.switch_chain_main
  • OAI.Problem315.switch_chain_tv_bound
  • OAI.Problem315.switch_connectivity
Comparator-backed, partial familyOpenAI Math result 238

Optimal logarithmic mixing of the Thorp shuffle

The family has multiple comparator endpoints; routing, compatibility, energy decay and final mixing must not be flattened into one implication.

Samplinglib placement

  • Markov Chain Monte Carlo: Chapter 2, Extended E2: Discrete chains beyond the source text — It illustrates mixing analysis outside the MCMC source text.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)
  • OAI.Thorp.Current.first_reciprocal_main
  • OAI.ThorpResults.remaining_main
  • OAI.ThorpNine.main
  • OAI.ThorpCompatibility.weightedCompatibility_main
Comparator-backed upstream endpointOpenAI Math result 227

Critical SK heat-bath/Glauber mixing

Spin-glass-specific hypotheses are source binders; generic Dirichlet, entropy or TV leaves may be extracted only after audit.

Samplinglib placement

  • Markov Chain Monte Carlo: Chapter 2, Chapter 5, Extended E2: Discrete chains beyond the source text — The heat-bath chain belongs to reversible/continuous-time MCMC with a discrete target.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)
  • OAI.CriticalSK.critical_mixing_bounds
Comparator linked by upstream result noteOpenAI Math result 229

Three-state reconstruction above the Kesten-Stigum threshold

Upstream Lean covers only the supercritical direction; non-reconstruction, equality and stochastic-block-model consequences remain outside the selected statements.

Samplinglib placement

  • Markov Chain Monte Carlo: Extended E2: Discrete chains beyond the source text — This is a discrete probabilistic threshold, not automatically an MCMC mixing theorem.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Comparator-backed upstream endpointOpenAI Math result 327

Markov type characterizes superreflexivity

Markov type is metric/Banach geometry of chains; it is not an invariant-law or convergence theorem for an arbitrary MCMC kernel.

Samplinglib placement

  • Markov Chain Monte Carlo: Extended E1: Metric geometry of Markov chains — The metric geometry of chains deserves a separate extension rather than insertion into the applied source text.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)
  • OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm
Manuscript only in this auditOpenAI Math result 332

Metric Markov cotype two for l1

No result-specific Lean document or comparator-backed endpoint was found in the audited snapshot.

Samplinglib placement

  • Markov Chain Monte Carlo: Extended E1: Metric geometry of Markov chains — It belongs beside Markov type as metric chain geometry, not as a standard MCMC result.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.