OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabOriginQuadrature.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The scalar slab shift is computed by cubature of a capped kernel on the fixed cube. Its singular truncation error is independent of the box.

  1. def OAI.ContinuumCoulomb.SlabOriginQuadrature.point line 16
  2. def OAI.ContinuumCoulomb.SlabOriginQuadrature.integrand line 19
  3. def OAI.ContinuumCoulomb.SlabOriginQuadrature.capped line 21
  4. theorem OAI.ContinuumCoulomb.SlabOriginQuadrature.point_norm_sub line 23
  5. theorem OAI.ContinuumCoulomb.SlabOriginQuadrature.modulus line 48
  6. theorem OAI.ContinuumCoulomb.SlabOriginQuadrature.cap_error line 55
  7. theorem OAI.ContinuumCoulomb.SlabOriginQuadrature.interval_scale line 86
  8. theorem OAI.ContinuumCoulomb.SlabOriginQuadrature.triple_interval_scale line 91
  9. theorem OAI.ContinuumCoulomb.SlabOriginQuadrature.triple_setIntegral line 102
  10. theorem OAI.ContinuumCoulomb.SlabOriginQuadrature.setIntegral_scale line 131
  11. theorem OAI.ContinuumCoulomb.SlabOriginQuadrature.capped_eq_cube line 136
  12. theorem OAI.ContinuumCoulomb.SlabOriginQuadrature.sampling_error line 155