OAI/Probability/ThorpRouting/Harmonic/TailShapes.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.partition_count line 11
2. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.shapes_count line 16
3. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.rowLens_headD line 20
4. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.rowLens_tail_sum line 32
5. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.positive_list_eq_of_tail_sum line 43
6. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.TailShapes line 70
7. def OAI.ThorpNine.Harmonic.Thorp.Specht.tailShapePartition line 72
8. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tailShapePartition_injective line 77
9. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tail_shapes_count line 93
10. lemma OAI.ThorpNine.Harmonic.Thorp.tail_preserving_pairSwitch line 101
11. lemma OAI.ThorpNine.Harmonic.Thorp.pairSwitch_injective line 129
12. def OAI.ThorpNine.Harmonic.Thorp.Specht.pairFiberEquiv line 140
13. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.pair_sum_taboid_zero line 161
14. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.pair_operator_tall_zero line 170
15. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.palindrome_tall_zero line 194
16. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.palindrome_tall_zero_general line 207
17. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.twopow_tendsto line 222
18. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.twopow_nat_tendsto line 225
19. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.twopow_mul_eventually line 228
20. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.exp_two_absorb line 233
21. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.exponential_dimension_spectral line 244
22. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.spectral_regimes line 311
23. def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.regularAbsoluteEvenTrace line 368
24. def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.MainStatement line 371
25. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.mean_nonneg line 386
26. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.mean_rpow_concave line 389
27. def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.act line 401
28. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.act_nonneg line 404
29. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.act_rpow_le line 409
30. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.act_one_to_p line 417
31. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.act_b_to_pb line 466
32. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.kernel_pow_nonneg line 483
33. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.kernel_pow_row line 494
34. def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.rowDensity line 505
35. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.rowDensity_nonneg line 509
36. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.rowDensity_succ line 513
37. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.rowDensity_mean line 520
38. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.rowDensity_moment_iter line 525
39. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.rowDensity_second_moment line 552
40. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.symmetric_kernel_smoothing line 574
41. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.density_exponent_numeric line 606
42. def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.PermLaw.kernel line 618
43. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.PermLaw.nonneg line 622
44. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.PermLaw.row line 625
45. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.PermLaw.inverse line 630
46. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.PermLaw.col line 639
47. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.PermLaw.mul line 644
48. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.PermLaw.conjugate line 662
49. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.mul_nonneg_entries line 679
50. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.mul_row line 683
51. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.mul_col line 689
52. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.bound_mul_left line 695
53. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.bound_mul_right line 703
54. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.sandwich_power line 713
55. def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.tuplePerm line 727
56. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.tuplePerm_apply line 733
57. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.tuplePerm_mul line 736
58. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.tuplePerm_inverse line 741
59. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.tupleProbability_kernel line 748
60. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.sweepKernel_law line 760
61. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.reflectedKernel_conjugate line 765
62. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.sweepKernel_nonneg line 788
63. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.sweepKernel_row line 791
64. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.sweepKernel_col line 796
65. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.reflected_nonneg line 801
66. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.reflected_row line 806
67. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.reflected_col line 810
68. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.reflected_symmetric line 814
69. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.reflected_moment line 817
70. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.tuples_card line 833
71. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.canonical_pointwise line 836
72. lemma OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.both_pointwise line 849