OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListSum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reindexing the actual fresh-port list by its consecutive mediator number.

  1. theorem OAI.ContinuumCoulomb.QuantumForkList.range_sum line 13
  2. theorem OAI.ContinuumCoulomb.QuantumForkList.fresh_sum line 22
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.next_groupAt line 34
  4. theorem OAI.ContinuumCoulomb.QuantumForkList.next_active_sum line 40