OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoulombPackets.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The global Coulomb pairing for the bounded integrable packets used in the mode construction. Existing Gaussian-kernel positivity applies directly once the elementary bounded-density estimate supplies joint integrability.

  1. structure OAI.ContinuumCoulomb.CoulombPacket line 14
  2. instance OAI.ContinuumCoulomb.CoulombPacket.(instance at line 24) line 24
  3. def OAI.ContinuumCoulomb.CoulombPacket.add line 26
  4. def OAI.ContinuumCoulomb.CoulombPacket.smul line 34
  5. theorem OAI.ContinuumCoulomb.CoulombPacket.joint_integrable line 44
  6. def OAI.ContinuumCoulomb.CoulombPacket.pair line 85
  7. theorem OAI.ContinuumCoulomb.CoulombPacket.pair_nonnegative line 88
  8. theorem OAI.ContinuumCoulomb.CoulombPacket.pair_symmetric line 91
  9. theorem OAI.ContinuumCoulomb.CoulombPacket.pair_add_left line 102
  10. theorem OAI.ContinuumCoulomb.CoulombPacket.pair_smul_left line 108
  11. theorem OAI.ContinuumCoulomb.CoulombPacket.pair_add_right line 114
  12. theorem OAI.ContinuumCoulomb.CoulombPacket.pair_smul_right line 117
  13. theorem OAI.ContinuumCoulomb.CoulombPacket.pair_cauchy line 120