OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPropagationOrder.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual ordered support has its reference bit first, followed by the duplicate-free propagation support in its literal source order.

  1. def OAI.ContinuumCoulomb.QuantumPropagationOrder.term line 16
  2. theorem OAI.ContinuumCoulomb.QuantumPropagationOrder.sites_eq line 19
  3. theorem OAI.ContinuumCoulomb.QuantumPropagationOrder.length_eq line 30
  4. def OAI.ContinuumCoulomb.QuantumPropagationOrder.firstIndex line 36
  5. def OAI.ContinuumCoulomb.QuantumPropagationOrder.nextIndex line 42
  6. theorem OAI.ContinuumCoulomb.QuantumPropagationOrder.firstIndex_site line 49
  7. theorem OAI.ContinuumCoulomb.QuantumPropagationOrder.nextIndex_site line 57
  8. def OAI.ContinuumCoulomb.QuantumPropagationOrder.referenceBit line 68
  9. def OAI.ContinuumCoulomb.QuantumPropagationOrder.localBits line 74
  10. theorem OAI.ContinuumCoulomb.QuantumPropagationOrder.extend_reference line 81
  11. theorem OAI.ContinuumCoulomb.QuantumPropagationOrder.extend_data line 109
  12. theorem OAI.ContinuumCoulomb.QuantumPropagationOrder.ordered_entry line 148
  13. theorem OAI.ContinuumCoulomb.QuantumPropagationOrder.ordered_gram_entry line 177