OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPartialPaths.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Subdivide any selected subset of a finite exchange graph in one calibrated layer.

  1. def OAI.ContinuumCoulomb.qmaSelectedIndex line 16
  2. theorem OAI.ContinuumCoulomb.qmaSelectedIndex_mem line 19
  3. def OAI.ContinuumCoulomb.qmaSelectedSite line 22
  4. theorem OAI.ContinuumCoulomb.qmaSelectedSite_injective line 26
  5. theorem OAI.ContinuumCoulomb.qmaSelected_sum line 37
  6. theorem OAI.ContinuumCoulomb.qmaSelected_partition line 41
  7. theorem OAI.ContinuumCoulomb.qmaPartialPaths_source line 49
  8. def OAI.ContinuumCoulomb.qmaPartialPathsScale line 66
  9. def OAI.ContinuumCoulomb.qmaPartialPaths line 72
  10. theorem OAI.ContinuumCoulomb.qmaPartialPaths_accuracy line 78
  11. abbrev OAI.ContinuumCoulomb.QMAPartialPathsEdge line 90
  12. def OAI.ContinuumCoulomb.qmaPartialPathsLeft line 93
  13. def OAI.ContinuumCoulomb.qmaPartialPathsRight line 96
  14. theorem OAI.ContinuumCoulomb.qmaPartialPaths_distinct line 101
  15. theorem OAI.ContinuumCoulomb.qmaPartialPaths_edge_count line 107
  16. theorem OAI.ContinuumCoulomb.qmaPartialPaths_old_degree line 114
  17. theorem OAI.ContinuumCoulomb.qmaPartialPaths_fresh_degree line 127