OAI/Combinatorics/ContingencyTables/Counting/CompanionMetropolisWordProgram.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Bounded slicing of one flat companion transition word

  1. abbrev OAI.ContingencyTables.CompanionMetropolisWordProgram.Input line 13

    Source documentation

    The fixed frame, the acceptance precision, current code, and fresh word.

    abbrev Input := ((CompanionMetropolisProgram.Frame × ℕ) × List ℕ) × List Bool

    Mentions: OAI.ContingencyTables.CompanionMetropolisProgram.Frame

  2. def OAI.ContingencyTables.CompanionMetropolisWordProgram.proposalWidth line 15
  3. def OAI.ContingencyTables.CompanionMetropolisWordProgram.proposalWidthRealizer line 16
  4. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.polynomial_proposalWidth line 23
  5. def OAI.ContingencyTables.CompanionMetropolisWordProgram.context line 33
  6. def OAI.ContingencyTables.CompanionMetropolisWordProgram.contextRealizer line 34
  7. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.polynomial_context line 36
  8. def OAI.ContingencyTables.CompanionMetropolisWordProgram.queryWidth line 42
  9. def OAI.ContingencyTables.CompanionMetropolisWordProgram.queryWidthRealizer line 43
  10. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.polynomial_queryWidth line 50
  11. def OAI.ContingencyTables.CompanionMetropolisWordProgram.firstOffset line 58

    Source documentation

    Offsets are computed in binary; the physical take/drop calls remain bounded by the supplied word on every malformed input.

    def firstOffset (z : Input) : ℕ := 1+proposalWidth z

    Mentions: OAI.ContingencyTables.CompanionMetropolisWordProgram.Input, OAI.ContingencyTables.CompanionMetropolisWordProgram.proposalWidth

  12. def OAI.ContingencyTables.CompanionMetropolisWordProgram.firstOffsetRealizer line 59
  13. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.polynomial_firstOffset line 62
  14. def OAI.ContingencyTables.CompanionMetropolisWordProgram.secondOffset line 65
  15. def OAI.ContingencyTables.CompanionMetropolisWordProgram.secondOffsetRealizer line 68
  16. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.polynomial_secondOffset line 71
  17. def OAI.ContingencyTables.CompanionMetropolisWordProgram.coinOffset line 74
  18. def OAI.ContingencyTables.CompanionMetropolisWordProgram.coinOffsetRealizer line 77
  19. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.polynomial_coinOffset line 80
  20. def OAI.ContingencyTables.CompanionMetropolisWordProgram.slice line 83
  21. def OAI.ContingencyTables.CompanionMetropolisWordProgram.sliceRealizer line 85
  22. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.polynomial_slice line 88
  23. def OAI.ContingencyTables.CompanionMetropolisWordProgram.fields line 94
  24. def OAI.ContingencyTables.CompanionMetropolisWordProgram.fieldsRealizer line 99
  25. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.polynomial_fields line 105
  26. def OAI.ContingencyTables.CompanionMetropolisWordProgram.stepInput line 114
  27. def OAI.ContingencyTables.CompanionMetropolisWordProgram.stepInputRealizer line 115
  28. lemma OAI.ContingencyTables.CompanionMetropolisWordProgram.polynomial_stepInput line 117
  29. def OAI.ContingencyTables.CompanionMetropolisWordProgram.output line 123
  30. def OAI.ContingencyTables.CompanionMetropolisWordProgram.outputRealizer line 124
  31. theorem OAI.ContingencyTables.CompanionMetropolisWordProgram.polynomial_output line 127