OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A fork round keeps each new pair in the coarse cell of its active center.

  1. def OAI.ContinuumCoulomb.qmaForkCellNext line 13
  2. theorem OAI.ContinuumCoulomb.qmaForkCellNext_old line 18
  3. theorem OAI.ContinuumCoulomb.qmaForkCellNext_fresh line 22
  4. def OAI.ContinuumCoulomb.QMAForkCellAligned line 27
  5. theorem OAI.ContinuumCoulomb.qmaForkCellNext_aligned line 30
  6. def OAI.ContinuumCoulomb.qmaCellMass line 42
  7. theorem OAI.ContinuumCoulomb.qmaForkCellNext_mass line 45
  8. theorem OAI.ContinuumCoulomb.qmaForkCell_pair_mass_le line 59
  9. theorem OAI.ContinuumCoulomb.qmaForkCellNext_mass_le line 75