OAI/Analysis/CharacterCriterion/ConePauli.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KirchbergRordam.GenericRW.Pauli.Label line 26
  2. abbrev OAI.KirchbergRordam.GenericRW.Pauli.M2 line 27
  3. abbrev OAI.KirchbergRordam.GenericRW.Pauli.e line 28
  4. lemma OAI.KirchbergRordam.GenericRW.Pauli.e_zero line 29
  5. lemma OAI.KirchbergRordam.GenericRW.Pauli.e_star line 30
  6. lemma OAI.KirchbergRordam.GenericRW.Pauli.e_square line 31
  7. lemma OAI.KirchbergRordam.GenericRW.Pauli.e_gram line 32
  8. lemma OAI.KirchbergRordam.GenericRW.Pauli.trace_mul line 33
  9. lemma OAI.KirchbergRordam.GenericRW.Pauli.ne_zero line 36
  10. def OAI.KirchbergRordam.GenericRW.Pauli.coeff line 40
  11. lemma OAI.KirchbergRordam.GenericRW.Pauli.coeff_apply line 42
  12. lemma OAI.KirchbergRordam.GenericRW.Pauli.coeff_e line 43
  13. lemma OAI.KirchbergRordam.GenericRW.Pauli.independent line 46
  14. def OAI.KirchbergRordam.GenericRW.Pauli.basis line 51
  15. lemma OAI.KirchbergRordam.GenericRW.Pauli.basis_apply line 54
  16. lemma OAI.KirchbergRordam.GenericRW.Pauli.coeff_sum line 55
  17. def OAI.KirchbergRordam.GenericRW.PauliPower.Row line 65
  18. def OAI.KirchbergRordam.GenericRW.PauliPower.Label line 69
  19. instance OAI.KirchbergRordam.GenericRW.PauliPower.rowFintype line 73
  20. instance OAI.KirchbergRordam.GenericRW.PauliPower.rowDecidableEq line 76
  21. instance OAI.KirchbergRordam.GenericRW.PauliPower.labelFintype line 79
  22. instance OAI.KirchbergRordam.GenericRW.PauliPower.labelDecidableEq line 82
  23. abbrev OAI.KirchbergRordam.GenericRW.PauliPower.Mat line 86
  24. def OAI.KirchbergRordam.GenericRW.PauliPower.e line 88
  25. lemma OAI.KirchbergRordam.GenericRW.PauliPower.row_card line 93
  26. lemma OAI.KirchbergRordam.GenericRW.PauliPower.label_card line 105
  27. lemma OAI.KirchbergRordam.GenericRW.PauliPower.e_star line 115
  28. lemma OAI.KirchbergRordam.GenericRW.PauliPower.e_square line 126
  29. lemma OAI.KirchbergRordam.GenericRW.PauliPower.trace_mul line 135
  30. def OAI.KirchbergRordam.GenericRW.PauliPower.coeff line 156
  31. lemma OAI.KirchbergRordam.GenericRW.PauliPower.coeff_apply line 158
  32. lemma OAI.KirchbergRordam.GenericRW.PauliPower.coeff_e line 160
  33. lemma OAI.KirchbergRordam.GenericRW.PauliPower.independent line 164
  34. def OAI.KirchbergRordam.GenericRW.PauliPower.basis line 170
  35. lemma OAI.KirchbergRordam.GenericRW.PauliPower.basis_apply line 175
  36. lemma OAI.KirchbergRordam.GenericRW.PauliPower.coeff_sum line 176
  37. abbrev OAI.KirchbergRordam.GenericRW.PauliPower.CMat line 182
  38. instance OAI.KirchbergRordam.GenericRW.PauliPower.(instance at line 183) line 183
  39. def OAI.KirchbergRordam.GenericRW.PauliPower.ce line 185
  40. def OAI.KirchbergRordam.GenericRW.PauliPower.ccoeff line 186
  41. lemma OAI.KirchbergRordam.GenericRW.PauliPower.ccoeff_ce line 188
  42. lemma OAI.KirchbergRordam.GenericRW.PauliPower.ccoeff_sum line 190
  43. lemma OAI.KirchbergRordam.GenericRW.PauliPower.ce_star line 192
  44. lemma OAI.KirchbergRordam.GenericRW.PauliPower.ce_square line 194
  45. abbrev OAI.KirchbergRordam.GenericRW.ConePauli.E line 202
  46. lemma OAI.KirchbergRordam.GenericRW.ConePauli.E_zero line 203
  47. def OAI.KirchbergRordam.GenericRW.ConePauli.p line 204
  48. def OAI.KirchbergRordam.GenericRW.ConePauli.u line 205
  49. lemma OAI.KirchbergRordam.GenericRW.ConePauli.scalar_commute line 215
  50. lemma OAI.KirchbergRordam.GenericRW.ConePauli.u_gram line 223
  51. def OAI.KirchbergRordam.GenericRW.ConePauli.sectionMap line 233
  52. lemma OAI.KirchbergRordam.GenericRW.ConePauli.sectionMap_apply line 236
  53. def OAI.KirchbergRordam.GenericRW.ConePauli.coeff line 238
  54. lemma OAI.KirchbergRordam.GenericRW.ConePauli.coeff_zero line 240
  55. lemma OAI.KirchbergRordam.GenericRW.ConePauli.reconstruct line 254
  56. def OAI.KirchbergRordam.GenericRW.ConePauli.expansion line 261
  57. lemma OAI.KirchbergRordam.GenericRW.ConePauli.expansion_single line 266
  58. lemma OAI.KirchbergRordam.GenericRW.ConePauli.dense line 275
  59. abbrev OAI.KirchbergRordam.GenericRW.MatrixTensor.Mat line 327
  60. def OAI.KirchbergRordam.GenericRW.MatrixTensor.leftMatrixAlgebra line 329
  61. def OAI.KirchbergRordam.GenericRW.MatrixTensor.rightMatrixAlgebra line 346
  62. def OAI.KirchbergRordam.GenericRW.MatrixTensor.leftMatrix line 363
  63. def OAI.KirchbergRordam.GenericRW.MatrixTensor.rightMatrix line 368
  64. lemma OAI.KirchbergRordam.GenericRW.MatrixTensor.algebra_legs_commute line 374
  65. lemma OAI.KirchbergRordam.GenericRW.MatrixTensor.legs_commute line 390
  66. lemma OAI.KirchbergRordam.GenericRW.MatrixTensor.algebra_legs_product line 396
  67. lemma OAI.KirchbergRordam.GenericRW.MatrixTensor.legs_product line 412