OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ShiftedHubbardBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite Hubbard energy, including its off-site shift and form error, has polynomial size. No occupation-space dimension enters.

  1. theorem OAI.ContinuumCoulomb.localizedOffsiteCoulomb_nonnegative line 14
  2. theorem OAI.ContinuumCoulomb.localizedOffsiteCoulomb_le line 21
  3. theorem OAI.ContinuumCoulomb.localizedOffsiteCoulomb_sum_le line 29
  4. theorem OAI.ContinuumCoulomb.localizedHubbardFormError_nonnegative line 36
  5. theorem OAI.ContinuumCoulomb.shifted_hubbard_abs_bound line 44
  6. theorem OAI.ContinuumCoulomb.exists_shifted_hubbard_polynomial_bound line 72