OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoulombQuadrature.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual six-coordinate cubature of the finite Coulomb integral.

  1. def OAI.ContinuumCoulomb.RawCoulombSample.quadratureInput line 13
  2. def OAI.ContinuumCoulomb.RawCoulombSample.sampled line 17
  3. theorem OAI.ContinuumCoulomb.RawCoulombSample.quadrature_cast line 27
  4. theorem OAI.ContinuumCoulomb.RawCoulombSample.position_sampled line 37
  5. theorem OAI.ContinuumCoulomb.RawCoulombSample.quadrature_error line 55