OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarNearGroundCompactness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness of normalized near-ground sequences for the actual well. The positive free form makes compactness of the potential multiplier enough.

  1. theorem OAI.ContinuumCoulomb.PlanarSobolev.nearGround_cauchy_of_potential_cauchy line 18
  2. theorem OAI.ContinuumCoulomb.PlanarSobolev.nearGround_subsequence line 40