OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CorrectedDiagonalBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The same residual controls the actual compressed diagonal form, with no entrywise sum over occupation configurations.

  1. theorem OAI.ContinuumCoulomb.corrected_residual_sum_square_bound line 13
  2. theorem OAI.ContinuumCoulomb.corrected_diagonal_residual_identity line 52
  3. theorem OAI.ContinuumCoulomb.corrected_diagonal_lower line 94