OAI/Probability/ThorpRouting/Adaptive/TailShapes.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ThorpNine.Adaptive.Thorp.Specht.TailShapes line 11
2. def OAI.ThorpNine.Adaptive.Thorp.Specht.tailShapePartition line 13
3. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.tailShapePartition_injective line 18
4. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.tail_shapes_count line 34
5. lemma OAI.ThorpNine.Adaptive.Thorp.tail_preserving_pairSwitch line 42
6. lemma OAI.ThorpNine.Adaptive.Thorp.pairSwitch_injective line 70
7. def OAI.ThorpNine.Adaptive.Thorp.Specht.pairFiberEquiv line 81
8. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.pair_sum_taboid_zero line 102
9. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.pair_operator_tall_zero line 111
10. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.palindrome_tall_zero line 135
11. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.palindrome_tall_zero_general line 148
12. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.twopow_tendsto line 163
13. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.twopow_nat_tendsto line 166
14. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.twopow_mul_eventually line 169
15. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.exp_two_absorb line 174
16. theorem OAI.ThorpNine.Adaptive.Thorp.Specht.exponential_dimension_spectral line 185
17. theorem OAI.ThorpNine.Adaptive.Thorp.Specht.spectral_regimes line 252
18. def OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.coordinateRelabel line 309
19. def OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.sweep line 315
20. abbrev OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.Tuples line 320
21. def OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.sweepKernel line 322
22. def OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.reflectedKernel line 326
23. def OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.regularAbsoluteEvenTrace line 331
24. def OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.MainStatement line 334
25. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.mean_nonneg line 349
26. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.mean_rpow_concave line 352
27. def OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.act line 364
28. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.act_nonneg line 367
29. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.act_rpow_le line 372
30. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.act_one_to_p line 380
31. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.act_b_to_pb line 429
32. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.kernel_pow_nonneg line 446
33. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.kernel_pow_row line 457
34. def OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.rowDensity line 468
35. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.rowDensity_nonneg line 472
36. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.rowDensity_succ line 476
37. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.rowDensity_mean line 483
38. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.rowDensity_moment_iter line 488
39. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.rowDensity_second_moment line 515
40. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.symmetric_kernel_smoothing line 537
41. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.density_exponent_numeric line 569
42. def OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.PermLaw.kernel line 581
43. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.PermLaw.nonneg line 585
44. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.PermLaw.row line 588
45. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.PermLaw.inverse line 593
46. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.PermLaw.col line 602
47. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.PermLaw.mul line 607
48. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.PermLaw.conjugate line 625
49. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.mul_nonneg_entries line 642
50. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.mul_row line 646
51. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.mul_col line 652
52. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.bound_mul_left line 658
53. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.bound_mul_right line 666
54. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.sandwich_power line 676
55. def OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.tuplePerm line 690
56. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.tuplePerm_apply line 697
57. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.tuplePerm_mul line 701
58. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.tuplePerm_inverse line 707
59. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.tupleProbability_kernel line 713
60. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.sweepKernel_law line 725
61. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.reflectedKernel_conjugate line 730
62. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.sweepKernel_nonneg line 753
63. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.sweepKernel_row line 756
64. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.sweepKernel_col line 761
65. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.reflected_nonneg line 766
66. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.reflected_row line 771
67. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.reflected_col line 775
68. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.reflected_symmetric line 779
69. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.reflected_moment line 782
70. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.tuples_card line 798
71. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.canonical_pointwise line 801
72. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.both_pointwise line 814
73. lemma OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.regular_trace_bound line 831
74. theorem OAI.ThorpNine.Adaptive.Thorp.StrongSmoothing.strong_smoothing line 848
75. abbrev OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.Site line 858
76. def OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.site line 860
77. lemma OAI.ThorpNine.Adaptive.Thorp.ButterflyReverse.site_injective line 866