OAI/Combinatorics/ContingencyTables/Sampling/OriginalTableEnumeration.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Enumerating original tables by all their bounded entries

  1. def OAI.ContingencyTables.ProfilePrograms.originalLayoutMargins line 12

    Source documentation

    Dummy leading margins reuse the rectangular free-array layout only.

    def originalLayoutMargins (z : CompletionMargins) : CompletionMargins := (0::z.1,0::z.2)
  2. def OAI.ContingencyTables.ProfilePrograms.originalLayoutMarginsRealizer line 14
  3. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_originalLayoutMargins line 20
  4. def OAI.ContingencyTables.ProfilePrograms.originalFreeMatrix line 25
  5. def OAI.ContingencyTables.ProfilePrograms.originalFreeMatrixRealizer line 28
  6. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_originalFreeMatrix line 31
  7. def OAI.ContingencyTables.ProfilePrograms.originalCandidate line 36
  8. def OAI.ContingencyTables.ProfilePrograms.originalCandidateRealizer line 40
  9. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_originalCandidate line 44
  10. def OAI.ContingencyTables.ProfilePrograms.originalEnumerationData line 49
  11. def OAI.ContingencyTables.ProfilePrograms.originalEnumerationDataRealizer line 52
  12. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_originalEnumerationData line 55
  13. def OAI.ContingencyTables.ProfilePrograms.originalCandidates line 58
  14. def OAI.ContingencyTables.ProfilePrograms.originalCandidatesRealizer line 61
  15. def OAI.ContingencyTables.ProfilePrograms.originalEnumerationMeasure line 65
  16. lemma OAI.ContingencyTables.ProfilePrograms.work_originalCandidates line 68