OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabOrbitalResidual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite slab's actual harmonic-oscillator residual on a localized orbital. Interior accuracy and weighted tails are kept separately.

  1. def OAI.ContinuumCoulomb.slabResidualMultiplier line 14
  2. def OAI.ContinuumCoulomb.slabUniformBound line 17
  3. def OAI.ContinuumCoulomb.slabOrbitalResidual line 20
  4. theorem OAI.ContinuumCoulomb.slabResidualMultiplier_abs_bound line 23
  5. theorem OAI.ContinuumCoulomb.square_times_density_bound line 46
  6. theorem OAI.ContinuumCoulomb.slabOrbitalResidual_square_integrable line 54
  7. theorem OAI.ContinuumCoulomb.slabOrbitalResidual_square_bound line 80
  8. theorem OAI.ContinuumCoulomb.slabOrbitalResidual_square_bound_seventySecond line 163