OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/RationalTaylorRegisters.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A shared-denominator Taylor recurrence for arbitrary rational inputs. The numerator may be signed. Register size grows polynomially in the iteration count and the encoded numerator and denominator lengths.

  1. abbrev OAI.ContinuumCoulomb.RationalTaylorRegisters.State line 15
  2. def OAI.ContinuumCoulomb.RationalTaylorRegisters.code line 17
  3. def OAI.ContinuumCoulomb.RationalTaylorRegisters.step line 20
  4. def OAI.ContinuumCoulomb.RationalTaylorRegisters.initial line 25
  5. theorem OAI.ContinuumCoulomb.RationalTaylorRegisters.iterate_initial line 27
  6. def OAI.ContinuumCoulomb.RationalTaylorRegisters.result line 66
  7. theorem OAI.ContinuumCoulomb.RationalTaylorRegisters.result_correct line 68
  8. def OAI.ContinuumCoulomb.RationalTaylorRegisters.measure line 78
  9. theorem OAI.ContinuumCoulomb.RationalTaylorRegisters.code_length line 82
  10. theorem OAI.ContinuumCoulomb.RationalTaylorRegisters.measure_le_code line 90
  11. theorem OAI.ContinuumCoulomb.RationalTaylorRegisters.code_le_measure line 95
  12. theorem OAI.ContinuumCoulomb.RationalTaylorRegisters.int_add_bits line 100
  13. theorem OAI.ContinuumCoulomb.RationalTaylorRegisters.step_measure line 104
  14. theorem OAI.ContinuumCoulomb.RationalTaylorRegisters.iterate_parameters line 124
  15. theorem OAI.ContinuumCoulomb.RationalTaylorRegisters.iterate_measure line 134
  16. theorem OAI.ContinuumCoulomb.RationalTaylorRegisters.iterate_code_bound line 148