OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRawSchedule.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

All four-spin scales and precisions are computed from the raw finite input.

  1. def OAI.ContinuumCoulomb.QuantumRawExchange.mass line 12
  2. def OAI.ContinuumCoulomb.QuantumRawExchange.size line 13
  3. def OAI.ContinuumCoulomb.QuantumRawExchange.budget line 14
  4. def OAI.ContinuumCoulomb.QuantumRawExchange.scale line 15
  5. abbrev OAI.ContinuumCoulomb.QuantumRawExchange.ScheduleInput line 17
  6. def OAI.ContinuumCoulomb.QuantumRawExchange.scheduleCode line 18
  7. def OAI.ContinuumCoulomb.QuantumRawExchange.errorBound line 21
  8. def OAI.ContinuumCoulomb.QuantumRawExchange.bits line 23
  9. def OAI.ContinuumCoulomb.QuantumRawExchange.scheduled line 24
  10. def OAI.ContinuumCoulomb.QuantumRawExchange.compile line 25
  11. opaque OAI.ContinuumCoulomb.QuantumRawExchange.rawWeightProgram line 27
  12. opaque OAI.ContinuumCoulomb.QuantumRawExchange.rawAbsoluteProgram line 29
  13. opaque OAI.ContinuumCoulomb.QuantumRawExchange.massProgram line 31
  14. opaque OAI.ContinuumCoulomb.QuantumRawExchange.scheduleCountProgram line 34
  15. opaque OAI.ContinuumCoulomb.QuantumRawExchange.scheduleTailProgram line 35
  16. opaque OAI.ContinuumCoulomb.QuantumRawExchange.accuracyProgram line 37
  17. opaque OAI.ContinuumCoulomb.QuantumRawExchange.scheduleTermsProgram line 39
  18. opaque OAI.ContinuumCoulomb.QuantumRawExchange.scheduleLengthProgram line 41
  19. opaque OAI.ContinuumCoulomb.QuantumRawExchange.scheduleLengthRatProgram line 43
  20. opaque OAI.ContinuumCoulomb.QuantumRawExchange.scheduleMassProgram line 45
  21. opaque OAI.ContinuumCoulomb.QuantumRawExchange.sizeProgram line 47
  22. opaque OAI.ContinuumCoulomb.QuantumRawExchange.linearBudgetProgram line 49
  23. opaque OAI.ContinuumCoulomb.QuantumRawExchange.quadraticBaseProgram line 51
  24. opaque OAI.ContinuumCoulomb.QuantumRawExchange.quadraticBudgetProgram line 53
  25. opaque OAI.ContinuumCoulomb.QuantumRawExchange.budgetProgram line 56
  26. opaque OAI.ContinuumCoulomb.QuantumRawExchange.squareBudgetProgram line 59
  27. opaque OAI.ContinuumCoulomb.QuantumRawExchange.cubeBudgetProgram line 62
  28. opaque OAI.ContinuumCoulomb.QuantumRawExchange.accuracyRatProgram line 65
  29. opaque OAI.ContinuumCoulomb.QuantumRawExchange.scheduleScaleProgram line 67
  30. opaque OAI.ContinuumCoulomb.QuantumRawExchange.absoluteScaleProgram line 70
  31. opaque OAI.ContinuumCoulomb.QuantumRawExchange.countRatProgram line 72
  32. opaque OAI.ContinuumCoulomb.QuantumRawExchange.sixCountProgram line 74
  33. opaque OAI.ContinuumCoulomb.QuantumRawExchange.termCountProgram line 76
  34. opaque OAI.ContinuumCoulomb.QuantumRawExchange.edgeCountProgram line 78
  35. opaque OAI.ContinuumCoulomb.QuantumRawExchange.crossBudgetProgram line 81
  36. opaque OAI.ContinuumCoulomb.QuantumRawExchange.fieldBudgetProgram line 86
  37. opaque OAI.ContinuumCoulomb.QuantumRawExchange.matrixBudgetProgram line 88
  38. opaque OAI.ContinuumCoulomb.QuantumRawExchange.scalarBudgetProgram line 94
  39. opaque OAI.ContinuumCoulomb.QuantumRawExchange.errorBoundProgram line 96
  40. opaque OAI.ContinuumCoulomb.QuantumRawExchange.bitsProgram line 98
  41. opaque OAI.ContinuumCoulomb.QuantumRawExchange.scheduledProgram line 100
  42. opaque OAI.ContinuumCoulomb.QuantumRawExchange.compileProgram line 102
  43. def OAI.ContinuumCoulomb.QuantumRawExchange.compileCertificate line 104