OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/NuclearMeshBalance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A rational mesh suffices for the stronger compressed error. Taking h = R^-9 balances fourth-order cubature with the H1 cutoff tail.

  1. theorem OAI.ContinuumCoulomb.nuclear_mesh_balance line 11
  2. theorem OAI.ContinuumCoulomb.nuclear_mesh_balance_scaled line 27