OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/NuclearCutoff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

One fixed smooth cutoff supplies all translated and scaled near-nucleus Hardy estimates; its constants are independent of the mesh and particle count.

  1. def OAI.ContinuumCoulomb.nuclearBump line 14
  2. def OAI.ContinuumCoulomb.nuclearCutoff line 16
  3. theorem OAI.ContinuumCoulomb.nuclearBump_derivative_bound line 19
  4. theorem OAI.ContinuumCoulomb.nuclearCutoff_contDiff line 28
  5. theorem OAI.ContinuumCoulomb.nuclearCutoff_abs_le_one line 32
  6. theorem OAI.ContinuumCoulomb.nuclearCutoff_fderiv line 38
  7. theorem OAI.ContinuumCoulomb.nuclearCutoff_partial_bound line 46
  8. theorem OAI.ContinuumCoulomb.nuclearCutoff_one line 64
  9. theorem OAI.ContinuumCoulomb.nuclearCutoff_outside line 72