OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarMultiwellMatrix.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The unperturbed shifted multiwell matrix: its leading off-diagonal entry is the actual hopping, and every remaining term has two tail factors. No independent matrix approximation is assumed.

  1. def OAI.ContinuumCoulomb.planarMultiwellMatrix line 14
  2. def OAI.ContinuumCoulomb.planarHoppingMatrix line 17
  3. theorem OAI.ContinuumCoulomb.planarMultiwellMatrix_error_eq line 20
  4. theorem OAI.ContinuumCoulomb.planarMultiwellMatrix_error_bound line 44