OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedResidualGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The residual-controlled one-electron estimate and its integral over all electron slots. The admitted many-electron state remains unrestricted.

  1. theorem OAI.ContinuumCoulomb.manufacturedSlab_residual_finite_rank_lower line 12
  2. theorem OAI.ContinuumCoulomb.manufacturedSlab_uniform_residual_manyElectron_lower line 51