OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedPrivate.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A literal private-pair subdivision of an ordered X/Z family. The source site's list order determines both factors and every output site.

  1. def OAI.ContinuumCoulomb.QuantumOrderedPrivate.outputWord line 15
  2. def OAI.ContinuumCoulomb.QuantumOrderedPrivate.outputSites line 21
  3. def OAI.ContinuumCoulomb.QuantumOrderedPrivate.outputCoefficient line 24
  4. theorem OAI.ContinuumCoulomb.QuantumOrderedPrivate.output_noY line 28
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedPrivate.outputSites_nodup line 35
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedPrivate.outputSites_length line 40
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedPrivate.outputSites_cover line 44
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedPrivate.output_private line 66
  9. theorem OAI.ContinuumCoulomb.QuantumOrderedPrivate.output_accuracy line 81