OAI/MathematicalPhysics/ContinuumCoulomb/Programs/DyadicRootProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A computed dyadic square root of a nonnegative rational, with strict error below one unit in the requested binary precision. Precision is unary; numerator, denominator, and result are binary.

  1. def OAI.ContinuumCoulomb.DyadicRootProgram.value line 13
  2. theorem OAI.ContinuumCoulomb.DyadicRootProgram.value_error line 16
  3. abbrev OAI.ContinuumCoulomb.DyadicRootProgram.Input line 58
  4. def OAI.ContinuumCoulomb.DyadicRootProgram.rawCode line 60
  5. def OAI.ContinuumCoulomb.DyadicRootProgram.precisionProgram line 62
  6. def OAI.ContinuumCoulomb.DyadicRootProgram.numeratorProgram line 65
  7. def OAI.ContinuumCoulomb.DyadicRootProgram.denominatorProgram line 69
  8. def OAI.ContinuumCoulomb.DyadicRootProgram.powerProgram line 73
  9. def OAI.ContinuumCoulomb.DyadicRootProgram.squareProgram line 77
  10. def OAI.ContinuumCoulomb.DyadicRootProgram.quotientProgram line 80
  11. def OAI.ContinuumCoulomb.DyadicRootProgram.rootNumeratorProgram line 85
  12. def OAI.ContinuumCoulomb.DyadicRootProgram.rawProgram line 89
  13. def OAI.ContinuumCoulomb.DyadicRootProgram.fractionParameters line 96
  14. def OAI.ContinuumCoulomb.DyadicRootProgram.parameters line 99
  15. theorem OAI.ContinuumCoulomb.DyadicRootProgram.parameters_length line 102
  16. def OAI.ContinuumCoulomb.DyadicRootProgram.inputProgram line 111
  17. def OAI.ContinuumCoulomb.DyadicRootProgram.output line 121
  18. def OAI.ContinuumCoulomb.DyadicRootProgram.rationalOutput line 124
  19. def OAI.ContinuumCoulomb.DyadicRootProgram.certificate line 132

    Source documentation

    A concrete polynomial machine emits the canonical numerator and denominator of the certified dyadic approximation.

    noncomputable def certificate :
    Turing.TM2ComputableInPolyTime parameters.encode output.encode
      (fun x => ((value x.1 x.2.1 x.2.2).num, (value x.1 x.2.1 x.2.2).den)) :=
…

    Mentions: OAI.ContinuumCoulomb.DyadicRootProgram.value