OAI/Combinatorics/ContingencyTables/Sampling/OriginalTableCheck.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Binary row and column checks for original-table candidates

  1. abbrev OAI.ContingencyTables.ProfilePrograms.OriginalCheckInput line 10
  2. def OAI.ContingencyTables.ProfilePrograms.originalColumnTotals line 12
  3. def OAI.ContingencyTables.ProfilePrograms.originalColumnTotalsRealizer line 15
  4. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_originalColumnTotals line 19
  5. def OAI.ContingencyTables.ProfilePrograms.originalTableTest line 31

    Source documentation

    Applied to the fixed rectangular shape generated by the enumerator.

    def originalTableTest (z : OriginalCheckInput) : Bool :=
…

    Mentions: OAI.ContingencyTables.ProfilePrograms.OriginalCheckInput

  6. def OAI.ContingencyTables.ProfilePrograms.originalTableTestRealizer line 34
  7. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_originalTableTest line 39
  8. lemma OAI.ContingencyTables.ProfilePrograms.originalColumnTotals_code line 47
  9. lemma OAI.ContingencyTables.ProfilePrograms.originalTableTest_code line 60