OAI/Combinatorics/ContingencyTables/Machines/PairedProfileProgram.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Reading the two cell counts from the actual paired code

The block widths come from the stored capacity list. Each count scans only supplied code entries and clips them to one, including on malformed input. No numeric capacity controls an unbounded allocation.

  1. abbrev OAI.ContingencyTables.PairedProfileProgram.ReadInput line 17
  2. def OAI.ContingencyTables.PairedProfileProgram.sideValue line 19
  3. def OAI.ContingencyTables.PairedProfileProgram.sideValueRealizer line 21
  4. lemma OAI.ContingencyTables.PairedProfileProgram.polynomial_sideValue line 28
  5. def OAI.ContingencyTables.PairedProfileProgram.sideEntries line 37
  6. def OAI.ContingencyTables.PairedProfileProgram.sideEntriesRealizer line 39
  7. lemma OAI.ContingencyTables.PairedProfileProgram.polynomial_sideEntries line 42
  8. def OAI.ContingencyTables.PairedProfileProgram.sideCount line 47
  9. def OAI.ContingencyTables.PairedProfileProgram.sideCountRealizer line 48
  10. lemma OAI.ContingencyTables.PairedProfileProgram.polynomial_sideCount line 49
  11. lemma OAI.ContingencyTables.PairedProfileProgram.sideCount_le line 52
  12. abbrev OAI.ContingencyTables.PairedProfileProgram.Input line 62
  13. def OAI.ContingencyTables.PairedProfileProgram.width line 64
  14. def OAI.ContingencyTables.PairedProfileProgram.widthRealizer line 65
  15. lemma OAI.ContingencyTables.PairedProfileProgram.polynomial_width line 68
  16. def OAI.ContingencyTables.PairedProfileProgram.rows line 72
  17. def OAI.ContingencyTables.PairedProfileProgram.rowsRealizer line 74
  18. lemma OAI.ContingencyTables.PairedProfileProgram.polynomial_rows line 77
  19. def OAI.ContingencyTables.PairedProfileProgram.counts line 82
  20. def OAI.ContingencyTables.PairedProfileProgram.countsRealizer line 83
  21. lemma OAI.ContingencyTables.PairedProfileProgram.polynomial_counts line 88
  22. def OAI.ContingencyTables.PairedProfileProgram.profileRows line 95
  23. def OAI.ContingencyTables.PairedProfileProgram.profileRowsRealizer line 96
  24. theorem OAI.ContingencyTables.PairedProfileProgram.polynomial_profileRows line 97
  25. def OAI.ContingencyTables.PairedProfileProgram.interleave line 100
  26. lemma OAI.ContingencyTables.PairedProfileProgram.interleave_length line 104
  27. lemma OAI.ContingencyTables.PairedProfileProgram.interleave_get_even line 109
  28. lemma OAI.ContingencyTables.PairedProfileProgram.interleave_get_odd line 120
  29. lemma OAI.ContingencyTables.PairedProfileProgram.sideEntries_interleave line 131
  30. lemma OAI.ContingencyTables.PairedProfileProgram.interleave_flatMap line 153