OAI/Probability/SKGap/Localization/Letter.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SKGap.Noncrossing.Letter line 12
  2. inductive OAI.SKGap.Noncrossing.Diagram line 17
  3. def OAI.SKGap.Noncrossing.Diagram.word line 26
  4. def OAI.SKGap.Noncrossing.Diagram.size line 31
  5. lemma OAI.SKGap.Noncrossing.Diagram.word_length line 36
  6. def OAI.SKGap.Noncrossing.Diagram.insert line 42
  7. lemma OAI.SKGap.Noncrossing.Diagram.insert_zero line 51
  8. lemma OAI.SKGap.Noncrossing.Diagram.insert_size line 54
  9. lemma OAI.SKGap.Noncrossing.Diagram.insert_word line 68
  10. structure OAI.SKGap.Noncrossing.Diagram.Cut line 106
  11. def OAI.SKGap.Noncrossing.Diagram.Cut.diag line 113
  12. def OAI.SKGap.Noncrossing.Diagram.Cut.inner line 115
  13. def OAI.SKGap.Noncrossing.Diagram.Cut.tail line 117
  14. def OAI.SKGap.Noncrossing.Diagram.cut line 120
  15. lemma OAI.SKGap.Noncrossing.Diagram.cut_spec line 130
  16. lemma OAI.SKGap.Noncrossing.Diagram.cut_insert line 174
  17. lemma OAI.SKGap.Noncrossing.Diagram.cut_exists_iff line 218
  18. def OAI.SKGap.Noncrossing.Diagram.labels line 243
  19. lemma OAI.SKGap.Noncrossing.Diagram.labels_nil line 247
  20. lemma OAI.SKGap.Noncrossing.Diagram.labels_diag line 248
  21. lemma OAI.SKGap.Noncrossing.Diagram.labels_noise line 252
  22. lemma OAI.SKGap.Noncrossing.Diagram.labels_append line 254
  23. def OAI.SKGap.Noncrossing.Diagram.supply line 258
  24. lemma OAI.SKGap.Noncrossing.Diagram.mem_supply line 265
  25. def OAI.SKGap.Noncrossing.Diagram.enumerate line 293
  26. theorem OAI.SKGap.Noncrossing.Diagram.mem_enumerate line 297
  27. def OAI.SKGap.Noncrossing.Diagram.Paired line 303
  28. instance OAI.SKGap.Noncrossing.Diagram.pairedFintype line 305
  29. def OAI.SKGap.Noncrossing.Diagram.CutAt line 308
  30. def OAI.SKGap.Noncrossing.Diagram.markedCut line 313
  31. lemma OAI.SKGap.Noncrossing.Diagram.cut_markedCut line 315
  32. def OAI.SKGap.Noncrossing.Diagram.cutEquiv line 319
  33. structure OAI.SKGap.Noncrossing.Diagram.PairShape line 340
  34. lemma OAI.SKGap.Noncrossing.Diagram.PairShape.length_bound line 348
  35. lemma OAI.SKGap.Noncrossing.Diagram.PairShape.before_eq_take line 355
  36. lemma OAI.SKGap.Noncrossing.Diagram.PairShape.between_eq_take line 360
  37. lemma OAI.SKGap.Noncrossing.Diagram.PairShape.after_eq_drop line 365
  38. def OAI.SKGap.Noncrossing.Diagram.PairShape.code line 372
  39. lemma OAI.SKGap.Noncrossing.Diagram.PairShape.code_injective line 376
  40. instance OAI.SKGap.Noncrossing.Diagram.pairShapeFinite line 388
  41. instance OAI.SKGap.Noncrossing.Diagram.pairShapeFintype line 390
  42. def OAI.SKGap.Noncrossing.Diagram.Separated line 393
  43. instance OAI.SKGap.Noncrossing.Diagram.separatedFintype line 396
  44. def OAI.SKGap.Noncrossing.Diagram.shapeOfCut line 399