OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/SplitSpectralBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Combining the actual planar and transverse form estimates. The projection budget removes the planar penalty from transverse excitations.

  1. def OAI.ContinuumCoulomb.splitPlanarForm line 15
  2. def OAI.ContinuumCoulomb.splitVerticalForm line 18
  3. theorem OAI.ContinuumCoulomb.split_form_projection_lower line 21