OAI/Combinatorics/ContingencyTables/Sampling/UnitProfileProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The bounded profile program for the all-small branch

  1. abbrev OAI.ContingencyTables.ProfilePrograms.UnitStepInput line 10
  2. def OAI.ContingencyTables.ProfilePrograms.unitCandidateInput line 12
  3. def OAI.ContingencyTables.ProfilePrograms.unitCandidateInputRealizer line 14
  4. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitCandidateInput line 17
  5. def OAI.ContingencyTables.ProfilePrograms.unitNext line 21
  6. def OAI.ContingencyTables.ProfilePrograms.unitNextRealizer line 23
  7. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitNext line 30
  8. def OAI.ContingencyTables.ProfilePrograms.unitAdvance line 36
  9. def OAI.ContingencyTables.ProfilePrograms.unitAdvanceRealizer line 38
  10. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitAdvance line 42
  11. lemma OAI.ContingencyTables.ProfilePrograms.unitAdvance_weight line 46
  12. def OAI.ContingencyTables.ProfilePrograms.unitProfileWalk line 63
  13. def OAI.ContingencyTables.ProfilePrograms.unitProfileWalkRealizer line 66
  14. lemma OAI.ContingencyTables.ProfilePrograms.unitFold_fixed line 69
  15. lemma OAI.ContingencyTables.ProfilePrograms.unitFold_weight line 75
  16. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_unitProfileWalk line 89