OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedHubbardComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual Hubbard lower bound passes through the full continuum complement estimate. The only spectral and domain inputs here are the explicit published planar, oscillator, and smooth-density propositions.

  1. theorem OAI.ContinuumCoulomb.manufacturedSlab_uniform_hubbard_lower line 16