OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarOverlap.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual normalized planar orbitals have overlap bounded at rate 0.9, uniformly over every pair of centers.

  1. def OAI.ContinuumCoulomb.normalizedPlanarExponentialConstant line 13
  2. theorem OAI.ContinuumCoulomb.normalizedPlanarExponentialConstant_positive line 16
  3. theorem OAI.ContinuumCoulomb.normalizedPlanarMode_exponential_envelope line 21
  4. def OAI.ContinuumCoulomb.planarModeOverlap line 31
  5. theorem OAI.ContinuumCoulomb.planarModeOverlap_integrable line 34
  6. theorem OAI.ContinuumCoulomb.planarModeOverlap_nonnegative line 39
  7. theorem OAI.ContinuumCoulomb.planarModeOverlap_diagonal line 42
  8. theorem OAI.ContinuumCoulomb.planarModeOverlap_envelope line 48
  9. def OAI.ContinuumCoulomb.planarOverlapConstant line 85
  10. theorem OAI.ContinuumCoulomb.planarOverlapConstant_nonnegative line 88
  11. theorem OAI.ContinuumCoulomb.planarModeOverlap_decay line 91