OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/MoserDifferenceBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Fixed polynomial precision parameters for coordinate differences of the manufactured field. Both the spatial step and scalar accuracy are chosen from its already proved uniform six-derivative bound.

  1. def OAI.ContinuumCoulomb.MoserDifferenceBudget.guard line 13
  2. theorem OAI.ContinuumCoulomb.MoserDifferenceBudget.guard_positive line 15
  3. theorem OAI.ContinuumCoulomb.MoserDifferenceBudget.guard_bound line 17
  4. def OAI.ContinuumCoulomb.MoserDifferenceBudget.step line 23
  5. def OAI.ContinuumCoulomb.MoserDifferenceBudget.precision line 24
  6. theorem OAI.ContinuumCoulomb.MoserDifferenceBudget.step_positive line 26
  7. theorem OAI.ContinuumCoulomb.MoserDifferenceBudget.step_le_one line 31
  8. theorem OAI.ContinuumCoulomb.MoserDifferenceBudget.second_budget line 38
  9. theorem OAI.ContinuumCoulomb.MoserDifferenceBudget.first_budget line 65
  10. theorem OAI.ContinuumCoulomb.MoserDifferenceBudget.laplacian_budget line 81