OAI/Combinatorics/ContingencyTables/Transport/BoundedProfileWalk.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

A polynomial loop for the encoded small-profile walk

  1. def OAI.ContingencyTables.ProfilePrograms.capView line 10
  2. def OAI.ContingencyTables.ProfilePrograms.capViewRealizer line 13
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_capView line 18
  4. lemma OAI.ContingencyTables.ProfilePrograms.capView_weight line 25
  5. lemma OAI.ContingencyTables.ProfilePrograms.capView_eq line 36
  6. def OAI.ContingencyTables.ProfilePrograms.capViews line 44
  7. def OAI.ContingencyTables.ProfilePrograms.capBounds line 47
  8. def OAI.ContingencyTables.ProfilePrograms.capBoundsRealizer line 50
  9. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_capBounds line 56
  10. def OAI.ContingencyTables.ProfilePrograms.capViewsRealizer line 61
  11. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_capViews line 65
  12. abbrev OAI.ContingencyTables.ProfilePrograms.ProfileConfiguration line 72
  13. abbrev OAI.ContingencyTables.ProfilePrograms.ProfileWord line 73
  14. def OAI.ContingencyTables.ProfilePrograms.currentParameters line 75
  15. def OAI.ContingencyTables.ProfilePrograms.currentParametersRealizer line 78
  16. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_currentParameters line 83
  17. def OAI.ContingencyTables.ProfilePrograms.boundedNext line 90
  18. def OAI.ContingencyTables.ProfilePrograms.boundedNextRealizer line 93
  19. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_boundedNext line 100
  20. def OAI.ContingencyTables.ProfilePrograms.advanceProfile line 109
  21. def OAI.ContingencyTables.ProfilePrograms.advanceProfileRealizer line 112
  22. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_advanceProfile line 117
  23. lemma OAI.ContingencyTables.ProfilePrograms.advanceProfile_weight line 121
  24. def OAI.ContingencyTables.ProfilePrograms.profileWalk line 138
  25. def OAI.ContingencyTables.ProfilePrograms.profileWalkRealizer line 141
  26. lemma OAI.ContingencyTables.ProfilePrograms.profileFold_fixed line 144
  27. lemma OAI.ContingencyTables.ProfilePrograms.profileFold_weight line 150
  28. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileWalk line 164