OAI/Combinatorics/ContingencyTables/Counting/CompanionBoundedWalkProgram.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Polynomial iteration of the physical companion transition

Clipping is redundant on the encoded binary chain states. It gives a uniform bound on malformed inputs, so repeated calls remain polynomial.

  1. abbrev OAI.ContingencyTables.CompanionBoundedWalkProgram.Fixed line 16
  2. abbrev OAI.ContingencyTables.CompanionBoundedWalkProgram.State line 17
  3. def OAI.ContingencyTables.CompanionBoundedWalkProgram.transitionInput line 19
  4. def OAI.ContingencyTables.CompanionBoundedWalkProgram.transitionInputRealizer line 21
  5. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.polynomial_transitionInput line 23
  6. def OAI.ContingencyTables.CompanionBoundedWalkProgram.candidate line 27
  7. def OAI.ContingencyTables.CompanionBoundedWalkProgram.candidateRealizer line 28
  8. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.polynomial_candidate line 31
  9. def OAI.ContingencyTables.CompanionBoundedWalkProgram.bound line 34
  10. def OAI.ContingencyTables.CompanionBoundedWalkProgram.boundRealizer line 35
  11. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.polynomial_bound line 37
  12. def OAI.ContingencyTables.CompanionBoundedWalkProgram.next line 43
  13. def OAI.ContingencyTables.CompanionBoundedWalkProgram.nextRealizer line 44
  14. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.polynomial_next line 48
  15. def OAI.ContingencyTables.CompanionBoundedWalkProgram.advance line 52
  16. def OAI.ContingencyTables.CompanionBoundedWalkProgram.advanceRealizer line 53
  17. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.polynomial_advance line 54
  18. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.advance_fixed line 57
  19. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.advance_weight line 59
  20. def OAI.ContingencyTables.CompanionBoundedWalkProgram.walk line 70
  21. def OAI.ContingencyTables.CompanionBoundedWalkProgram.walkRealizer line 72
  22. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.fold_fixed line 74
  23. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.fold_weight line 80
  24. theorem OAI.ContingencyTables.CompanionBoundedWalkProgram.polynomial_walk line 91
  25. abbrev OAI.ContingencyTables.CompanionBoundedWalkProgram.RecordState line 98
  26. def OAI.ContingencyTables.CompanionBoundedWalkProgram.recordAdvance line 100
  27. def OAI.ContingencyTables.CompanionBoundedWalkProgram.recordAdvanceRealizer line 103
  28. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.polynomial_recordAdvance line 108
  29. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.recordFold_bounds_fixed line 119
  30. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.recordFold_weight line 137
  31. def OAI.ContingencyTables.CompanionBoundedWalkProgram.recordWalk line 150
  32. def OAI.ContingencyTables.CompanionBoundedWalkProgram.recordWalkRealizer line 152
  33. theorem OAI.ContingencyTables.CompanionBoundedWalkProgram.polynomial_recordWalk line 154
  34. def OAI.ContingencyTables.CompanionBoundedWalkProgram.initialRecord line 164
  35. def OAI.ContingencyTables.CompanionBoundedWalkProgram.initialRecordRealizer line 165
  36. lemma OAI.ContingencyTables.CompanionBoundedWalkProgram.polynomial_initialRecord line 167
  37. def OAI.ContingencyTables.CompanionBoundedWalkProgram.history line 171
  38. def OAI.ContingencyTables.CompanionBoundedWalkProgram.historyRealizer line 173
  39. theorem OAI.ContingencyTables.CompanionBoundedWalkProgram.polynomial_history line 178