OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/GaussianPacket.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A certified rational sample of the actual transverse Gaussian. The frequency is sqrt(4*pi*rho), with rho fixed, and is evaluated internally.

  1. abbrev OAI.ContinuumCoulomb.GaussianPacket.Input line 14
  2. def OAI.ContinuumCoulomb.GaussianPacket.frequencyPrecision line 16
  3. def OAI.ContinuumCoulomb.GaussianPacket.exponentialPrecision line 17
  4. def OAI.ContinuumCoulomb.GaussianPacket.magnitude line 18
  5. def OAI.ContinuumCoulomb.GaussianPacket.exponent line 20
  6. def OAI.ContinuumCoulomb.GaussianPacket.argument line 23
  7. def OAI.ContinuumCoulomb.GaussianPacket.approximate line 26
  8. theorem OAI.ContinuumCoulomb.GaussianPacket.frequencyApprox_nonnegative line 29
  9. theorem OAI.ContinuumCoulomb.GaussianPacket.frequency_le line 34
  10. theorem OAI.ContinuumCoulomb.GaussianPacket.frequencyApprox_le line 42
  11. theorem OAI.ContinuumCoulomb.GaussianPacket.exponent_nonpositive line 49
  12. theorem OAI.ContinuumCoulomb.GaussianPacket.exponent_abs_le line 54
  13. theorem OAI.ContinuumCoulomb.GaussianPacket.exponent_error line 70
  14. theorem OAI.ContinuumCoulomb.GaussianPacket.exponential_precision_bound line 99
  15. theorem OAI.ContinuumCoulomb.GaussianPacket.approximation_error line 107