OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/OrbitalCutoff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Expanding smooth cutoffs for the actual orbitals. Their first four jets are bounded independently of the radius and center.

  1. def OAI.ContinuumCoulomb.orbitalCutoffBump line 14
  2. def OAI.ContinuumCoulomb.orbitalCutoff line 16
  3. theorem OAI.ContinuumCoulomb.orbitalCutoff_smooth line 19
  4. theorem OAI.ContinuumCoulomb.orbitalCutoff_nonnegative line 23
  5. theorem OAI.ContinuumCoulomb.orbitalCutoff_le_one line 26
  6. theorem OAI.ContinuumCoulomb.orbitalCutoff_eq_one line 29
  7. theorem OAI.ContinuumCoulomb.orbitalCutoff_support line 37
  8. theorem OAI.ContinuumCoulomb.orbitalCutoff_hasCompactSupport line 51
  9. theorem OAI.ContinuumCoulomb.orbitalCutoff_jets_bounded line 56