OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoulombEvaluationParameters.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

One fixed set of polynomial precision parameters for the actual localized Coulomb coefficient. Only the requested accuracy varies.

  1. def OAI.ContinuumCoulomb.CoulombEvaluation.frequencyBound line 13
  2. def OAI.ContinuumCoulomb.CoulombEvaluation.normalizationBound line 14
  3. def OAI.ContinuumCoulomb.CoulombEvaluation.rawMassBound line 16
  4. def OAI.ContinuumCoulomb.CoulombEvaluation.truncationPrecision line 19
  5. def OAI.ContinuumCoulomb.CoulombEvaluation.denominator line 20
  6. def OAI.ContinuumCoulomb.CoulombEvaluation.radius line 23
  7. def OAI.ContinuumCoulomb.CoulombEvaluation.rawPrecision line 25
  8. def OAI.ContinuumCoulomb.CoulombEvaluation.mesh line 26
  9. def OAI.ContinuumCoulomb.CoulombEvaluation.samplePrecision line 28
  10. def OAI.ContinuumCoulomb.CoulombEvaluation.kernelPrecision line 30
  11. def OAI.ContinuumCoulomb.CoulombEvaluation.normalizationPrecision line 32
  12. def OAI.ContinuumCoulomb.CoulombEvaluation.input line 34
  13. def OAI.ContinuumCoulomb.CoulombEvaluation.rawApproximate line 38
  14. def OAI.ContinuumCoulomb.CoulombEvaluation.approximate line 41
  15. theorem OAI.ContinuumCoulomb.CoulombEvaluation.frequencyBound_le line 44
  16. theorem OAI.ContinuumCoulomb.CoulombEvaluation.normalizationBound_bounds line 49
  17. theorem OAI.ContinuumCoulomb.CoulombEvaluation.rawMassBound_le line 58
  18. theorem OAI.ContinuumCoulomb.CoulombEvaluation.denominator_positive line 64
  19. theorem OAI.ContinuumCoulomb.CoulombEvaluation.radius_positive line 72
  20. theorem OAI.ContinuumCoulomb.CoulombEvaluation.rawPrecision_positive line 76
  21. theorem OAI.ContinuumCoulomb.CoulombEvaluation.mesh_positive line 83
  22. theorem OAI.ContinuumCoulomb.CoulombEvaluation.epsilon_eq line 100