OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact ordinary product coordinates for the slab Coulomb integral. These allow the finite-box potential to be treated by one-coordinate integrals without changing the Euclidean volume normalization.

  1. abbrev OAI.ContinuumCoulomb.SlabTriple line 15
  2. def OAI.ContinuumCoulomb.slabTripleEquiv line 17
  3. theorem OAI.ContinuumCoulomb.slabTripleEquiv_apply line 23
  4. theorem OAI.ContinuumCoulomb.slabTripleEquiv_symm_apply line 25
  5. theorem OAI.ContinuumCoulomb.slabTripleEquiv_measurePreserving line 30
  6. def OAI.ContinuumCoulomb.slabTripleBox line 36
  7. theorem OAI.ContinuumCoulomb.slabTripleBox_measurable line 39
  8. theorem OAI.ContinuumCoulomb.slabTripleBox_preimage line 42
  9. theorem OAI.ContinuumCoulomb.slabTriple_setIntegral line 48
  10. theorem OAI.ContinuumCoulomb.slabPotential_eq_setIntegral line 56
  11. theorem OAI.ContinuumCoulomb.slabPotential_triple line 69