OAI/Analysis/Quantum/DimensionTen/PencilModel.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.blocksZ line 12

    Also declared: ComparatorChallenges/DimensionTenPair.lean:10 (same declaration text).

  2. def OAI.DimensionTen.blocks line 18

    Also declared: ComparatorChallenges/DimensionTenPair.lean:16 (same declaration text).

  3. def OAI.DimensionTen.pencil line 21
  4. def OAI.DimensionTen.pencilMap line 25

    Also declared: ComparatorChallenges/DimensionTenPair.lean:19 (same declaration text).

  5. def OAI.DimensionTen.projector line 28
  6. def OAI.DimensionTen.chart line 32
  7. abbrev OAI.DimensionTen.QuadraticIndex line 35
  8. def OAI.DimensionTen.quadraticEval line 37
  9. def OAI.DimensionTen.TwentyDirections line 43
  10. abbrev OAI.DimensionTen.Mat line 54

    Also declared: ComparatorChallenges/DimensionTenPair.lean:22 (same declaration text).

  11. def OAI.DimensionTen.IsComplexLinear line 56

    Also declared: ComparatorChallenges/DimensionTenPair.lean:24 (same declaration text).

  12. def OAI.DimensionTen.amplify line 61

    Also declared: ComparatorChallenges/DimensionTenPair.lean:28 (same declaration text).

  13. def OAI.DimensionTen.CompletelyPositive line 66

    Also declared: ComparatorChallenges/DimensionTenPair.lean:33 (same declaration text).

  14. def OAI.DimensionTen.PPT line 71

    Also declared: ComparatorChallenges/DimensionTenPair.lean:37 (same declaration text).

  15. def OAI.DimensionTen.separable line 75

    Also declared: ComparatorChallenges/DimensionTenPair.lean:41 (same declaration text).

  16. def OAI.DimensionTen.EntanglementBreaking line 80

    Also declared: ComparatorChallenges/DimensionTenPair.lean:46 (same declaration text).

  17. def OAI.DimensionTen.choi line 85

    Also declared: ComparatorChallenges/DimensionTenPair.lean:51 (same declaration text).

  18. def OAI.DimensionTen.tensorMap line 90

    Also declared: ComparatorChallenges/DimensionTenPair.lean:55 (same declaration text).

  19. def OAI.DimensionTen.hsAdjoint line 97

    Also declared: ComparatorChallenges/DimensionTenPair.lean:61 (same declaration text).

  20. def OAI.DimensionTen.symmetricPairs line 100

    Also declared: ComparatorChallenges/DimensionTenPair.lean:64 (same declaration text).

  21. def OAI.DimensionTen.exteriorPairs line 103

    Also declared: ComparatorChallenges/DimensionTenPair.lean:67 (same declaration text).

  22. def OAI.DimensionTen.symmetricIsometry line 106

    Also declared: ComparatorChallenges/DimensionTenPair.lean:70 (same declaration text).

  23. def OAI.DimensionTen.exteriorIsometry line 114

    Also declared: ComparatorChallenges/DimensionTenPair.lean:78 (same declaration text).

  24. def OAI.DimensionTen.hodgeComplement line 121

    Also declared: ComparatorChallenges/DimensionTenPair.lean:85 (same declaration text).

  25. def OAI.DimensionTen.firstSix line 125

    Also declared: ComparatorChallenges/DimensionTenPair.lean:89 (same declaration text).

  26. def OAI.DimensionTen.exteriorMap line 128

    Also declared: ComparatorChallenges/DimensionTenPair.lean:92 (same declaration text).

  27. def OAI.DimensionTen.complementaryMap line 133

    Also declared: ComparatorChallenges/DimensionTenPair.lean:97 (same declaration text).

  28. def OAI.DimensionTen.phiOne line 136

    Also declared: ComparatorChallenges/DimensionTenPair.lean:100 (same declaration text).

  29. def OAI.DimensionTen.phiTwo line 139

    Also declared: ComparatorChallenges/DimensionTenPair.lean:103 (same declaration text).

  30. def OAI.DimensionTen.compositeChoi line 142

    Also declared: ComparatorChallenges/DimensionTenPair.lean:106 (same declaration text).

  31. def OAI.DimensionTen.productVector line 145

    Also declared: ComparatorChallenges/DimensionTenPair.lean:109 (same declaration text).

  32. def OAI.DimensionTen.ExactDimensionTenPair line 149
  33. theorem OAI.DimensionTen.blocksZ_transpose_mul_comm line 156
  34. theorem OAI.DimensionTen.blocks_transpose_mul_comm line 161
  35. theorem OAI.DimensionTen.blocks_conjTranspose line 167
  36. theorem OAI.DimensionTen.pencilMap_projector_gram line 171
  37. theorem OAI.DimensionTen.pencilMap_projector_rank line 182
  38. theorem OAI.DimensionTen.pencilMap_projector_posSemidef line 186