OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarModeProperties.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Positivity, finite L² normalization and compact support of the actual manufactured planar potential. The differential eigen-equation and gap are not assumed by these declarations.

  1. theorem OAI.ContinuumCoulomb.planarResolventKernel_integral line 13
  2. theorem OAI.ContinuumCoulomb.planarResolventMode_integrable line 24
  3. theorem OAI.ContinuumCoulomb.planarResolventMode_integral line 28
  4. theorem OAI.ContinuumCoulomb.planarResolventMode_square_integrable line 34
  5. theorem OAI.ContinuumCoulomb.planarResolventMode_memLp line 44
  6. theorem OAI.ContinuumCoulomb.planarResolventMode_square_integral_positive line 48
  7. def OAI.ContinuumCoulomb.normalizedPlanarMode line 54
  8. theorem OAI.ContinuumCoulomb.normalizedPlanarMode_C7 line 57
  9. theorem OAI.ContinuumCoulomb.normalizedPlanarMode_positive line 60
  10. theorem OAI.ContinuumCoulomb.normalizedPlanarMode_normalized line 63
  11. def OAI.ContinuumCoulomb.manufacturedPlanarWell line 68
  12. theorem OAI.ContinuumCoulomb.manufacturedPlanarWell_C7 line 71
  13. theorem OAI.ContinuumCoulomb.manufacturedPlanarWell_nonpositive line 75
  14. theorem OAI.ContinuumCoulomb.manufacturedPlanarWell_support line 79
  15. theorem OAI.ContinuumCoulomb.manufacturedPlanarWell_hasCompactSupport line 87