OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFourAxis.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A common interface for the fixed X and Z exchange encodings.

  1. def OAI.ContinuumCoulomb.qmaFourAxis line 13
  2. def OAI.ContinuumCoulomb.qmaFourAxisWeights line 14
  3. def OAI.ContinuumCoulomb.qmaFourAxisShift line 16
  4. def OAI.ContinuumCoulomb.qmaFourAxisScale line 18
  5. def OAI.ContinuumCoulomb.qmaFourAxisSign line 19
  6. theorem OAI.ContinuumCoulomb.qmaFourAxisScale_pos line 21
  7. theorem OAI.ContinuumCoulomb.qmaFourAxisWeights_correlation line 27
  8. def OAI.ContinuumCoulomb.qmaFourAxisField line 35
  9. def OAI.ContinuumCoulomb.qmaFourAxisFieldShift line 38
  10. theorem OAI.ContinuumCoulomb.qmaFourAxisField_compression line 40