OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CorrectedCrossBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The off-diagonal form bound sums over spatial modes and spin components, without a sum over exponentially many many-electron occupations.

  1. theorem OAI.ContinuumCoulomb.complex_conj_sum_square_le line 14
  2. theorem OAI.ContinuumCoulomb.corrected_cross_square_bound line 22