OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedUniformGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single positive complementary gap for every admissible manufactured configuration. Localization widths and error tolerances are selected before the instance and before the number of wells.

  1. theorem OAI.ContinuumCoulomb.localizedOverlap_row_threshold line 14
  2. theorem OAI.ContinuumCoulomb.manufacturedSlab_uniform_complement_gap line 36