OAI/Combinatorics/ContingencyTables/Transport/MetropolisChain.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite weighted Metropolis chain

The holding probability, stationary law, and cut flow are proved from positive weights, symmetric proposals, and the proposal-degree bound. Only the final Poincaré consequence uses the explicit published Cheeger input.

  1. def OAI.ContingencyTables.MetropolisChain.normalizer line 22
  2. theorem OAI.ContingencyTables.MetropolisChain.normalizer_pos line 24
  3. def OAI.ContingencyTables.MetropolisChain.move line 27
  4. theorem OAI.ContingencyTables.MetropolisChain.accept_mass line 30
  5. theorem OAI.ContingencyTables.MetropolisChain.move_nonnegative line 35
  6. theorem OAI.ContingencyTables.MetropolisChain.move_reversible line 44
  7. theorem OAI.ContingencyTables.MetropolisChain.move_row_bound line 62
  8. def OAI.ContingencyTables.MetropolisChain.chain line 79
  9. theorem OAI.ContingencyTables.MetropolisChain.chain_flow line 91
  10. theorem OAI.ContingencyTables.MetropolisChain.chain_cut_flow line 108
  11. theorem OAI.ContingencyTables.MetropolisChain.poincare_of_weighted_cut line 127