OAI/Probability/ThorpRouting/Harmonic/Main.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ThorpNine.Harmonic.Thorp.Casimir.palindrome_cost_mgf_coarse line 11
2. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.row_moment_coarse line 41
3. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.applyKernel_mul line 69
4. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.applyKernel_one line 85
5. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.symmetric_hs_power line 92
6. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.trace_power_le_hs line 106
7. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.palindrome_selfadjoint line 132
8. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.coefficient_trace_amplification line 140
9. def OAI.ThorpNine.Harmonic.Thorp.Casimir.tupleKernel line 193
10. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.palindrome_trace_amplification line 196
11. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.tupleKernel_symm line 221
12. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.tupleKernel_power64 line 225
13. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.K_selfadjoint line 249
14. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.K_norm_le_one line 253
15. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.fixed_trace_bound line 257
16. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.levelScale_ge line 280
17. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.choose_le_exp_levelScale line 288
18. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.trace_bound line 304
19. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.levelScale_le line 342
20. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.nontrivial_uniform_zero line 353
21. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.gap_of_uniform_zero line 364
22. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.nontrivial_gap line 372
23. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.eventual_level_dimension line 377
24. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.eventual_level_contraction line 415
25. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.finite_positive_lower line 436
26. theorem OAI.ThorpNine.Harmonic.Thorp.Casimir.level_contraction line 448
27. def OAI.ThorpNine.Harmonic.Thorp.Specht.cardLabels line 487

    Also declared: ComparatorChallenges/CoordinateTrace.lean:324 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:401 (same declaration text).

28. def OAI.ThorpNine.Harmonic.Thorp.Specht.cardRepresentation line 490

    Also declared: ComparatorChallenges/CoordinateTrace.lean:327 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:404 (same declaration text).

29. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.cardRepresentation_unitary line 494
30. instance OAI.ThorpNine.Harmonic.Thorp.Specht.cardRepresentation_irreducible line 498
31. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.relabelledUnitary_neq line 502
32. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.cardRepresentation_distinct line 527
33. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_conjugacy_shapes line 532
34. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.row_zero_of_full_row line 537
35. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloid_subsingleton_of_full_row line 543
36. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.representation_full_row line 554
37. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.relabelled_full_row line 564
38. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sample_uniform_left line 575
39. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.uniform_zero_of_sample_norm_lt_one line 579
40. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_trivial line 587
41. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.uniformOperator_trivial line 599
42. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.weighted_sub line 604
43. lemma OAI.ThorpNine.Harmonic.Thorp.physical_palindrome_norm line 615
44. lemma OAI.ThorpNine.Harmonic.Thorp.physical_power_bound line 624
45. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_fourier_decay line 642
46. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_fourier_tall line 675
47. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_fourier_full_row line 691
48. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.half_geom_sum line 700
49. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.shape_weight_sum line 708
50. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.near_shape_term line 728
51. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.shapes_medium_sum line 750
52. lemma OAI.ThorpNine.Harmonic.Thorp.sampleLaw_run line 775
53. lemma OAI.ThorpNine.Harmonic.Thorp.physical_fourier_bound line 786
54. theorem OAI.ThorpNine.Harmonic.Thorp.eventual_physical_bound line 812
55. lemma OAI.ThorpNine.Harmonic.Thorp.physical_convergence line 880
56. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.K_source_square line 905
57. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.density_bound line 914
58. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.fromDistance_eq line 929
59. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.trace_real line 934
60. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.trace_power_real line 946
61. lemma OAI.ThorpNine.Harmonic.Thorp.Casimir.traceMoment_real line 951
62. theorem OAI.ThorpNine.Harmonic.Thorp.Casimir.casimir_main line 956
63. def OAI.ThorpNine.Harmonic.Thorp.StrongTail.MainStatement line 973
64. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.dimension_le_factorial line 980
65. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.tail_card_exact line 988
66. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.tail_dimension_le_factorial line 992
67. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.sweep_sq_palindrome line 996
68. lemma OAI.ThorpNine.Harmonic.Thorp.StrongTail.sweep_sq_le_one line 1009
69. theorem OAI.ThorpNine.Harmonic.Thorp.StrongTail.strong_tail line 1014
70. lemma OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.dimension_contraction line 1087
71. lemma OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.exp_intersection line 1134
72. lemma OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.flat_tuple_trace line 1143
73. theorem OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.harmonic_cycle_main line 1159