OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedComplement.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The manufactured field has a positive gap above its one-orbital energy on the complement of the actual orthonormalized modes. All localization losses are retained explicitly; they are not charged to the final energy precision.

  1. def OAI.ContinuumCoulomb.manufacturedSpectralLoss line 15
  2. theorem OAI.ContinuumCoulomb.manufacturedSpectralLevel_eq line 22
  3. theorem OAI.ContinuumCoulomb.manufacturedSpectralLevel_lower line 28
  4. theorem OAI.ContinuumCoulomb.manufacturedSlab_corrected_complement_lower line 34