OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListWeights.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Coefficient bounds for the actual ordered lists, including every active port and the scalar offset.

  1. structure OAI.ContinuumCoulomb.QuantumForkList.CoefficientBound line 14
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.groupAt_mem line 19
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.CoefficientBound.port line 24
  4. theorem OAI.ContinuumCoulomb.QuantumForkList.CoefficientBound.actualJ line 30
  5. theorem OAI.ContinuumCoulomb.QuantumForkList.CoefficientBound.actualK line 34
  6. theorem OAI.ContinuumCoulomb.QuantumForkList.unpairedBonds_length_le line 38
  7. theorem OAI.ContinuumCoulomb.QuantumForkList.CoefficientBound.background line 44
  8. theorem OAI.ContinuumCoulomb.QuantumForkList.scale_abs_bound line 53