OAI/Probability/ThorpRouting/Casimir/Site.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.regular_trace_bound line 11
2. theorem OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.strong_smoothing line 28
3. abbrev OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.Site line 38
4. def OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.site line 40
5. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.site_injective line 46
6. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.site_surjective line 79
7. def OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.siteEquiv line 96
8. def OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.reverseCard line 99
9. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.reverseCard_apply line 105
10. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.reverseCard_involutive line 108
11. def OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.mirrorSite line 111
12. def OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.mirrorSwitch line 117
13. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.site_mirrorSwitch line 120
14. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.routeDomain_site line 124
15. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.routeValue_site line 177
16. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.mirrorSwitch_involutive line 186
17. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.mirror_routeDomain line 193
18. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.mirror_routeValue line 216
19. def OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.mirrorCoins line 223
20. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.mirror_endpoint line 229
21. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.butterfly_mirror line 244
22. def OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.reverseOrder line 254
23. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.relabel_mul line 260
24. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.relabel_reverse line 264
25. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.reverseCard_sq line 267
26. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.sweep_mirror line 271
27. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.sweepKernel_reverse line 285
28. lemma OAI.ThorpNine.Casimir.Thorp.ButterflyReverse.reflectedKernel_reverse line 300
29. def OAI.ThorpNine.Casimir.Thorp.StrongTail.tailDiagram line 314
30. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.mem_tailDiagram line 317
31. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.tail_height line 331
32. def OAI.ThorpNine.Casimir.Thorp.StrongTail.tailCellEquiv line 336
33. abbrev OAI.ThorpNine.Casimir.Thorp.StrongTail.upCell line 350
34. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.upCell_row line 352
35. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.upCell_col line 353
36. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.tail_card_eq line 355
37. def OAI.ThorpNine.Casimir.Thorp.StrongTail.extendPerm line 358
38. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.extendPerm_up line 361
39. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.extendPerm_top line 365
40. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.extendPerm_inv line 369
41. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.extendPerm_sign line 372
42. def OAI.ThorpNine.Casimir.Thorp.StrongTail.liftRows line 376
43. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.liftRows_up line 384
44. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.liftRows_top line 388
45. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.liftRows_perm line 391
46. def OAI.ThorpNine.Casimir.Thorp.StrongTail.liftTabloid line 403
47. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.liftTabloid_base line 406
48. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.liftTabloid_action line 418
49. def OAI.ThorpNine.Casimir.Thorp.StrongTail.restrictTabloids line 433
50. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.restrict_action line 439
51. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.extend_colGroup line 447
52. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.restrict_polytabloid line 457
53. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.tail_space_le_image line 480
54. theorem OAI.ThorpNine.Casimir.Thorp.StrongTail.tail_dimension_le line 487
55. def OAI.ThorpNine.Casimir.Thorp.StrongTail.DensityAt line 494
56. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.reflected_nonneg_both line 505
57. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.reflected_symm_both line 512
58. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.reflected_moment_both line 519
59. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.reflected_moment_small line 529
60. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.log_factorial_le_power line 557
61. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.log_normalization_le line 563
62. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.normalized_moment_identity line 590
63. lemma OAI.ThorpNine.Casimir.Thorp.StrongTail.density_at_small_exponent line 606
64. theorem OAI.ThorpNine.Casimir.Thorp.CasimirBounds.cycleCoefficient_decay line 649
65. theorem OAI.ThorpNine.Casimir.Thorp.CasimirBounds.palindrome_slab_partial_mgf line 715
66. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.palindrome_slab_adapted_mul_le line 760
67. theorem OAI.ThorpNine.Casimir.Thorp.CasimirBounds.palindrome_family_mgf line 771
68. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.palindrome_family_mgf_decay line 807
69. theorem OAI.ThorpNine.Casimir.Thorp.CasimirBounds.palindrome_high_mgf line 818
70. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.palindrome_high_full_mgf line 835