OAI/Probability/ThorpRouting/Casimir/Main.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ThorpNine.Casimir.Thorp.CasimirBounds.palindrome_cost_mgf_coarse line 11
2. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.row_moment_coarse line 41
3. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.applyKernel_mul line 69
4. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.applyKernel_one line 85
5. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.symmetric_hs_power line 92
6. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.trace_power_le_hs line 106
7. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.palindrome_selfadjoint line 132
8. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.coefficient_trace_amplification line 140
9. def OAI.ThorpNine.Casimir.Thorp.CasimirBounds.tupleKernel line 193
10. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.palindrome_trace_amplification line 196
11. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.tupleKernel_symm line 221
12. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.tupleKernel_power64 line 225
13. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.K_selfadjoint line 249
14. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.K_norm_le_one line 253
15. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.fixed_trace_bound line 257
16. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.levelScale_ge line 280
17. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.choose_le_exp_levelScale line 288
18. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.trace_bound line 304
19. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.levelScale_le line 342
20. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.nontrivial_uniform_zero line 353
21. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.gap_of_uniform_zero line 364
22. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.nontrivial_gap line 372
23. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.eventual_level_dimension line 377
24. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.eventual_level_contraction line 415
25. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.finite_positive_lower line 436
26. theorem OAI.ThorpNine.Casimir.Thorp.CasimirBounds.level_contraction line 448
27. def OAI.ThorpNine.Casimir.Thorp.Specht.cardLabels line 487
28. def OAI.ThorpNine.Casimir.Thorp.Specht.cardRepresentation line 490
29. lemma OAI.ThorpNine.Casimir.Thorp.Specht.cardRepresentation_unitary line 494
30. instance OAI.ThorpNine.Casimir.Thorp.Specht.cardRepresentation_irreducible line 498
31. lemma OAI.ThorpNine.Casimir.Thorp.Specht.relabelledUnitary_neq line 502
32. lemma OAI.ThorpNine.Casimir.Thorp.Specht.cardRepresentation_distinct line 527
33. lemma OAI.ThorpNine.Casimir.Thorp.Specht.card_conjugacy_shapes line 532
34. lemma OAI.ThorpNine.Casimir.Thorp.Specht.row_zero_of_full_row line 537
35. lemma OAI.ThorpNine.Casimir.Thorp.Specht.tabloid_subsingleton_of_full_row line 543
36. lemma OAI.ThorpNine.Casimir.Thorp.Specht.representation_full_row line 554
37. lemma OAI.ThorpNine.Casimir.Thorp.Specht.relabelled_full_row line 564
38. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.sample_uniform_left line 575
39. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.uniform_zero_of_sample_norm_lt_one line 579
40. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.sampleOperator_trivial line 587
41. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.uniformOperator_trivial line 599
42. lemma OAI.ThorpNine.Casimir.Thorp.UnitaryFinite.weighted_sub line 604
43. lemma OAI.ThorpNine.Casimir.Thorp.physical_palindrome_norm line 615
44. lemma OAI.ThorpNine.Casimir.Thorp.physical_power_bound line 624
45. lemma OAI.ThorpNine.Casimir.Thorp.Specht.card_fourier_decay line 642
46. lemma OAI.ThorpNine.Casimir.Thorp.Specht.card_fourier_tall line 675
47. lemma OAI.ThorpNine.Casimir.Thorp.Specht.card_fourier_full_row line 691
48. lemma OAI.ThorpNine.Casimir.Thorp.Specht.half_geom_sum line 700
49. lemma OAI.ThorpNine.Casimir.Thorp.Specht.shape_weight_sum line 708
50. lemma OAI.ThorpNine.Casimir.Thorp.Specht.near_shape_term line 728
51. lemma OAI.ThorpNine.Casimir.Thorp.Specht.shapes_medium_sum line 750
52. lemma OAI.ThorpNine.Casimir.Thorp.sampleLaw_run line 775
53. lemma OAI.ThorpNine.Casimir.Thorp.physical_fourier_bound line 786
54. theorem OAI.ThorpNine.Casimir.Thorp.eventual_physical_bound line 812
55. lemma OAI.ThorpNine.Casimir.Thorp.physical_convergence line 880
56. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.K_source_square line 905
57. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.density_bound line 914
58. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.fromDistance_eq line 929
59. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.trace_real line 934
60. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.trace_power_real line 946
61. lemma OAI.ThorpNine.Casimir.Thorp.CasimirBounds.traceMoment_real line 951
62. theorem OAI.ThorpNine.Casimir.Thorp.CasimirBounds.casimir_main line 956