OAI/Probability/ThorpRouting/Tail/Main.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Tail.Thorp.StrongTail.tailCellEquiv line 12
  2. abbrev OAI.ThorpNine.Tail.Thorp.StrongTail.upCell line 26
  3. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.upCell_row line 28
  4. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.upCell_col line 29
  5. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.tail_card_eq line 31
  6. def OAI.ThorpNine.Tail.Thorp.StrongTail.extendPerm line 34
  7. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.extendPerm_up line 37
  8. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.extendPerm_top line 41
  9. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.extendPerm_inv line 45
  10. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.extendPerm_sign line 48
  11. def OAI.ThorpNine.Tail.Thorp.StrongTail.liftRows line 52
  12. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.liftRows_up line 60
  13. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.liftRows_top line 64
  14. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.liftRows_perm line 67
  15. def OAI.ThorpNine.Tail.Thorp.StrongTail.liftTabloid line 79
  16. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.liftTabloid_base line 82
  17. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.liftTabloid_action line 94
  18. def OAI.ThorpNine.Tail.Thorp.StrongTail.restrictTabloids line 109
  19. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.restrict_action line 115
  20. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.extend_colGroup line 123
  21. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.restrict_polytabloid line 133
  22. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.tail_space_le_image line 156
  23. theorem OAI.ThorpNine.Tail.Thorp.StrongTail.tail_dimension_le line 163
  24. abbrev OAI.ThorpNine.Tail.Thorp.ButterflyReverse.Site line 172
  25. def OAI.ThorpNine.Tail.Thorp.ButterflyReverse.site line 174
  26. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.site_injective line 180
  27. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.site_surjective line 213
  28. def OAI.ThorpNine.Tail.Thorp.ButterflyReverse.siteEquiv line 230
  29. def OAI.ThorpNine.Tail.Thorp.ButterflyReverse.reverseCard line 233
  30. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.reverseCard_apply line 239
  31. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.reverseCard_involutive line 242
  32. def OAI.ThorpNine.Tail.Thorp.ButterflyReverse.mirrorSite line 245
  33. def OAI.ThorpNine.Tail.Thorp.ButterflyReverse.mirrorSwitch line 251
  34. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.site_mirrorSwitch line 254
  35. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.routeDomain_site line 258
  36. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.routeValue_site line 311
  37. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.mirrorSwitch_involutive line 320
  38. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.mirror_routeDomain line 327
  39. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.mirror_routeValue line 350
  40. def OAI.ThorpNine.Tail.Thorp.ButterflyReverse.mirrorCoins line 357
  41. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.mirror_endpoint line 363
  42. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.butterfly_mirror line 378
  43. def OAI.ThorpNine.Tail.Thorp.ButterflyReverse.reverseOrder line 388
  44. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.relabel_mul line 394
  45. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.relabel_reverse line 398
  46. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.reverseCard_sq line 401
  47. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.sweep_mirror line 405
  48. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.sweepKernel_reverse line 419
  49. lemma OAI.ThorpNine.Tail.Thorp.ButterflyReverse.reflectedKernel_reverse line 434
  50. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.reflected_nonneg_both line 448
  51. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.reflected_symm_both line 455
  52. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.reflected_moment_both line 462
  53. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.reflected_moment_small line 472
  54. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.log_factorial_le_power line 500
  55. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.log_normalization_le line 506
  56. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.normalized_moment_identity line 533
  57. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.density_at_small_exponent line 549
  58. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.dimension_le_factorial line 589
  59. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.tail_card_exact line 597
  60. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.tail_dimension_le_factorial line 601
  61. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.sweep_sq_palindrome line 605
  62. lemma OAI.ThorpNine.Tail.Thorp.StrongTail.sweep_sq_le_one line 618
  63. theorem OAI.ThorpNine.Tail.Thorp.StrongTail.strong_tail line 623