OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedOneBody.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual differential action of the full multiwell operator on the localized modes. Subtraction of the common ground energy leaves exactly the sum of other wells, so its matrix is the checked hopping matrix plus the explicit two-tail error.

  1. def OAI.ContinuumCoulomb.multiwellPotential line 16
  2. def OAI.ContinuumCoulomb.multiwellAction line 19
  3. theorem OAI.ContinuumCoulomb.multiwellAction_localizedMode line 23
  4. def OAI.ContinuumCoulomb.localizedOneBodyIntegrand line 50
  5. theorem OAI.ContinuumCoulomb.localizedOneBodyIntegrand_eq line 56
  6. theorem OAI.ContinuumCoulomb.localizedOneBodyIntegrand_integrable line 73
  7. def OAI.ContinuumCoulomb.localizedOneBodyMatrix line 87
  8. theorem OAI.ContinuumCoulomb.localizedOneBodyMatrix_eq line 90
  9. theorem OAI.ContinuumCoulomb.localizedOneBodyMatrix_error_bound line 111