OAI/Probability/ThorpRouting/Casimir/TailShapes.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Casimir.Thorp.Specht.partition_count line 11
2. lemma OAI.ThorpNine.Casimir.Thorp.Specht.shapes_count line 16
3. lemma OAI.ThorpNine.Casimir.Thorp.Specht.rowLens_headD line 20
4. lemma OAI.ThorpNine.Casimir.Thorp.Specht.rowLens_tail_sum line 32
5. lemma OAI.ThorpNine.Casimir.Thorp.Specht.positive_list_eq_of_tail_sum line 43
6. abbrev OAI.ThorpNine.Casimir.Thorp.Specht.TailShapes line 70
7. def OAI.ThorpNine.Casimir.Thorp.Specht.tailShapePartition line 72
8. lemma OAI.ThorpNine.Casimir.Thorp.Specht.tailShapePartition_injective line 77
9. lemma OAI.ThorpNine.Casimir.Thorp.Specht.tail_shapes_count line 93
10. lemma OAI.ThorpNine.Casimir.Thorp.tail_preserving_pairSwitch line 101
11. lemma OAI.ThorpNine.Casimir.Thorp.pairSwitch_injective line 129
12. def OAI.ThorpNine.Casimir.Thorp.Specht.pairFiberEquiv line 140
13. lemma OAI.ThorpNine.Casimir.Thorp.Specht.pair_sum_taboid_zero line 161
14. lemma OAI.ThorpNine.Casimir.Thorp.Specht.pair_operator_tall_zero line 170
15. lemma OAI.ThorpNine.Casimir.Thorp.Specht.palindrome_tall_zero line 194
16. lemma OAI.ThorpNine.Casimir.Thorp.Specht.palindrome_tall_zero_general line 207
17. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.twopow_tendsto line 222
18. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.twopow_nat_tendsto line 225
19. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.twopow_mul_eventually line 228
20. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.exp_two_absorb line 233
21. theorem OAI.ThorpNine.Casimir.Thorp.Specht.exponential_dimension_spectral line 244
22. theorem OAI.ThorpNine.Casimir.Thorp.Specht.spectral_regimes line 311
23. def OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.coordinateRelabel line 368
24. def OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.sweep line 374
25. abbrev OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.Tuples line 379
26. def OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.sweepKernel line 381
27. def OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.reflectedKernel line 385
28. def OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.regularAbsoluteEvenTrace line 390
29. def OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.MainStatement line 393
30. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.mean_nonneg line 408
31. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.mean_rpow_concave line 411
32. def OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.act line 423
33. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.act_nonneg line 426
34. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.act_rpow_le line 431
35. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.act_one_to_p line 439
36. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.act_b_to_pb line 488
37. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.kernel_pow_nonneg line 505
38. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.kernel_pow_row line 516
39. def OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.rowDensity line 527
40. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.rowDensity_nonneg line 531
41. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.rowDensity_succ line 535
42. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.rowDensity_mean line 542
43. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.rowDensity_moment_iter line 547
44. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.rowDensity_second_moment line 574
45. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.symmetric_kernel_smoothing line 596
46. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.density_exponent_numeric line 628
47. def OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.PermLaw.kernel line 640
48. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.PermLaw.nonneg line 644
49. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.PermLaw.row line 647
50. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.PermLaw.inverse line 652
51. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.PermLaw.col line 661
52. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.PermLaw.mul line 666
53. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.PermLaw.conjugate line 684
54. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.mul_nonneg_entries line 701
55. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.mul_row line 705
56. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.mul_col line 711
57. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.bound_mul_left line 717
58. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.bound_mul_right line 725
59. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.sandwich_power line 735
60. def OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.tuplePerm line 749
61. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.tuplePerm_apply line 756
62. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.tuplePerm_mul line 760
63. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.tuplePerm_inverse line 766
64. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.tupleProbability_kernel line 772
65. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.sweepKernel_law line 784
66. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.reflectedKernel_conjugate line 789
67. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.sweepKernel_nonneg line 812
68. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.sweepKernel_row line 815
69. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.sweepKernel_col line 820
70. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.reflected_nonneg line 825
71. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.reflected_row line 830
72. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.reflected_col line 834
73. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.reflected_symmetric line 838
74. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.reflected_moment line 841
75. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.tuples_card line 857
76. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.canonical_pointwise line 860
77. lemma OAI.ThorpNine.Casimir.Thorp.StrongSmoothing.both_pointwise line 873