OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedGram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Coercivity of the actual full Coulomb Gram matrix of the localized resolvent--Gaussian modes.

  1. def OAI.ContinuumCoulomb.localizedPacket line 14
  2. theorem OAI.ContinuumCoulomb.localizedPacket_pair line 24
  3. theorem OAI.ContinuumCoulomb.testCharge_localizedTest line 38
  4. theorem OAI.ContinuumCoulomb.localizedTest_energy line 43
  5. def OAI.ContinuumCoulomb.localDualEnergyBound line 49
  6. theorem OAI.ContinuumCoulomb.localDualEnergyBound_positive line 51
  7. theorem OAI.ContinuumCoulomb.localizedGram_coercive line 55