OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkDegreeBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Degree control for many fork centers sharing a retained background graph.

  1. theorem OAI.ContinuumCoulomb.qmaGraphDegree_sum line 14
  2. theorem OAI.ContinuumCoulomb.qmaCount_eq_le_one line 21
  3. def OAI.ContinuumCoulomb.qmaForkOuter line 29
  4. theorem OAI.ContinuumCoulomb.qmaForkOuter_count line 32
  5. theorem OAI.ContinuumCoulomb.qmaForks_old_degree line 38
  6. theorem OAI.ContinuumCoulomb.qmaForks_noncenter_degree line 51
  7. theorem OAI.ContinuumCoulomb.qmaForks_center_degree line 66