OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/GaussianFrequency.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Certified approximation of the manuscript's actual transverse frequency sqrt (4*pi*rho). The integer density is fixed once for the construction; it is not assumed that the resulting frequency is rational.

  1. def OAI.ContinuumCoulomb.GaussianFrequency.frequency line 15
  2. def OAI.ContinuumCoulomb.GaussianFrequency.count line 17
  3. def OAI.ContinuumCoulomb.GaussianFrequency.precision line 19
  4. def OAI.ContinuumCoulomb.GaussianFrequency.radicand line 21
  5. def OAI.ContinuumCoulomb.GaussianFrequency.approximate line 23
  6. theorem OAI.ContinuumCoulomb.GaussianFrequency.count_positive line 25
  7. theorem OAI.ContinuumCoulomb.GaussianFrequency.pi_approximate_nonnegative line 27
  8. theorem OAI.ContinuumCoulomb.GaussianFrequency.radicand_nonnegative line 36
  9. theorem OAI.ContinuumCoulomb.GaussianFrequency.radicand_error line 40
  10. theorem OAI.ContinuumCoulomb.GaussianFrequency.root_precision_bound line 67
  11. theorem OAI.ContinuumCoulomb.GaussianFrequency.approximation_error line 77