OAI/Combinatorics/ContingencyTables/Sampling/ProfileTransitionProgram.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

A binary small-profile transition with a fresh dense completion

  1. abbrev OAI.ContingencyTables.ProfilePrograms.ProfileStepInput line 12
  2. def OAI.ContingencyTables.ProfilePrograms.stepCheck line 14
  3. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_stepCheck line 17
  4. def OAI.ContingencyTables.ProfilePrograms.stepViews line 20
  5. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_stepViews line 24
  6. def OAI.ContingencyTables.ProfilePrograms.stepProposal line 27
  7. def OAI.ContingencyTables.ProfilePrograms.stepProposalRealizer line 30
  8. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_stepProposal line 33
  9. def OAI.ContingencyTables.ProfilePrograms.stepCandidateViews line 37
  10. def OAI.ContingencyTables.ProfilePrograms.stepCandidateViewsRealizer line 40
  11. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_stepCandidateViews line 43
  12. def OAI.ContingencyTables.ProfilePrograms.stepCandidate line 47
  13. def OAI.ContingencyTables.ProfilePrograms.stepCandidateRealizer line 50
  14. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_stepCandidate line 53
  15. def OAI.ContingencyTables.ProfilePrograms.stepCandidateParameters line 57
  16. def OAI.ContingencyTables.ProfilePrograms.stepCandidateParametersRealizer line 60
  17. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_stepCandidateParameters line 64
  18. def OAI.ContingencyTables.ProfilePrograms.stepOldMargins line 69
  19. def OAI.ContingencyTables.ProfilePrograms.stepOldMarginsRealizer line 72
  20. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_stepOldMargins line 78
  21. def OAI.ContingencyTables.ProfilePrograms.stepNewMargins line 82
  22. def OAI.ContingencyTables.ProfilePrograms.stepNewMarginsRealizer line 85
  23. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_stepNewMargins line 91
  24. def OAI.ContingencyTables.ProfilePrograms.stepCompletion line 95
  25. def OAI.ContingencyTables.ProfilePrograms.stepCompletionRealizer line 98
  26. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_stepCompletion line 102
  27. def OAI.ContingencyTables.ProfilePrograms.stepTranslation line 106
  28. def OAI.ContingencyTables.ProfilePrograms.stepTranslationRealizer line 109
  29. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_stepTranslation line 112
  30. def OAI.ContingencyTables.ProfilePrograms.profileStep line 116
  31. def OAI.ContingencyTables.ProfilePrograms.profileStepRealizer line 119
  32. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_profileStep line 124