OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ResolventSchedule.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial-sized mesh and precision choices for the resolvent quadrature. The radius and requested inverse accuracy are unary inputs.

  1. def OAI.ContinuumCoulomb.ResolventSchedule.scale line 11
  2. def OAI.ContinuumCoulomb.ResolventSchedule.countPrefix line 12
  3. def OAI.ContinuumCoulomb.ResolventSchedule.count line 13
  4. def OAI.ContinuumCoulomb.ResolventSchedule.magnitude line 14
  5. def OAI.ContinuumCoulomb.ResolventSchedule.precision line 15
  6. abbrev OAI.ContinuumCoulomb.ResolventSchedule.Input line 17
  7. def OAI.ContinuumCoulomb.ResolventSchedule.inputCode line 18
  8. def OAI.ContinuumCoulomb.ResolventSchedule.argument line 21
  9. def OAI.ContinuumCoulomb.ResolventSchedule.approximate line 28
  10. opaque OAI.ContinuumCoulomb.ResolventSchedule.mulProgram line 30
  11. opaque OAI.ContinuumCoulomb.ResolventSchedule.addProgram line 33
  12. opaque OAI.ContinuumCoulomb.ResolventSchedule.scaleProgram line 36
  13. opaque OAI.ContinuumCoulomb.ResolventSchedule.squareProgram line 41
  14. opaque OAI.ContinuumCoulomb.ResolventSchedule.fourthProgram line 45
  15. opaque OAI.ContinuumCoulomb.ResolventSchedule.eighthProgram line 48
  16. opaque OAI.ContinuumCoulomb.ResolventSchedule.constant4096Program line 51
  17. opaque OAI.ContinuumCoulomb.ResolventSchedule.radiusOffsetProgram line 56
  18. opaque OAI.ContinuumCoulomb.ResolventSchedule.radiusFourthProgram line 62
  19. opaque OAI.ContinuumCoulomb.ResolventSchedule.scaleEighthProgram line 66
  20. opaque OAI.ContinuumCoulomb.ResolventSchedule.countPrefixProgram line 70
  21. opaque OAI.ContinuumCoulomb.ResolventSchedule.countFactorsProgram line 75
  22. opaque OAI.ContinuumCoulomb.ResolventSchedule.countRawProgram line 80
  23. theorem OAI.ContinuumCoulomb.ResolventSchedule.count_value line 84
  24. opaque OAI.ContinuumCoulomb.ResolventSchedule.countProgram line 88
  25. opaque OAI.ContinuumCoulomb.ResolventSchedule.magnitudeProgram line 91
  26. opaque OAI.ContinuumCoulomb.ResolventSchedule.precisionProgram line 102
  27. opaque OAI.ContinuumCoulomb.ResolventSchedule.argumentProgram line 106
  28. opaque OAI.ContinuumCoulomb.ResolventSchedule.program line 123
  29. opaque OAI.ContinuumCoulomb.ResolventSchedule.certificate line 126
  30. theorem OAI.ContinuumCoulomb.ResolventSchedule.scale_positive line 129
  31. theorem OAI.ContinuumCoulomb.ResolventSchedule.count_positive line 131