OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteTensorFormError.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual finite continuum form inherits the polynomial CAR coefficient error bound, with no dependence on the exponentially large Fock dimension.

  1. theorem OAI.ContinuumCoulomb.HubbardGlobal.oneBodyOperator_smul line 15
  2. theorem OAI.ContinuumCoulomb.HubbardGlobal.twoBodyOperator_smul line 19
  3. def OAI.ContinuumCoulomb.nuclearFormIntegrable line 26
  4. theorem OAI.ContinuumCoulomb.finiteTensorState_form_approximation line 90