OAI/Combinatorics/ContingencyTables/Counting/CountingInputParser.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Parsing the public cell-bounded counting input

Dimensions only delimit bounded list slices. The matrix layout uses the lengths of the parsed margin lists, so malformed headers do not create unbounded numeric loops. Positive rational parameters use their natural numerator and denominator, exactly as in the public tape encoding.

  1. abbrev OAI.ContingencyTables.CountingInputParser.Input line 19
  2. def OAI.ContingencyTables.CountingInputParser.offset line 21
  3. def OAI.ContingencyTables.CountingInputParser.offsetRealizer line 23
  4. lemma OAI.ContingencyTables.CountingInputParser.polynomial_offset line 26
  5. def OAI.ContingencyTables.CountingInputParser.rest line 33
  6. def OAI.ContingencyTables.CountingInputParser.restRealizer line 34
  7. lemma OAI.ContingencyTables.CountingInputParser.polynomial_rest line 35
  8. def OAI.ContingencyTables.CountingInputParser.cells line 38
  9. def OAI.ContingencyTables.CountingInputParser.cellsRealizer line 40
  10. lemma OAI.ContingencyTables.CountingInputParser.polynomial_cells line 43
  11. def OAI.ContingencyTables.CountingInputParser.capacityFrame line 50
  12. def OAI.ContingencyTables.CountingInputParser.capacityFrameRealizer line 53
  13. lemma OAI.ContingencyTables.CountingInputParser.polynomial_capacityFrame line 62
  14. def OAI.ContingencyTables.CountingInputParser.parameters line 70
  15. def OAI.ContingencyTables.CountingInputParser.parametersRealizer line 71
  16. lemma OAI.ContingencyTables.CountingInputParser.polynomial_parameters line 73
  17. def OAI.ContingencyTables.CountingInputParser.fractionPair line 76
  18. def OAI.ContingencyTables.CountingInputParser.fractionPairRealizer line 78
  19. lemma OAI.ContingencyTables.CountingInputParser.polynomial_fractionPair line 82
  20. def OAI.ContingencyTables.CountingInputParser.decode line 91
  21. def OAI.ContingencyTables.CountingInputParser.decodeRealizer line 93
  22. lemma OAI.ContingencyTables.CountingInputParser.polynomial_decode line 97
  23. def OAI.ContingencyTables.CountingInputParser.parseInput line 102
  24. def OAI.ContingencyTables.CountingInputParser.publicRealizer line 103
  25. lemma OAI.ContingencyTables.CountingInputParser.polynomial_public line 105
  26. lemma OAI.ContingencyTables.CountingInputParser.decode_blocks line 108
  27. lemma OAI.ContingencyTables.CountingInputParser.encodeMatrix_words line 126
  28. lemma OAI.ContingencyTables.CountingInputParser.parse_public line 136
  29. lemma OAI.ContingencyTables.CountingInputParser.public_spec line 148