OAI/Probability/ThorpRouting/Harmonic/Site.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.regular_trace_bound line 11
2. theorem OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.strong_smoothing line 28
3. abbrev OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.Site line 38
4. def OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.site line 40
5. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.site_injective line 46
6. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.site_surjective line 79
7. def OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.siteEquiv line 96
8. def OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.reverseCard line 99
9. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.reverseCard_apply line 105
10. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.reverseCard_involutive line 108
11. def OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.mirrorSite line 111
12. def OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.mirrorSwitch line 117
13. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.site_mirrorSwitch line 120
14. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.routeDomain_site line 124
15. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.routeValue_site line 177
16. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.mirrorSwitch_involutive line 186
17. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.mirror_routeDomain line 193
18. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.mirror_routeValue line 216
19. def OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.mirrorCoins line 223
20. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.mirror_endpoint line 229
21. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.butterfly_mirror line 244
22. def OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.reverseOrder line 254
23. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.relabel_mul line 260
24. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.relabel_reverse line 264
25. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.reverseCard_sq line 267
26. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.sweep_mirror line 271
27. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.sweepKernel_reverse line 285
28. lemma OAI.ThorpNine.Harmonic.Thorp.ButterflyReverse.reflectedKernel_reverse line 300
29. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.mem_tailDiagram line 314
30. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.tail_height line 328
31. def OAI.ThorpNine.Harmonic.Thorp.StrongTail.tailCellEquiv line 333
32. abbrev OAI.ThorpNine.Harmonic.Thorp.StrongTail.upCell line 347
33. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.upCell_row line 349
34. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.upCell_col line 350
35. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.tail_card_eq line 352
36. def OAI.ThorpNine.Harmonic.Thorp.StrongTail.extendPerm line 355
37. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.extendPerm_up line 358
38. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.extendPerm_top line 362
39. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.extendPerm_inv line 366
40. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.extendPerm_sign line 369
41. def OAI.ThorpNine.Harmonic.Thorp.StrongTail.liftRows line 373
42. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.liftRows_up line 381
43. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.liftRows_top line 385
44. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.liftRows_perm line 388
45. def OAI.ThorpNine.Harmonic.Thorp.StrongTail.liftTabloid line 400
46. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.liftTabloid_base line 403
47. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.liftTabloid_action line 415
48. def OAI.ThorpNine.Harmonic.Thorp.StrongTail.restrictTabloids line 430
49. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.restrict_action line 436
50. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.extend_colGroup line 444
51. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.restrict_polytabloid line 454
52. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.tail_space_le_image line 477
53. theorem OAI.ThorpNine.Harmonic.Thorp.StrongTail.tail_dimension_le line 484
54. def OAI.ThorpNine.Harmonic.Thorp.StrongTail.DensityAt line 491
55. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.reflected_nonneg_both line 502
56. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.reflected_symm_both line 509
57. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.reflected_moment_both line 516
58. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.reflected_moment_small line 526
59. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.log_factorial_le_power line 554
60. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.log_normalization_le line 560
61. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.normalized_moment_identity line 587
62. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.density_at_small_exponent line 603
63. def OAI.ThorpNine.Harmonic.Thorp.Casimir.traceMoment line 648
64. def OAI.ThorpNine.Harmonic.Thorp.Casimir.fromDistance line 652
65. def OAI.ThorpNine.Harmonic.Thorp.Casimir.MainStatement line 656
66. theorem OAI.ThorpNine.Harmonic.Thorp.Casimir.cycleCoefficient_decay line 671
67. theorem OAI.ThorpNine.Harmonic.Thorp.Casimir.palindrome_slab_partial_mgf line 737
68. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.palindrome_slab_adapted_mul_le line 782
69. theorem OAI.ThorpNine.Harmonic.Thorp.Casimir.palindrome_family_mgf line 793
70. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.palindrome_family_mgf_decay line 829
71. theorem OAI.ThorpNine.Harmonic.Thorp.Casimir.palindrome_high_mgf line 840
72. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.palindrome_high_full_mgf line 857