OAI/MathematicalPhysics/ContinuumCoulomb/Programs/RationalSumProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Actual polynomial rational-list summation. Unreduced numerator and positive denominator registers are accumulated with ordinary integer arithmetic, then reduced once. Their bit lengths grow cubically at most.

  1. abbrev OAI.ContinuumCoulomb.RationalSumProgram.State line 14
  2. def OAI.ContinuumCoulomb.RationalSumProgram.stateCode line 16
  3. def OAI.ContinuumCoulomb.RationalSumProgram.step line 18
  4. def OAI.ContinuumCoulomb.RationalSumProgram.value line 21
  5. theorem OAI.ContinuumCoulomb.RationalSumProgram.step_den_pos line 23
  6. theorem OAI.ContinuumCoulomb.RationalSumProgram.step_value line 26
  7. theorem OAI.ContinuumCoulomb.RationalSumProgram.fold_den_pos line 34
  8. theorem OAI.ContinuumCoulomb.RationalSumProgram.fold_value line 40
  9. theorem OAI.ContinuumCoulomb.RationalSumProgram.integer_bits_add line 48
  10. theorem OAI.ContinuumCoulomb.RationalSumProgram.step_bits line 52
  11. theorem OAI.ContinuumCoulomb.RationalSumProgram.fold_bits line 64
  12. theorem OAI.ContinuumCoulomb.RationalSumProgram.state_length line 80
  13. theorem OAI.ContinuumCoulomb.RationalSumProgram.rational_length line 86
  14. def OAI.ContinuumCoulomb.RationalSumProgram.stepProgram line 90
  15. def OAI.ContinuumCoulomb.RationalSumProgram.foldProgram line 103
  16. def OAI.ContinuumCoulomb.RationalSumProgram.sumProgram line 131