OAI/Combinatorics/ContingencyTables/Sampling/SmallMarginTestProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Polynomial residual-margin inequality and equality tests

  1. abbrev OAI.ContingencyTables.ProfilePrograms.MarginCheckData line 10
  2. def OAI.ContingencyTables.ProfilePrograms.marginList line 12
  3. def OAI.ContingencyTables.ProfilePrograms.marginListRealizer line 15
  4. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_marginList line 19
  5. def OAI.ContingencyTables.ProfilePrograms.lineArgument line 24
  6. def OAI.ContingencyTables.ProfilePrograms.lineArgumentRealizer line 27
  7. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_lineArgument line 31
  8. def OAI.ContingencyTables.ProfilePrograms.marginValueRealizer line 36
  9. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_marginValue line 40
  10. def OAI.ContingencyTables.ProfilePrograms.lineValueRealizer line 45
  11. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_lineValue line 50
  12. def OAI.ContingencyTables.ProfilePrograms.validMarginAt line 53
  13. def OAI.ContingencyTables.ProfilePrograms.validMarginAtRealizer line 58
  14. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_validMarginAt line 70
  15. def OAI.ContingencyTables.ProfilePrograms.marginIndices line 80
  16. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_marginIndices line 84
  17. def OAI.ContingencyTables.ProfilePrograms.validMargins line 93
  18. def OAI.ContingencyTables.ProfilePrograms.validMarginsRealizer line 96
  19. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_validMargins line 102
  20. theorem OAI.ContingencyTables.ProfilePrograms.validMargins_iff line 108