OAI/InformationTheory/Entanglement/CombinatorialQuestions.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiniteConstruction.Question line 11
  2. abbrev OAI.FiniteConstruction.Coordinate line 12
  3. def OAI.FiniteConstruction.sign line 13
  4. def OAI.FiniteConstruction.s line 14
  5. def OAI.FiniteConstruction.u line 15
  6. def OAI.FiniteConstruction.baseOrth line 16
  7. lemma OAI.FiniteConstruction.baseOrth_symm line 17
  8. lemma OAI.FiniteConstruction.sign_sum line 20
  9. lemma OAI.FiniteConstruction.base_gram line 36
  10. lemma OAI.FiniteConstruction.base_unit line 43
  11. lemma OAI.FiniteConstruction.question_gram line 46
  12. lemma OAI.FiniteConstruction.question_unit line 57
  13. lemma OAI.FiniteConstruction.question_card line 62
  14. lemma OAI.FiniteConstruction.coordinate_card line 65
  15. lemma OAI.FiniteConstruction.base_gram_zero_iff line 66
  16. lemma OAI.FiniteConstruction.question_orth_iff line 76
  17. lemma OAI.FiniteConstruction.no_orthogonal_eight_bound line 81