OAI/Combinatorics/ContingencyTables/Machines/SignedFloorProgram.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Binary floor of a signed rational

Two natural quotients and the comparison of their remainders compute the exact floor. No loop depends on the numeric numerator or denominator.

  1. abbrev OAI.ContingencyTables.SignedFloorProgram.Input line 17
  2. def OAI.ContingencyTables.SignedFloorProgram.numeratorQuotient line 19
  3. def OAI.ContingencyTables.SignedFloorProgram.numeratorQuotientRealizer line 20
  4. lemma OAI.ContingencyTables.SignedFloorProgram.polynomial_numeratorQuotient line 22
  5. def OAI.ContingencyTables.SignedFloorProgram.negativeQuotient line 27
  6. def OAI.ContingencyTables.SignedFloorProgram.negativeQuotientRealizer line 28
  7. lemma OAI.ContingencyTables.SignedFloorProgram.polynomial_negativeQuotient line 30
  8. def OAI.ContingencyTables.SignedFloorProgram.carry line 35
  9. def OAI.ContingencyTables.SignedFloorProgram.carryRealizer line 36
  10. lemma OAI.ContingencyTables.SignedFloorProgram.polynomial_carry line 40
  11. def OAI.ContingencyTables.SignedFloorProgram.carryValue line 49
  12. def OAI.ContingencyTables.SignedFloorProgram.carryValueRealizer line 50
  13. lemma OAI.ContingencyTables.SignedFloorProgram.polynomial_carryValue line 52
  14. def OAI.ContingencyTables.SignedFloorProgram.raw line 55
  15. def OAI.ContingencyTables.SignedFloorProgram.rawRealizer line 56
  16. lemma OAI.ContingencyTables.SignedFloorProgram.polynomial_raw line 58
  17. def OAI.ContingencyTables.SignedFloorProgram.floorCode line 63
  18. def OAI.ContingencyTables.SignedFloorProgram.floorCodeRealizer line 64
  19. theorem OAI.ContingencyTables.SignedFloorProgram.polynomial_floorCode line 67
  20. lemma OAI.ContingencyTables.SignedFloorProgram.raw_value line 72
  21. theorem OAI.ContingencyTables.SignedFloorProgram.floorCode_value line 104
  22. abbrev OAI.ContingencyTables.SignedFloorProgram.ScaledInput line 111
  23. def OAI.ContingencyTables.SignedFloorProgram.scale line 113
  24. def OAI.ContingencyTables.SignedFloorProgram.scaleRealizer line 115
  25. lemma OAI.ContingencyTables.SignedFloorProgram.polynomial_scale line 121
  26. def OAI.ContingencyTables.SignedFloorProgram.scaledFloor line 133
  27. def OAI.ContingencyTables.SignedFloorProgram.scaledFloorRealizer line 134
  28. theorem OAI.ContingencyTables.SignedFloorProgram.polynomial_scaledFloor line 135
  29. theorem OAI.ContingencyTables.SignedFloorProgram.scaledFloor_value line 138