OAI/Combinatorics/ContingencyTables/Dense/DenseMetropolisProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A polynomial binary program for a full dense Metropolis step

  1. abbrev OAI.ContingencyTables.DensePrograms.FlatStepData line 11
  2. def OAI.ContingencyTables.DensePrograms.replaceFlat line 13
  3. def OAI.ContingencyTables.DensePrograms.replaceFlatRealizer line 16
  4. lemma OAI.ContingencyTables.DensePrograms.polynomial_replaceFlat line 19
  5. def OAI.ContingencyTables.DensePrograms.flatAcceptCandidate line 24
  6. def OAI.ContingencyTables.DensePrograms.flatAcceptCandidateRealizer line 28
  7. theorem OAI.ContingencyTables.DensePrograms.polynomial_flatAcceptCandidate line 38
  8. def OAI.ContingencyTables.DensePrograms.flatStepCandidate line 53
  9. def OAI.ContingencyTables.DensePrograms.flatStepCandidateRealizer line 56
  10. theorem OAI.ContingencyTables.DensePrograms.polynomial_flatStepCandidate line 63
  11. def OAI.ContingencyTables.DensePrograms.flatMetropolisStep line 74
  12. def OAI.ContingencyTables.DensePrograms.flatMetropolisStepRealizer line 77
  13. theorem OAI.ContingencyTables.DensePrograms.polynomial_flatMetropolisStep line 83

    Source documentation

    Includes proposal decoding, exact integer exponent evaluation and the independent acceptance word. Every finite input terminates in polynomial time.

    theorem polynomial_flatMetropolisStep : PolynomialTime flatMetropolisStepRealizer :=
…

    Mentions: OAI.ContingencyTables.DensePrograms.flatMetropolisStepRealizer