OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/SharpBlockPerturbation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A block estimate retaining the cancellation in the effective energy. It is needed when the third-order gadget's coupling exceeds its low block.

  1. theorem OAI.ContinuumCoulomb.Perturbation.sharp_lowBlockEnergy_lower line 16
  2. theorem OAI.ContinuumCoulomb.Perturbation.sharp_lowBlockRayleigh_lower line 44
  3. theorem OAI.ContinuumCoulomb.Perturbation.sharp_lowBlockRayleigh_trial_upper line 61
  4. theorem OAI.ContinuumCoulomb.Perturbation.sharp_lowBlockBottom line 81