OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkPlaced.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Repeated degree reduction retains the coarse cells of all active centers.

  1. structure OAI.ContinuumCoulomb.QMAPlacedForkNetwork line 12
  2. def OAI.ContinuumCoulomb.QMAPlacedForkNetwork.centerCell line 20
  3. def OAI.ContinuumCoulomb.QMAPlacedForkNetwork.next line 22
  4. theorem OAI.ContinuumCoulomb.QMAPlacedForkNetwork.next_centerCell line 27
  5. def OAI.ContinuumCoulomb.QMAPlacedForkNetwork.iterate line 31
  6. theorem OAI.ContinuumCoulomb.QMAPlacedForkNetwork.iterate_graph line 35
  7. theorem OAI.ContinuumCoulomb.QMAPlacedForkNetwork.iterate_centerCell line 43
  8. theorem OAI.ContinuumCoulomb.QMAPlacedForkNetwork.next_cell_mass line 49
  9. theorem OAI.ContinuumCoulomb.QMAPlacedForkNetwork.iterate_cell_mass line 54