OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteCubeQuadrature.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Product-interval integration and its uniform coordinate modulus. The application uses dimension six; the recursion only avoids repeating six identical one-dimensional estimates.

  1. def OAI.ContinuumCoulomb.UniformQuadrature.cubeMem line 14
  2. def OAI.ContinuumCoulomb.UniformQuadrature.cubeModulus line 16
  3. def OAI.ContinuumCoulomb.UniformQuadrature.cubeIntegral line 20
  4. def OAI.ContinuumCoulomb.UniformQuadrature.cubeSample line 24
  5. theorem OAI.ContinuumCoulomb.UniformQuadrature.cubeMem_cons line 28
  6. theorem OAI.ContinuumCoulomb.UniformQuadrature.cubeModulus_section line 35
  7. theorem OAI.ContinuumCoulomb.UniformQuadrature.cubeModulus_head line 42
  8. theorem OAI.ContinuumCoulomb.UniformQuadrature.cubeIntegral_difference line 50
  9. theorem OAI.ContinuumCoulomb.UniformQuadrature.cubeIntegral_head_modulus line 94
  10. theorem OAI.ContinuumCoulomb.UniformQuadrature.cube_quadrature_error line 108