OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarModeEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual manufactured planar mode attains energy -1/2. The integration by parts uses its proved square-integrable first and second derivatives, rather than imposing an eigenvalue or normalization hypothesis.

  1. theorem OAI.ContinuumCoulomb.planarResolventMode_partial_memLp line 14
  2. theorem OAI.ContinuumCoulomb.planarResolventMode_second_memLp line 20
  3. theorem OAI.ContinuumCoulomb.planarResolventMode_energy_ibp line 26
  4. theorem OAI.ContinuumCoulomb.planarResolventMode_energy line 38