OAI/Probability/ThorpRouting/Adaptive/SiteEquiv.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.site_surjective line 11
2. def OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.siteEquiv line 28
3. def OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.reverseCard line 31
4. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.reverseCard_apply line 37
5. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.reverseCard_involutive line 40
6. def OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.mirrorSite line 43
7. def OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.mirrorSwitch line 49
8. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.site_mirrorSwitch line 52
9. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.routeDomain_site line 56
10. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.routeValue_site line 109
11. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.mirrorSwitch_involutive line 118
12. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.mirror_routeDomain line 125
13. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.mirror_routeValue line 148
14. def OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.mirrorCoins line 155
15. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.mirror_endpoint line 161
16. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.butterfly_mirror line 176
17. def OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.reverseOrder line 186
18. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.relabel_mul line 192
19. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.relabel_reverse line 196
20. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.reverseCard_sq line 199
21. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.sweep_mirror line 203
22. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.sweepKernel_reverse line 217
23. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.reflectedKernel_reverse line 232
24. def OAI.ThorpNine.Adaptive.Thorp.StrongTail.tailDiagram line 246
25. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.mem_tailDiagram line 249
26. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.tail_height line 263
27. def OAI.ThorpNine.Adaptive.Thorp.StrongTail.tailCellEquiv line 268
28. abbrev OAI.ThorpNine.Adaptive.Thorp.StrongTail.upCell line 282
29. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.upCell_row line 284
30. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.upCell_col line 285
31. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.tail_card_eq line 287
32. def OAI.ThorpNine.Adaptive.Thorp.StrongTail.extendPerm line 290
33. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.extendPerm_up line 293
34. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.extendPerm_top line 297
35. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.extendPerm_inv line 301
36. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.extendPerm_sign line 304
37. def OAI.ThorpNine.Adaptive.Thorp.StrongTail.liftRows line 308
38. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.liftRows_up line 316
39. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.liftRows_top line 320
40. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.liftRows_perm line 323
41. def OAI.ThorpNine.Adaptive.Thorp.StrongTail.liftTabloid line 335
42. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.liftTabloid_base line 338
43. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.liftTabloid_action line 350
44. def OAI.ThorpNine.Adaptive.Thorp.StrongTail.restrictTabloids line 365
45. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.restrict_action line 371
46. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.extend_colGroup line 379
47. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.restrict_polytabloid line 389
48. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.tail_space_le_image line 412
49. theorem OAI.ThorpNine.Adaptive.Thorp.StrongTail.tail_dimension_le line 419
50. def OAI.ThorpNine.Adaptive.Thorp.StrongTail.DensityAt line 426
51. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.reflected_nonneg_both line 437
52. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.reflected_symm_both line 444
53. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.reflected_moment_both line 451
54. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.reflected_moment_small line 461
55. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.log_factorial_le_power line 489
56. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.log_normalization_le line 495
57. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.normalized_moment_identity line 522
58. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.density_at_small_exponent line 538
59. def OAI.ThorpNine.Adaptive.Thorp.Casimir.K line 583
60. def OAI.ThorpNine.Adaptive.Thorp.Casimir.traceMoment line 588
61. def OAI.ThorpNine.Adaptive.Thorp.Casimir.fromDistance line 592
62. def OAI.ThorpNine.Adaptive.Thorp.Casimir.MainStatement line 596
63. theorem OAI.ThorpNine.Adaptive.Thorp.Casimir.cycleCoefficient_decay line 611
64. theorem OAI.ThorpNine.Adaptive.Thorp.Casimir.palindrome_slab_partial_mgf line 677
65. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.palindrome_slab_adapted_mul_le line 722
66. theorem OAI.ThorpNine.Adaptive.Thorp.Casimir.palindrome_family_mgf line 733
67. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.palindrome_family_mgf_decay line 769
68. theorem OAI.ThorpNine.Adaptive.Thorp.Casimir.palindrome_high_mgf line 780
69. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.palindrome_high_full_mgf line 797
70. theorem OAI.ThorpNine.Adaptive.Thorp.Casimir.palindrome_cost_mgf_coarse line 809
71. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.row_moment_coarse line 839