OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPaddedHistory.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A literal 4096-word family for each actual ordered history term. The term type is a product, so its emitted order requires no filtered finite type.

  1. abbrev OAI.ContinuumCoulomb.QuantumPaddedHistory.Term line 14
  2. def OAI.ContinuumCoulomb.QuantumPaddedHistory.widthIndex line 17
  3. def OAI.ContinuumCoulomb.QuantumPaddedHistory.tableMatrix line 21
  4. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.tableMatrix_eq line 25
  5. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.tableMatrix_hermitian line 35
  6. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.tableMatrix_real line 41
  7. def OAI.ContinuumCoulomb.QuantumPaddedHistory.word line 47
  8. def OAI.ContinuumCoulomb.QuantumPaddedHistory.coefficient line 54
  9. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.term_sum line 61
  10. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.family_sum line 95
  11. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.term_count line 101
  12. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.support line 107
  13. theorem OAI.ContinuumCoulomb.QuantumPaddedHistory.even line 111