OAI/Combinatorics/ContingencyTables/Counting/CompanionLabelMetadataProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Recovering each paired label's cell and capacity

The multiplicities come from the actual bounded profile blocks. A large numeric capacity never causes an allocation beyond the supplied profile code. On a canonical code, the resulting order is exactly the copy order used by the initializer and arithmetic proposals.

  1. abbrev OAI.ContingencyTables.CompanionLabelMetadataProgram.Input line 20
  2. def OAI.ContingencyTables.CompanionLabelMetadataProgram.indices line 22
  3. def OAI.ContingencyTables.CompanionLabelMetadataProgram.indicesRealizer line 23
  4. lemma OAI.ContingencyTables.CompanionLabelMetadataProgram.polynomial_indices line 25
  5. def OAI.ContingencyTables.CompanionLabelMetadataProgram.labelRow line 31
  6. def OAI.ContingencyTables.CompanionLabelMetadataProgram.labelRowRealizer line 33
  7. lemma OAI.ContingencyTables.CompanionLabelMetadataProgram.polynomial_labelRow line 36
  8. def OAI.ContingencyTables.CompanionLabelMetadataProgram.rowInput line 41
  9. def OAI.ContingencyTables.CompanionLabelMetadataProgram.rowInputRealizer line 43
  10. lemma OAI.ContingencyTables.CompanionLabelMetadataProgram.polynomial_rowInput line 47
  11. def OAI.ContingencyTables.CompanionLabelMetadataProgram.indexedRow line 51
  12. def OAI.ContingencyTables.CompanionLabelMetadataProgram.indexedRowRealizer line 52
  13. lemma OAI.ContingencyTables.CompanionLabelMetadataProgram.polynomial_indexedRow line 54
  14. def OAI.ContingencyTables.CompanionLabelMetadataProgram.output line 57
  15. def OAI.ContingencyTables.CompanionLabelMetadataProgram.outputRealizer line 59
  16. theorem OAI.ContingencyTables.CompanionLabelMetadataProgram.polynomial_output line 62
  17. lemma OAI.ContingencyTables.CompanionLabelMetadataProgram.labelRow_eq line 66
  18. lemma OAI.ContingencyTables.CompanionLabelMetadataProgram.indexedRow_encode line 76
  19. lemma OAI.ContingencyTables.CompanionLabelMetadataProgram.output_encode line 88