OAI/InformationTheory/QuantumCircuit/Degree.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Local support and degree bounds for quantum operators.

  1. def OAI.QAC.TensorSupported line 13
  2. def OAI.QAC.degreeSpace line 16
  3. def OAI.QAC.HasDegreeLE line 19
  4. lemma OAI.QAC.HasDegreeLE.mono line 21
  5. lemma OAI.QAC.tensor_hasDegreeLE line 27
  6. lemma OAI.QAC.degree_zero line 31
  7. lemma OAI.QAC.degree_one line 34
  8. lemma OAI.QAC.HasDegreeLE.add line 38
  9. lemma OAI.QAC.HasDegreeLE.smul line 42
  10. lemma OAI.QAC.degree_sum line 46
  11. lemma OAI.QAC.degree_list_sum line 50
  12. lemma OAI.QAC.TensorSupported.mul line 58
  13. lemma OAI.QAC.HasDegreeLE.mul line 68
  14. lemma OAI.QAC.HasDegreeLE.pow line 87
  15. lemma OAI.QAC.Count.zero_degree line 94
  16. lemma OAI.QAC.Count.operator_degree line 99
  17. lemma OAI.QAC.Count.polynomial_degree line 105
  18. lemma OAI.QAC.TensorSupported.local_conjugate line 114
  19. lemma OAI.QAC.HasDegreeLE.local_conjugate line 124