OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoulombPacketCoercivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Global Coulomb coercivity from disjoint compact tests and approximate local duality. All integrals range over the whole Euclidean space.

  1. theorem OAI.ContinuumCoulomb.CoulombPacket.test_combination_energy line 13
  2. theorem OAI.ContinuumCoulomb.CoulombPacket.gram_coercive_of_dual_lower line 36