OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedSplit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Deterministic balanced support factors. The actual compiler carries ordered lists of sites and splits them with take/drop; no chosen finite subset is needed by either subdivision stage.

  1. def OAI.ContinuumCoulomb.QuantumOrderedSplit.left line 16
  2. def OAI.ContinuumCoulomb.QuantumOrderedSplit.right line 17
  3. theorem OAI.ContinuumCoulomb.QuantumOrderedSplit.union line 20
  4. theorem OAI.ContinuumCoulomb.QuantumOrderedSplit.disjoint line 24
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedSplit.left_card line 31
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedSplit.right_card line 35
  7. def OAI.ContinuumCoulomb.QuantumOrderedSplit.firstWord line 41
  8. def OAI.ContinuumCoulomb.QuantumOrderedSplit.secondWord line 44
  9. theorem OAI.ContinuumCoulomb.QuantumOrderedSplit.first_support line 47
  10. theorem OAI.ContinuumCoulomb.QuantumOrderedSplit.second_support line 51
  11. theorem OAI.ContinuumCoulomb.QuantumOrderedSplit.factor line 55
  12. theorem OAI.ContinuumCoulomb.QuantumOrderedSplit.commute line 61
  13. theorem OAI.ContinuumCoulomb.QuantumOrderedSplit.same_parity line 66