OAI/Probability/SKGap/Localization/ClosedMarked.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKGap.Noncrossing.ClosedMarked.Word line 15
  2. abbrev OAI.SKGap.Noncrossing.ClosedMarked.Polynomial line 16
  3. def OAI.SKGap.Noncrossing.ClosedMarked.matrixValue line 17
  4. def OAI.SKGap.Noncrossing.ClosedMarked.prediction line 20
  5. def OAI.SKGap.Noncrossing.ClosedMarked.ungrade line 23
  6. lemma OAI.SKGap.Noncrossing.ClosedMarked.ungrade_matrix line 25
  7. lemma OAI.SKGap.Noncrossing.ClosedMarked.ungrade_prediction line 29
  8. inductive OAI.SKGap.Noncrossing.ClosedMarked.Mark line 34
  9. def OAI.SKGap.Noncrossing.ClosedMarked.Mark.vector line 39
  10. def OAI.SKGap.Noncrossing.ClosedMarked.Mark.word line 42
  11. def OAI.SKGap.Noncrossing.ClosedMarked.Mark.scalar line 45
  12. def OAI.SKGap.Noncrossing.ClosedMarked.Mark.prepend line 48
  13. lemma OAI.SKGap.Noncrossing.ClosedMarked.Mark.prefix_vector line 51
  14. lemma OAI.SKGap.Noncrossing.ClosedMarked.Mark.prefix_scalar line 52
  15. lemma OAI.SKGap.Noncrossing.ClosedMarked.Mark.prefix_word line 53
  16. def OAI.SKGap.Noncrossing.ClosedMarked.Mark.diagnostic line 55
  17. lemma OAI.SKGap.Noncrossing.ClosedMarked.Mark.diagnostic_inverse line 59
  18. lemma OAI.SKGap.Noncrossing.ClosedMarked.Mark.trace_error line 63
  19. abbrev OAI.SKGap.Noncrossing.ClosedMarked.Marked line 87
  20. def OAI.SKGap.Noncrossing.ClosedMarked.Marked.plain line 90
  21. def OAI.SKGap.Noncrossing.ClosedMarked.Marked.budget line 91
  22. def OAI.SKGap.Noncrossing.ClosedMarked.Marked.prepend line 92
  23. def OAI.SKGap.Noncrossing.ClosedMarked.Marked.scale line 93
  24. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.plain_prefix line 94
  25. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.plain_scale line 97
  26. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.plain_append line 99
  27. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.budget_prefix line 100
  28. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.budget_scale line 102
  29. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.budget_append line 106
  30. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.budget_nonneg line 107
  31. theorem OAI.SKGap.Noncrossing.ClosedMarked.Marked.trace_error line 111
  32. lemma OAI.SKGap.Noncrossing.ClosedMarked.ungrade_append line 153
  33. lemma OAI.SKGap.Noncrossing.ClosedMarked.ungrade_bump line 154
  34. lemma OAI.SKGap.Noncrossing.ClosedMarked.ungrade_prepend line 156
  35. lemma OAI.SKGap.Noncrossing.ClosedMarked.ungrade_scale line 159
  36. def OAI.SKGap.Noncrossing.ClosedMarked.Marked.diagonalWords line 165
  37. def OAI.SKGap.Noncrossing.ClosedMarked.Marked.averageWords line 167
  38. def OAI.SKGap.Noncrossing.ClosedMarked.Marked.mass line 169
  39. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.plain_diagonalWords line 170
  40. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.plain_averageWords line 173
  41. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.budget_diagonalWords line 177
  42. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.budget_averageWords line 184
  43. lemma OAI.SKGap.Noncrossing.ClosedMarked.Marked.bounded_of_plain line 192
  44. abbrev OAI.SKGap.Noncrossing.ClosedMarked.Pair line 202
  45. def OAI.SKGap.Noncrossing.ClosedMarked.pairPlain line 203
  46. def OAI.SKGap.Noncrossing.ClosedMarked.pairUngrade line 204
  47. def OAI.SKGap.Noncrossing.ClosedMarked.zeroPair line 205
  48. lemma OAI.SKGap.Noncrossing.ClosedMarked.zeroPair_plain line 206
  49. def OAI.SKGap.Noncrossing.ClosedMarked.implicitPair line 210
  50. lemma OAI.SKGap.Noncrossing.ClosedMarked.implicitPair_plain line 216
  51. def OAI.SKGap.Noncrossing.ClosedMarked.smallBranch line 230
  52. def OAI.SKGap.Noncrossing.ClosedMarked.boundedBranch line 233
  53. lemma OAI.SKGap.Noncrossing.ClosedMarked.smallBranch_plain line 236
  54. lemma OAI.SKGap.Noncrossing.ClosedMarked.boundedBranch_plain line 244
  55. inductive OAI.SKGap.Noncrossing.ClosedMarked.SmallTree line 255
  56. def OAI.SKGap.Noncrossing.ClosedMarked.SmallTree.tree line 262
  57. def OAI.SKGap.Noncrossing.ClosedMarked.SmallTree.marked line 267
  58. lemma OAI.SKGap.Noncrossing.ClosedMarked.SmallTree.leafMass line 272
  59. lemma OAI.SKGap.Noncrossing.ClosedMarked.SmallTree.plain line 278
  60. theorem OAI.SKGap.Noncrossing.ClosedMarked.SmallTree.diagonal line 288