OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FockCoefficientNorm.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Coefficient perturbations of the actual one- and two-body CAR operators. The bounds depend polynomially on the number of modes and not on the exponentially large dimension of the exterior algebra.

  1. def OAI.ContinuumCoulomb.HubbardGlobal.oneBodyOperator line 16
  2. def OAI.ContinuumCoulomb.HubbardGlobal.twoBodyOperator line 19
  3. lemma OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_mul_norm_one line 24
  4. lemma OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_quartic_norm line 31
  5. lemma OAI.ContinuumCoulomb.HubbardGlobal.oneBodyOperator_norm line 40
  6. lemma OAI.ContinuumCoulomb.HubbardGlobal.twoBodyOperator_norm line 53
  7. lemma OAI.ContinuumCoulomb.HubbardGlobal.oneBodyOperator_sub line 78
  8. lemma OAI.ContinuumCoulomb.HubbardGlobal.twoBodyOperator_sub line 83
  9. lemma OAI.ContinuumCoulomb.HubbardGlobal.oneBodyOperator_error line 90
  10. lemma OAI.ContinuumCoulomb.HubbardGlobal.twoBodyOperator_error line 103
  11. lemma OAI.ContinuumCoulomb.HubbardGlobal.electronicOperator_error line 120