OAI/Probability/SKGap/Matrix/ClosedTrace.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.Noncrossing.exactWord_append line 17
  2. lemma OAI.SKGap.Noncrossing.exactWord_diag line 25
  3. lemma OAI.SKGap.Noncrossing.wordPrediction_diag line 29
  4. lemma OAI.SKGap.Noncrossing.trace_small_diagonal_error line 44
  5. theorem OAI.SKGap.Noncrossing.rotated_small_word_trace_error line 53
  6. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.matrixValue line 78
  7. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.trace_list_error line 81
  8. theorem OAI.SKGap.Noncrossing.Primary.Tensor.Series.GradedWords.closed_source_trace_bound line 111
  9. inductive OAI.SKGap.Noncrossing.Primary.SmallMark line 133
  10. def OAI.SKGap.Noncrossing.Primary.SmallMark.vector line 139
  11. def OAI.SKGap.Noncrossing.Primary.SmallMark.word line 143
  12. def OAI.SKGap.Noncrossing.Primary.SmallMark.scalar line 147
  13. def OAI.SKGap.Noncrossing.Primary.SmallMark.prepend line 151
  14. lemma OAI.SKGap.Noncrossing.Primary.SmallMark.prefix_vector line 155
  15. lemma OAI.SKGap.Noncrossing.Primary.SmallMark.prefix_scalar line 156
  16. lemma OAI.SKGap.Noncrossing.Primary.SmallMark.prefix_word line 157
  17. def OAI.SKGap.Noncrossing.Primary.SmallMark.diagnostic line 160
  18. lemma OAI.SKGap.Noncrossing.Primary.SmallMark.average_norm_product line 164
  19. lemma OAI.SKGap.Noncrossing.Primary.SmallMark.rotated_trace_error line 172
  20. theorem OAI.SKGap.Noncrossing.Primary.SmallMark.trace_error line 188
  21. abbrev OAI.SKGap.Noncrossing.Primary.MarkedPolynomial line 213
  22. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.plain line 216
  23. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.budget line 218
  24. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.prepend line 221
  25. def OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.scale line 223
  26. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.plain_prefix line 225
  27. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.plain_scale line 228
  28. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.plain_append line 230
  29. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.budget_prefix line 231
  30. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.budget_scale line 233
  31. lemma OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.budget_append line 237
  32. theorem OAI.SKGap.Noncrossing.Primary.MarkedPolynomial.trace_error line 239