OAI/Probability/ThorpRouting/Harmonic/PalindromeFamilyCost.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Harmonic.Thorp.familyEnd_two line 10
2. lemma OAI.ThorpNine.Harmonic.Thorp.familyEnd_ge line 15
3. def OAI.ThorpNine.Harmonic.Thorp.palindromeFamilyCost line 23
4. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeFamilyCost_adapted line 27
5. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_family_mgf line 35
6. lemma OAI.ThorpNine.Harmonic.Thorp.pow_four_ge line 71
7. lemma OAI.ThorpNine.Harmonic.Thorp.sum_family_decay line 76
8. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeLevelCost_step_add line 101
9. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeLowCost_sum line 119
10. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeLowCost_slab line 132
11. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeCost_family line 139
12. lemma OAI.ThorpNine.Harmonic.Thorp.finiteMean_mul_sq_le line 154
13. lemma OAI.ThorpNine.Harmonic.Thorp.finiteMean_mul_exp_le line 160
14. def OAI.ThorpNine.Harmonic.Thorp.heightDecay line 178
15. lemma OAI.ThorpNine.Harmonic.Thorp.heightDecay_nonneg line 181
16. lemma OAI.ThorpNine.Harmonic.Thorp.heightDecay_antitone line 185
17. lemma OAI.ThorpNine.Harmonic.Thorp.palindrome_family_mgf_decay line 196
18. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_high_mgf line 207
19. lemma OAI.ThorpNine.Harmonic.Thorp.palindrome_high_full_mgf line 224
20. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_cost_mgf_cutoff line 236
21. lemma OAI.ThorpNine.Harmonic.Thorp.cutoffMass_le line 262
22. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeLowCost_le line 273
23. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_cost_mgf_coarse line 277
24. def OAI.ThorpNine.Harmonic.Thorp.momentBase line 314
25. lemma OAI.ThorpNine.Harmonic.Thorp.momentBase_one_le line 316
26. lemma OAI.ThorpNine.Harmonic.Thorp.momentBase_log line 319
27. lemma OAI.ThorpNine.Harmonic.Thorp.momentBase_pow line 325
28. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeRowMoment_le_cost line 329
29. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_row_moment_coarse line 346
30. def OAI.ThorpNine.Harmonic.Thorp.densityCutoff line 352
31. lemma OAI.ThorpNine.Harmonic.Thorp.log_small_density line 354
32. lemma OAI.ThorpNine.Harmonic.Thorp.densityCutoff_bounds line 362
33. lemma OAI.ThorpNine.Harmonic.Thorp.densityCutoff_decay line 376
34. lemma OAI.ThorpNine.Harmonic.Thorp.densityCutoff_power line 388
35. lemma OAI.ThorpNine.Harmonic.Thorp.densityCutoff_sparse line 409
36. lemma OAI.ThorpNine.Harmonic.Thorp.momentBase_log_exact line 424
37. lemma OAI.ThorpNine.Harmonic.Thorp.densityCutoff_le_height line 428
38. def OAI.ThorpNine.Harmonic.Thorp.densityTailConstant line 445
39. lemma OAI.ThorpNine.Harmonic.Thorp.densityTailConstant_nonneg line 448
40. lemma OAI.ThorpNine.Harmonic.Thorp.heightDecay_cutoff line 452
41. lemma OAI.ThorpNine.Harmonic.Thorp.sparse_low_algebra line 461
42. lemma OAI.ThorpNine.Harmonic.Thorp.palindrome_row_moment_small line 470
43. def OAI.ThorpNine.Harmonic.Thorp.densityConstant line 507
44. lemma OAI.ThorpNine.Harmonic.Thorp.densityConstant_pos line 510
45. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_row_moment_bound line 516
46. lemma OAI.ThorpNine.Harmonic.Thorp.palindromeRowMoment_nonneg line 551
47. theorem OAI.ThorpNine.Harmonic.Thorp.palindrome_log_row_moment line 558
48. lemma OAI.ThorpNine.Harmonic.Thorp.orbitSet_eq_of_agree line 571
49. def OAI.ThorpNine.Harmonic.Thorp.survivingCycle line 594
50. def OAI.ThorpNine.Harmonic.Thorp.perturbCycleMap line 603
51. lemma OAI.ThorpNine.Harmonic.Thorp.perturbCycleMap_injective line 611
52. theorem OAI.ThorpNine.Harmonic.Thorp.selectedCycle_perturb_le line 629
53. def OAI.ThorpNine.Harmonic.Thorp.permDistance line 637
54. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_sum line 640
55. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_refl line 645
56. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_le line 648
57. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_symm line 651
58. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_triangle line 654
59. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_mul_left line 664
60. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_mul_right line 673
61. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_inv line 679
62. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_mul_le line 686
63. lemma OAI.ThorpNine.Harmonic.Thorp.selectedCycle_distance_le line 691
64. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_alternating line 698
65. lemma OAI.ThorpNine.Harmonic.Thorp.alternatingCycles_distance_le line 704
66. def OAI.ThorpNine.Harmonic.Thorp.centralBlockPerm line 722
67. def OAI.ThorpNine.Harmonic.Thorp.centralPalindromePerm line 727
68. lemma OAI.ThorpNine.Harmonic.Thorp.centralPalindromePerm_step line 732
69. def OAI.ThorpNine.Harmonic.Thorp.centralLevelCost line 751
70. def OAI.ThorpNine.Harmonic.Thorp.centralSlabCost line 767
71. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_childLift line 771
72. def OAI.ThorpNine.Harmonic.Thorp.centralDistance line 795
73. lemma OAI.ThorpNine.Harmonic.Thorp.centralDistance_step line 798
74. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_centralBlock line 813
75. lemma OAI.ThorpNine.Harmonic.Thorp.permDistance_centralPalindrome line 822
76. lemma OAI.ThorpNine.Harmonic.Thorp.centralLevelCost_step line 829
77. lemma OAI.ThorpNine.Harmonic.Thorp.centralLevelCost_perturb line 846