OAI/InformationTheory/QuantumCircuit/LowDegreePropagation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Low-degree propagation with subexponential norm and error bounds.

  1. def OAI.QAC.headLayer line 13
  2. lemma OAI.QAC.headLayer_nil_matrix line 16
  3. lemma OAI.QAC.evolution_tail line 19
  4. lemma OAI.QAC.evolution_take_tail line 25
  5. lemma OAI.QAC.RegularTrajectory.head line 31
  6. lemma OAI.QAC.RegularTrajectory.tail line 43
  7. theorem OAI.QAC.low_degree_propagation_with_prefactor line 55
  8. theorem OAI.QAC.low_degree_propagation line 127