OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedDualMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Concrete compact bumps supply local duality for the actual mode densities.

  1. def OAI.ContinuumCoulomb.localDualBump line 13
  2. theorem OAI.ContinuumCoulomb.localDualBump_smooth line 15
  3. theorem OAI.ContinuumCoulomb.localDualBump_support line 18
  4. def OAI.ContinuumCoulomb.localDualMass line 22
  5. theorem OAI.ContinuumCoulomb.localDualMass_positive line 25
  6. def OAI.ContinuumCoulomb.localLeakageBound line 32
  7. theorem OAI.ContinuumCoulomb.localLeakageBound_nonnegative line 35
  8. theorem OAI.ContinuumCoulomb.localDualPair_offsite line 39
  9. theorem OAI.ContinuumCoulomb.localDualTests_disjoint line 48
  10. theorem OAI.ContinuumCoulomb.localizedDualMatrix_lower line 53