OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CorrectedManufacturedResidual.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Gram correction preserves a polynomial residual bound: it sums over spatial modes, independently of the many-electron occupation basis.

  1. def OAI.ContinuumCoulomb.correctedManufacturedResidual line 14
  2. theorem OAI.ContinuumCoulomb.correctedManufacturedResidual_memLp line 18
  3. theorem OAI.ContinuumCoulomb.correctedManufacturedResidual_square_bound line 27