OAI/Combinatorics/ContingencyTables/Counting/CompanionMetropolisProgram.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

One physical companion-chain step with independent word fields

The proposed state is computed by the quadratic arithmetic candidate list. Two disjoint words evaluate the current and candidate states, and a third field supplies the rational acceptance coin.

  1. abbrev OAI.ContingencyTables.CompanionMetropolisProgram.Frame line 17
  2. abbrev OAI.ContingencyTables.CompanionMetropolisProgram.Words line 18
  3. abbrev OAI.ContingencyTables.CompanionMetropolisProgram.Input line 19
  4. def OAI.ContingencyTables.CompanionMetropolisProgram.proposed line 21
  5. def OAI.ContingencyTables.CompanionMetropolisProgram.proposedRealizer line 23
  6. lemma OAI.ContingencyTables.CompanionMetropolisProgram.polynomial_proposed line 28
  7. def OAI.ContingencyTables.CompanionMetropolisProgram.defaultCode line 33
  8. def OAI.ContingencyTables.CompanionMetropolisProgram.defaultCodeRealizer line 34
  9. lemma OAI.ContingencyTables.CompanionMetropolisProgram.polynomial_defaultCode line 37
  10. def OAI.ContingencyTables.CompanionMetropolisProgram.candidate line 42
  11. def OAI.ContingencyTables.CompanionMetropolisProgram.candidateRealizer line 43
  12. lemma OAI.ContingencyTables.CompanionMetropolisProgram.polynomial_candidate line 46
  13. def OAI.ContingencyTables.CompanionMetropolisProgram.currentInput line 52
  14. def OAI.ContingencyTables.CompanionMetropolisProgram.currentInputRealizer line 53
  15. lemma OAI.ContingencyTables.CompanionMetropolisProgram.polynomial_currentInput line 55
  16. def OAI.ContingencyTables.CompanionMetropolisProgram.targetInput line 60
  17. def OAI.ContingencyTables.CompanionMetropolisProgram.targetInputRealizer line 62
  18. lemma OAI.ContingencyTables.CompanionMetropolisProgram.polynomial_targetInput line 65
  19. def OAI.ContingencyTables.CompanionMetropolisProgram.currentValue line 72
  20. def OAI.ContingencyTables.CompanionMetropolisProgram.currentValueRealizer line 73
  21. lemma OAI.ContingencyTables.CompanionMetropolisProgram.polynomial_currentValue line 76
  22. def OAI.ContingencyTables.CompanionMetropolisProgram.targetValue line 79
  23. def OAI.ContingencyTables.CompanionMetropolisProgram.targetValueRealizer line 80
  24. lemma OAI.ContingencyTables.CompanionMetropolisProgram.polynomial_targetValue line 83
  25. def OAI.ContingencyTables.CompanionMetropolisProgram.acceptanceInput line 88
  26. def OAI.ContingencyTables.CompanionMetropolisProgram.acceptanceInputRealizer line 90
  27. lemma OAI.ContingencyTables.CompanionMetropolisProgram.polynomial_acceptanceInput line 93
  28. def OAI.ContingencyTables.CompanionMetropolisProgram.accepted line 98
  29. def OAI.ContingencyTables.CompanionMetropolisProgram.acceptedRealizer line 99
  30. lemma OAI.ContingencyTables.CompanionMetropolisProgram.polynomial_accepted line 102
  31. def OAI.ContingencyTables.CompanionMetropolisProgram.output line 107
  32. def OAI.ContingencyTables.CompanionMetropolisProgram.outputRealizer line 108
  33. theorem OAI.ContingencyTables.CompanionMetropolisProgram.polynomial_output line 111
  34. lemma OAI.ContingencyTables.CompanionMetropolisProgram.output_hold line 117