OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedNuclearTensorLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Singular nuclear perturbations of the actual manufactured tensor projection. The differential residual and kinetic bounds are discharged from the orbitals.

  1. theorem OAI.ContinuumCoulomb.manufacturedTensor_nuclear_interacting_lower line 15