OAI/Combinatorics/ContingencyTables/Machines/SignedPairProgram.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Binary signed arithmetic used to prepare the forest evaluator

A pair stores a difference of naturals. Arithmetic never iterates through the represented integer value, and normalization returns the exact positive/negative parts expected by the affine penalty program.

  1. abbrev OAI.ContingencyTables.SignedPairProgram.Signed line 17
  2. def OAI.ContingencyTables.SignedPairProgram.value line 19
  3. def OAI.ContingencyTables.SignedPairProgram.plus line 21
  4. def OAI.ContingencyTables.SignedPairProgram.neg line 22
  5. def OAI.ContingencyTables.SignedPairProgram.minus line 23
  6. def OAI.ContingencyTables.SignedPairProgram.times line 24
  7. def OAI.ContingencyTables.SignedPairProgram.normalize line 26
  8. lemma OAI.ContingencyTables.SignedPairProgram.value_plus line 28
  9. lemma OAI.ContingencyTables.SignedPairProgram.value_neg line 32
  10. lemma OAI.ContingencyTables.SignedPairProgram.value_minus line 36
  11. lemma OAI.ContingencyTables.SignedPairProgram.value_times line 40
  12. lemma OAI.ContingencyTables.SignedPairProgram.normalize_eq line 44
  13. lemma OAI.ContingencyTables.SignedPairProgram.value_normalize line 50
  14. def OAI.ContingencyTables.SignedPairProgram.plusRealizer line 54
  15. def OAI.ContingencyTables.SignedPairProgram.negRealizer line 59
  16. def OAI.ContingencyTables.SignedPairProgram.minusRealizer line 61
  17. def OAI.ContingencyTables.SignedPairProgram.timesRealizer line 64
  18. def OAI.ContingencyTables.SignedPairProgram.normalizeRealizer line 73
  19. lemma OAI.ContingencyTables.SignedPairProgram.polynomial_plus line 76
  20. lemma OAI.ContingencyTables.SignedPairProgram.polynomial_neg line 85
  21. lemma OAI.ContingencyTables.SignedPairProgram.polynomial_minus line 88
  22. lemma OAI.ContingencyTables.SignedPairProgram.polynomial_times line 92
  23. lemma OAI.ContingencyTables.SignedPairProgram.polynomial_normalize line 109
  24. def OAI.ContingencyTables.SignedPairProgram.sum line 113
  25. def OAI.ContingencyTables.SignedPairProgram.sumRealizer line 115
  26. lemma OAI.ContingencyTables.SignedPairProgram.polynomial_sum line 118
  27. lemma OAI.ContingencyTables.SignedPairProgram.value_sum line 123