OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumMatrixError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Entrywise errors of the bounded-size local matrices give quadratic bounds that can be summed before any spectral approximation.

  1. theorem OAI.ContinuumCoulomb.qmaQuadratic_entry_bound line 13