OAI/InformationTheory/QuantumCircuit/RegularApproximation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Polynomial approximations on regular quantum trajectories.

  1. def OAI.QAC.Count.Subcount line 13
  2. lemma OAI.QAC.Count.Subcount.refl line 16
  3. lemma OAI.QAC.Count.Subcount.trans line 18
  4. lemma OAI.QAC.Count.Subcount.zero_eq line 22
  5. lemma OAI.QAC.Count.subcount_join_left line 32
  6. lemma OAI.QAC.Count.subcount_join_right line 36
  7. lemma OAI.QAC.Count.Subcount.join line 44
  8. lemma OAI.QAC.jointTest_support line 54
  9. lemma OAI.QAC.jointTest_disjoint line 60
  10. lemma OAI.QAC.jointTest_subcount line 68
  11. lemma OAI.QAC.reflectionTerms_subcount line 80
  12. lemma OAI.QAC.TensorSupported.disjoint_commute line 92
  13. lemma OAI.QAC.Count.zero_supported line 107
  14. lemma OAI.QAC.localMatrix_supported line 110
  15. def OAI.QAC.ReflectionLayer.touching line 114
  16. lemma OAI.QAC.ReflectionLayer.touching_length line 119
  17. lemma OAI.QAC.ReflectionLayer.touching_conjugate line 127
  18. def OAI.QAC.interiorTerm line 138
  19. lemma OAI.QAC.interiorTerm_supported line 142
  20. lemma OAI.QAC.interiorTerm_norm line 155
  21. lemma OAI.QAC.sandwich_factor line 161
  22. lemma OAI.QAC.Count.restrict_zero_pattern_commute line 180
  23. lemma OAI.QAC.Count.restrict_zero_high_commute line 193
  24. lemma OAI.QAC.Count.restrict_high_absorb line 204
  25. lemma OAI.QAC.Count.restrict_high_action_le line 221
  26. lemma OAI.QAC.Count.polynomial_action_error line 227