OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedModes.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual localized modes in planar/transverse coordinates. The measure is the product of planar Euclidean volume and one-dimensional Lebesgue measure. The split Laplacian below is the sum of the three coordinate derivatives.

  1. abbrev OAI.ContinuumCoulomb.SplitPosition line 15
  2. def OAI.ContinuumCoulomb.localizedMode line 17
  3. def OAI.ContinuumCoulomb.localizedPotential line 20
  4. def OAI.ContinuumCoulomb.splitLaplacian line 23
  5. theorem OAI.ContinuumCoulomb.localizedMode_C7 line 27
  6. theorem OAI.ContinuumCoulomb.localizedMode_positive line 32
  7. theorem OAI.ContinuumCoulomb.localizedMode_square_integrable line 36
  8. theorem OAI.ContinuumCoulomb.localizedMode_normalized line 42
  9. theorem OAI.ContinuumCoulomb.localizedMode_memLp line 51
  10. theorem OAI.ContinuumCoulomb.localizedMode_planar_laplacian line 56
  11. theorem OAI.ContinuumCoulomb.localizedMode_vertical_second line 69
  12. theorem OAI.ContinuumCoulomb.localizedMode_eigen_equation line 76