OAI/Analysis/Quantum/DimensionTen/LowBasis.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DimensionTen.Border.low_zero line 10
  2. lemma OAI.DimensionTen.Border.low_shift_1 line 13
  3. lemma OAI.DimensionTen.Border.NB_shift_1 line 17
  4. lemma OAI.DimensionTen.Border.low_shift_2 line 20
  5. lemma OAI.DimensionTen.Border.NB_shift_2 line 24
  6. lemma OAI.DimensionTen.Border.low_shift_3 line 27
  7. lemma OAI.DimensionTen.Border.NB_shift_3 line 31
  8. lemma OAI.DimensionTen.Border.low_shift_4 line 34
  9. lemma OAI.DimensionTen.Border.NB_shift_4 line 39
  10. lemma OAI.DimensionTen.Border.low_shift_5 line 42
  11. lemma OAI.DimensionTen.Border.NB_shift_5 line 46
  12. lemma OAI.DimensionTen.Border.low_shift_6 line 49
  13. lemma OAI.DimensionTen.Border.NB_shift_6 line 54
  14. lemma OAI.DimensionTen.Border.low_shift_7 line 57
  15. lemma OAI.DimensionTen.Border.NB_shift_7 line 61
  16. lemma OAI.DimensionTen.Border.low_shift_8 line 64
  17. lemma OAI.DimensionTen.Border.NB_shift_8 line 68
  18. lemma OAI.DimensionTen.Border.low_shift_9 line 71
  19. lemma OAI.DimensionTen.Border.NB_shift_9 line 76
  20. lemma OAI.DimensionTen.Border.low_shift_10 line 79
  21. lemma OAI.DimensionTen.Border.NB_shift_10 line 84
  22. lemma OAI.DimensionTen.Border.low_shift_11 line 87
  23. lemma OAI.DimensionTen.Border.NB_shift_11 line 91
  24. lemma OAI.DimensionTen.Border.low_shift_12 line 94
  25. lemma OAI.DimensionTen.Border.NB_shift_12 line 99
  26. lemma OAI.DimensionTen.Border.low_shift_13 line 102
  27. lemma OAI.DimensionTen.Border.NB_shift_13 line 107
  28. lemma OAI.DimensionTen.Border.low_shift_14 line 110
  29. lemma OAI.DimensionTen.Border.NB_shift_14 line 114
  30. lemma OAI.DimensionTen.Border.low_shift_15 line 117
  31. lemma OAI.DimensionTen.Border.NB_shift_15 line 121
  32. lemma OAI.DimensionTen.Border.low_shift_16 line 124
  33. lemma OAI.DimensionTen.Border.NB_shift_16 line 128
  34. lemma OAI.DimensionTen.Border.low_shift_17 line 131
  35. lemma OAI.DimensionTen.Border.NB_shift_17 line 136
  36. lemma OAI.DimensionTen.Border.low_shift_18 line 139
  37. lemma OAI.DimensionTen.Border.NB_shift_18 line 144
  38. lemma OAI.DimensionTen.Border.low_shift_19 line 147
  39. lemma OAI.DimensionTen.Border.NB_shift_19 line 152
  40. lemma OAI.DimensionTen.Border.E_low_0 line 155
  41. lemma OAI.DimensionTen.Border.E_low_1 line 157
  42. lemma OAI.DimensionTen.Border.E_low_2 line 160
  43. lemma OAI.DimensionTen.Border.E_low_3 line 163
  44. lemma OAI.DimensionTen.Border.E_low_4 line 166
  45. lemma OAI.DimensionTen.Border.E_low_5 line 169
  46. lemma OAI.DimensionTen.Border.E_low_6 line 172
  47. lemma OAI.DimensionTen.Border.E_low_7 line 175
  48. lemma OAI.DimensionTen.Border.E_low_8 line 178
  49. lemma OAI.DimensionTen.Border.E_low_9 line 181
  50. lemma OAI.DimensionTen.Border.E_low_10 line 184
  51. lemma OAI.DimensionTen.Border.E_low_11 line 187
  52. lemma OAI.DimensionTen.Border.E_low_12 line 190
  53. lemma OAI.DimensionTen.Border.E_low_13 line 193
  54. lemma OAI.DimensionTen.Border.E_low_14 line 196
  55. lemma OAI.DimensionTen.Border.E_low_15 line 199
  56. lemma OAI.DimensionTen.Border.E_low_16 line 202
  57. lemma OAI.DimensionTen.Border.E_low_17 line 205
  58. lemma OAI.DimensionTen.Border.E_low_18 line 208
  59. lemma OAI.DimensionTen.Border.E_low_19 line 211
  60. lemma OAI.DimensionTen.Border.E_low line 214
  61. def OAI.DimensionTen.Border.basis line 238
  62. lemma OAI.DimensionTen.Border.basis_eq line 241
  63. lemma OAI.DimensionTen.Border.low_linearIndependent line 246