OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingSelection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Group a selected family of physical crossing edges without assuming a matrix identity. Each source edge is either retained or assigned to one crossing pair.

  1. theorem OAI.ContinuumCoulomb.qmaSumSubtypePredicate line 12
  2. theorem OAI.ContinuumCoulomb.qmaOptionFiberSum line 18
  3. structure OAI.ContinuumCoulomb.QMARationalCrossingSelection line 31
  4. abbrev OAI.ContinuumCoulomb.QMARationalCrossingSelection.retained line 42
  5. def OAI.ContinuumCoulomb.QMARationalCrossingSelection.weight line 51
  6. def OAI.ContinuumCoulomb.QMARationalCrossingSelection.layer line 53
  7. theorem OAI.ContinuumCoulomb.QMARationalCrossingSelection.tagged_matrix line 60
  8. theorem OAI.ContinuumCoulomb.QMARationalCrossingSelection.weight_matrix line 68
  9. theorem OAI.ContinuumCoulomb.QMARationalCrossingSelection.source_matrix line 80
  10. theorem OAI.ContinuumCoulomb.QMARationalCrossingSelection.source_energy line 106
  11. theorem OAI.ContinuumCoulomb.QMARationalCrossingSelection.output_energy_error line 111