OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CoulombQuadratureBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial mesh and precision budgets for the six-coordinate Coulomb quadrature. All varying parameters below are unary naturals.

  1. def OAI.ContinuumCoulomb.CoulombQuadratureSchedule.volume line 11
  2. def OAI.ContinuumCoulomb.CoulombQuadratureSchedule.lipschitz line 12
  3. def OAI.ContinuumCoulomb.CoulombQuadratureSchedule.mesh line 13
  4. def OAI.ContinuumCoulomb.CoulombQuadratureSchedule.accuracy line 14
  5. def OAI.ContinuumCoulomb.CoulombQuadratureSchedule.kernelPrecision line 15
  6. theorem OAI.ContinuumCoulomb.CoulombQuadratureSchedule.dyadic_le_inverse line 17
  7. theorem OAI.ContinuumCoulomb.CoulombQuadratureSchedule.scalar_budget line 23