OAI/Combinatorics/ContingencyTables/Sampling/SmallLineSumProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Binary row and column sums of the sparse stored view

  1. abbrev OAI.ContingencyTables.ProfilePrograms.LineData line 12
  2. def OAI.ContingencyTables.ProfilePrograms.lineEntry line 14
  3. def OAI.ContingencyTables.ProfilePrograms.lineEntryRealizer line 17
  4. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_lineEntry line 22
  5. def OAI.ContingencyTables.ProfilePrograms.lineIndices line 30
  6. lemma OAI.ContingencyTables.ProfilePrograms.polynomial_lineIndices line 33
  7. def OAI.ContingencyTables.ProfilePrograms.lineSum line 44
  8. def OAI.ContingencyTables.ProfilePrograms.lineSumRealizer line 47
  9. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_lineSum line 50
  10. lemma OAI.ContingencyTables.ProfilePrograms.lineSum_eq_sum line 55
  11. theorem OAI.ContingencyTables.SmallGraphProfiles.rowSum_eq line 77
  12. theorem OAI.ContingencyTables.SmallGraphProfiles.columnSum_eq line 84