OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRawOutputBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Polynomial magnitude envelopes for every actual physical edge and scalar offset in the rational four-spin output.

  1. theorem OAI.ContinuumCoulomb.QuantumRawExchange.field_bond_abs line 12
  2. theorem OAI.ContinuumCoulomb.QuantumRawExchange.cross_bond_abs line 17
  3. theorem OAI.ContinuumCoulomb.QuantumRawExchange.bonds_abs line 23
  4. theorem OAI.ContinuumCoulomb.QuantumRawExchange.scalar_abs line 41
  5. theorem OAI.ContinuumCoulomb.QuantumRawExchange.termBondsList_abs line 49
  6. theorem OAI.ContinuumCoulomb.QuantumRawExchange.termScalarList_abs line 57
  7. def OAI.ContinuumCoulomb.QuantumRawExchange.outputBound line 74
  8. theorem OAI.ContinuumCoulomb.QuantumRawExchange.fullBonds_abs line 77
  9. theorem OAI.ContinuumCoulomb.QuantumRawExchange.fullScalar_abs line 98