OAI/Probability/ThorpRouting/Adaptive/Main.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.trace_power_real line 12
2. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.traceMoment_real line 17
3. theorem OAI.ThorpNine.Adaptive.Thorp.Casimir.casimir_main line 22
4. def OAI.ThorpNine.Adaptive.Thorp.StrongTail.MainStatement line 39
5. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.dimension_le_factorial line 46
6. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.tail_card_exact line 54
7. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.tail_dimension_le_factorial line 58
8. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.sweep_sq_palindrome line 62
9. lemma OAI.ThorpNine.Adaptive.Thorp.StrongTail.sweep_sq_le_one line 75
10. theorem OAI.ThorpNine.Adaptive.Thorp.StrongTail.strong_tail line 80
11. abbrev OAI.ThorpNine.Adaptive.Thorp.Harmonic.tail line 154
12. def OAI.ThorpNine.Adaptive.Thorp.Harmonic.W line 155
13. def OAI.ThorpNine.Adaptive.Thorp.Harmonic.tupleTrace line 156
14. def OAI.ThorpNine.Adaptive.Thorp.Harmonic.MainStatement line 159
15. lemma OAI.ThorpNine.Adaptive.Thorp.Harmonic.dimension_contraction line 182
16. lemma OAI.ThorpNine.Adaptive.Thorp.Harmonic.exp_intersection line 229
17. lemma OAI.ThorpNine.Adaptive.Thorp.Harmonic.flat_tuple_trace line 238
18. theorem OAI.ThorpNine.Adaptive.Thorp.Harmonic.harmonic_cycle_main line 254
19. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh line 323
20. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.width line 327
21. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh_ge line 329
22. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.width_ge line 334
23. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh_step line 338
24. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh_lower line 340
25. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.width_lower line 345
26. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.width_pos line 351
27. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh_monotone line 353
28. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh_strictMono line 359
29. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.width_le line 366
30. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh_growth line 369
31. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh_growth_iter line 376
32. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh_seven line 387
33. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh_fresh line 395
34. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.mesh_fresh_first line 402
35. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.coefficient_decay line 407
36. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.bandCost line 474
37. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.band_adapted line 478
38. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.band_gt line 485
39. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.band_partial_mgf line 491
40. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.band_adapted_mgf line 533
41. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.bandEnd line 544
42. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.bandEnd_fresh line 548
43. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.bandEnd_ge line 555
44. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.familyCost line 560
45. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.family_adapted line 564
46. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.family_mgf line 573
47. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.familyBound line 607
48. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.familyBound_pos line 609
49. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.family_decay line 614
50. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.family_mgf_bound line 634
51. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.low_band line 646
52. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.low_bands line 654
53. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.cost_families line 665
54. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.high_mgf line 678
55. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.high_full_mgf line 702
56. def OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.densityConstant line 712
57. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.densityConstant_pos line 714
58. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.cost_mgf line 718
59. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.row_moment line 756
60. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.rpow_two_thirds_sq line 781
61. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.rpow_one_third_sq line 785
62. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.rpow_thirds line 789
63. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.young_cauchy line 793
64. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.row_convolution_moment line 822
65. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.kernel_fourth_hs line 852
66. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.even_trace_hs line 895
67. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.coefficient_even_trace_amplification line 915
68. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.palindrome_even_trace_amplification line 960
69. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.tuple_fourth_hs line 989
70. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.fixed_trace_bound line 1013
71. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.dimension_trace_bound line 1025
72. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.positiveSquare_norm line 1068
73. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.positiveSquare_selfadjoint line 1072
74. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.trace_mul_fourth_comm line 1077
75. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.F_norm line 1087
76. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.F_false line 1093
77. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.trace_eq line 1097
78. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.fourthTrace_real line 1109
79. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.fourthTrace_bound line 1115
80. lemma OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.zero_level_dimension line 1133
81. theorem OAI.ThorpNine.Adaptive.Thorp.AdaptiveBounds.adaptive_main line 1157