OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/HubbardTolerance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Combining the two entrywise approximation budgets in the finite form.

  1. theorem OAI.ContinuumCoulomb.localizedHubbardFormError_mono line 10
  2. theorem OAI.ContinuumCoulomb.double_inverse_power_le line 16
  3. theorem OAI.ContinuumCoulomb.exists_hubbardDouble_parameter_offset line 24