OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSubdivisionSites.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Literal ordered site lists for each of the four subdivision terms. The two finite subdivision stages reuse these lists, rather than selecting a new support from an existential locality certificate.

  1. def OAI.ContinuumCoulomb.QuantumOrderedSubdivision.appendMediator line 15
  2. theorem OAI.ContinuumCoulomb.QuantumOrderedSubdivision.appendMediator_nodup line 18
  3. theorem OAI.ContinuumCoulomb.QuantumOrderedSubdivision.appendMediator_length line 26
  4. def OAI.ContinuumCoulomb.QuantumOrderedSubdivision.outputSites line 30
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedSubdivision.outputSites_nodup line 34
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedSubdivision.outputSites_length line 44
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedSubdivision.join_support_cover line 63
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedSubdivision.outputSites_cover line 80