OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkRounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Constantly many actual fork rounds give a degree-three graph of linear size.

  1. structure OAI.ContinuumCoulomb.QMAForkNetwork line 11
  2. def OAI.ContinuumCoulomb.QMAForkNetwork.next line 23
  3. def OAI.ContinuumCoulomb.QMAForkNetwork.iterate line 29
  4. theorem OAI.ContinuumCoulomb.QMAForkNetwork.iterate_degree line 33
  5. theorem OAI.ContinuumCoulomb.QMAForkNetwork.next_degree_le line 42
  6. theorem OAI.ContinuumCoulomb.QMAForkNetwork.iterate_degree_le line 47
  7. theorem OAI.ContinuumCoulomb.QMAForkNetwork.iterate_mass_le line 53
  8. theorem OAI.ContinuumCoulomb.QMAForkNetwork.iterate_vertices line 57
  9. theorem OAI.ContinuumCoulomb.QMAForkNetwork.iterate_background_edges line 69
  10. theorem OAI.ContinuumCoulomb.QMAForkNetwork.constant_round_degree line 84