OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListNextWeights.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The emitted ordinary bonds, active ports and constant have one explicit polynomial envelope. The bound applies to the literal rational transition.

  1. theorem OAI.ContinuumCoulomb.QuantumForkList.two_mul_abs_le line 14
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.pairBonds_abs_le line 20
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.next_scalar_abs_le line 37
  4. theorem OAI.ContinuumCoulomb.QuantumForkList.next_coefficientBound line 80