OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/H1PairingBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An L2 residual controls its pairing with every weak-H1 state.

  1. theorem OAI.ContinuumCoulomb.h1_real_pairing_sq_le line 11