OAI/Probability/SKGap/Localization/PrimaryPrediction.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SKGap.Noncrossing.Primary.Partial line 13
  2. def OAI.SKGap.Noncrossing.Primary.Partial.word line 19
  3. def OAI.SKGap.Noncrossing.Primary.Partial.head line 22
  4. def OAI.SKGap.Noncrossing.Primary.Partial.diag line 25
  5. def OAI.SKGap.Noncrossing.Primary.Partial.create line 28
  6. def OAI.SKGap.Noncrossing.Primary.Partial.contract line 29
  7. def OAI.SKGap.Noncrossing.Primary.Partial.noise line 33
  8. lemma OAI.SKGap.Noncrossing.Primary.Partial.word_diag line 35
  9. lemma OAI.SKGap.Noncrossing.Primary.Partial.word_create line 37
  10. lemma OAI.SKGap.Noncrossing.Primary.Partial.word_contract line 38
  11. lemma OAI.SKGap.Noncrossing.Primary.Partial.diag_injective line 43
  12. lemma OAI.SKGap.Noncrossing.Primary.Partial.create_injective line 45
  13. lemma OAI.SKGap.Noncrossing.Primary.Partial.contract_injective line 47
  14. lemma OAI.SKGap.Noncrossing.Primary.Partial.create_ne_contract line 56
  15. lemma OAI.SKGap.Noncrossing.Primary.Partial.diag_preimage line 61
  16. lemma OAI.SKGap.Noncrossing.Primary.Partial.noise_preimage line 75
  17. def OAI.SKGap.Noncrossing.Primary.Partial.enumerate line 96
  18. lemma OAI.SKGap.Noncrossing.Primary.Partial.mem_enumerate line 101
  19. lemma OAI.SKGap.Noncrossing.Primary.Partial.noise_nodup line 123
  20. lemma OAI.SKGap.Noncrossing.Primary.Partial.noise_disjoint line 127
  21. lemma OAI.SKGap.Noncrossing.Primary.Partial.enumerate_nodup line 136
  22. abbrev OAI.SKGap.Noncrossing.Primary.D line 149
  23. abbrev OAI.SKGap.Noncrossing.Primary.Stack line 150
  24. abbrev OAI.SKGap.Noncrossing.Primary.Space line 151
  25. def OAI.SKGap.Noncrossing.Primary.ket line 153
  26. def OAI.SKGap.Noncrossing.Primary.diagonal line 155
  27. def OAI.SKGap.Noncrossing.Primary.creation line 157
  28. def OAI.SKGap.Noncrossing.Primary.annihilation line 159
  29. def OAI.SKGap.Noncrossing.Primary.noise line 163
  30. def OAI.SKGap.Noncrossing.Primary.vacuum line 165
  31. def OAI.SKGap.Noncrossing.Primary.project line 166
  32. lemma OAI.SKGap.Noncrossing.Primary.diagonal_ket line 170
  33. lemma OAI.SKGap.Noncrossing.Primary.creation_ket line 173
  34. lemma OAI.SKGap.Noncrossing.Primary.annihilation_ket_nil line 175
  35. lemma OAI.SKGap.Noncrossing.Primary.annihilation_ket_cons line 177
  36. lemma OAI.SKGap.Noncrossing.Primary.project_ket_nil line 180
  37. lemma OAI.SKGap.Noncrossing.Primary.project_ket_cons line 183
  38. def OAI.SKGap.Noncrossing.Primary.letter line 186
  39. def OAI.SKGap.Noncrossing.Primary.word line 190
  40. def OAI.SKGap.Noncrossing.Primary.outer line 194
  41. def OAI.SKGap.Noncrossing.Primary.coefficient line 199
  42. lemma OAI.SKGap.Noncrossing.Primary.value_factor line 204
  43. lemma OAI.SKGap.Noncrossing.Primary.mean_value line 210
  44. def OAI.SKGap.Noncrossing.Primary.Partial.stack line 214
  45. def OAI.SKGap.Noncrossing.Primary.Partial.coefficient line 217
  46. def OAI.SKGap.Noncrossing.Primary.Partial.state line 221
  47. lemma OAI.SKGap.Noncrossing.Primary.Partial.state_diag line 224
  48. lemma OAI.SKGap.Noncrossing.Primary.Partial.state_create line 227
  49. lemma OAI.SKGap.Noncrossing.Primary.Partial.state_contract line 230
  50. lemma OAI.SKGap.Noncrossing.Primary.Partial.state_noise line 237
  51. lemma OAI.SKGap.Noncrossing.Primary.word_vacuum line 242
  52. lemma OAI.SKGap.Noncrossing.Primary.Partial.project_state_done line 257
  53. lemma OAI.SKGap.Noncrossing.Primary.Partial.project_state_more line 260
  54. lemma OAI.SKGap.Noncrossing.Primary.prediction_as_finset line 264
  55. theorem OAI.SKGap.Noncrossing.Primary.project_word line 278
  56. def OAI.SKGap.Noncrossing.Primary.previousDiagonal line 302
  57. def OAI.SKGap.Noncrossing.Primary.creationLabels line 306
  58. def OAI.SKGap.Noncrossing.Primary.primaryOperator line 310
  59. theorem OAI.SKGap.Noncrossing.Primary.primaryOperator_vacuum line 318
  60. theorem OAI.SKGap.Noncrossing.Primary.primaryOperator_prediction_zero line 327
  61. abbrev OAI.SKGap.Noncrossing.Primary.WordPolynomial line 333
  62. def OAI.SKGap.Noncrossing.Primary.prependWords line 335
  63. def OAI.SKGap.Noncrossing.Primary.scale line 337
  64. def OAI.SKGap.Noncrossing.Primary.polynomialOperator line 340
  65. def OAI.SKGap.Noncrossing.Primary.polynomialPrediction line 344
  66. def OAI.SKGap.Noncrossing.Primary.primaryPolynomial line 347
  67. lemma OAI.SKGap.Noncrossing.Primary.word_append line 354
  68. lemma OAI.SKGap.Noncrossing.Primary.polynomialOperator_append line 359
  69. lemma OAI.SKGap.Noncrossing.Primary.polynomialOperator_prefix line 362
  70. lemma OAI.SKGap.Noncrossing.Primary.polynomialOperator_scale line 370
  71. lemma OAI.SKGap.Noncrossing.Primary.primaryPolynomial_operator line 378
  72. lemma OAI.SKGap.Noncrossing.Primary.polynomialPrediction_eq_project line 389
  73. theorem OAI.SKGap.Noncrossing.Primary.primaryPolynomial_prediction_zero line 399