OAI/Combinatorics/ContingencyTables/Dense/GridMetropolis.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual dyadic axis-proposal chain

  1. def OAI.ContingencyTables.GridBoundary.binProposal line 16
  2. theorem OAI.ContingencyTables.GridBoundary.binProposal_bounds line 18
  3. theorem OAI.ContingencyTables.GridBoundary.binProposal_degree line 38
  4. def OAI.ContingencyTables.GridBoundary.gridChain line 50
  5. theorem OAI.ContingencyTables.GridBoundary.gridChain_pi line 57