OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumWalkErasureProgram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A polynomial finite-stack implementation of the actual coarse-walk loop erasure. Each fold output is a sublist of the processed input and initial list.

  1. def OAI.ContinuumCoulomb.QuantumWalkErasure.stepProgram line 15
  2. theorem OAI.ContinuumCoulomb.QuantumWalkErasure.fold_sublist line 23
  3. theorem OAI.ContinuumCoulomb.QuantumWalkErasure.fold_code_bound line 31
  4. def OAI.ContinuumCoulomb.QuantumWalkErasure.foldProgram line 39
  5. def OAI.ContinuumCoulomb.QuantumWalkErasure.program line 50
  6. def OAI.ContinuumCoulomb.QuantumWalkErasure.cellProgram line 58