OAI/MathematicalPhysics/ContinuumCoulomb/Programs/RawCoulombMassBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform raw-integral bounds for certified normalization of the finite-box numerical output.

  1. theorem OAI.ContinuumCoulomb.localizedRawCoulombBox_bound line 13
  2. theorem OAI.ContinuumCoulomb.localizedCoulombBox_eq_normalizedRaw line 46