OAI/InformationTheory/QuantumCircuit/ProductProjection.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QAC.tensorMatrix_one line 11
  2. lemma OAI.QAC.tensorMatrix_mul line 22
  3. lemma OAI.QAC.tensorMatrix_star line 30
  4. lemma OAI.QAC.tensorMatrix_zero_of_zero line 36
  5. lemma OAI.QAC.tensorMatrix_projection line 43
  6. lemma OAI.QAC.tensorMatrix_unitary line 56
  7. lemma OAI.QAC.rankOne_star line 65
  8. lemma OAI.QAC.normalized_complex line 69
  9. lemma OAI.QAC.rankOne_projection line 75
  10. lemma OAI.QAC.Count.zero_projection line 89
  11. lemma OAI.QAC.Count.pattern_projection line 96
  12. lemma OAI.QAC.Count.pattern_empty line 105
  13. lemma OAI.QAC.Count.pattern_mul line 108
  14. lemma OAI.QAC.sum_powerset_prod_ite line 131
  15. lemma OAI.QAC.prod_ite_mem line 149
  16. lemma OAI.QAC.tensorMatrix_sum_patterns line 160
  17. lemma OAI.QAC.Count.sum_pattern line 174
  18. lemma OAI.QAC.projection_sum line 181
  19. lemma OAI.QAC.Count.high_eq_sum_filter line 202
  20. lemma OAI.QAC.Count.high_projection line 207
  21. lemma OAI.QAC.Count.high_mul_zero line 216
  22. lemma OAI.QAC.Count.high_eq_zero line 231
  23. lemma OAI.QAC.orthogonal_sum_mul line 246
  24. lemma OAI.QAC.orthogonal_sum_star line 261
  25. lemma OAI.QAC.orthogonal_sum_norm_le line 271
  26. lemma OAI.QAC.Count.spectral_norm_le line 296