OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedSourceIndex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Explicit finite sum/product indices for the history qubits and padded terms. Their natural values are the literal support-list site numbers.

  1. def OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.qubitCount line 13
  2. def OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.qubits line 16
  3. theorem OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.qubitCount_eq line 20
  4. theorem OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.qubits_index line 24
  5. def OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.referenceCount line 34
  6. def OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.reference line 37
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.referenceCount_eq line 41
  8. abbrev OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.Pattern line 46
  9. def OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.patternCount line 47
  10. def OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.patterns line 48
  11. def OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.termCount line 50
  12. def OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.terms line 51
  13. theorem OAI.ContinuumCoulomb.QuantumOrderedSourceIndex.termCount_eq line 54