OAI/Probability/ThorpRouting/SparseSaving/HeightDecay.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ThorpNine.SparseSaving.Thorp.palindrome_family_mgf line 10
2. lemma OAI.ThorpNine.SparseSaving.Thorp.pow_four_ge line 46
3. lemma OAI.ThorpNine.SparseSaving.Thorp.sum_family_decay line 51
4. lemma OAI.ThorpNine.SparseSaving.Thorp.palindromeLevelCost_step_add line 76
5. lemma OAI.ThorpNine.SparseSaving.Thorp.palindromeLowCost_sum line 94
6. lemma OAI.ThorpNine.SparseSaving.Thorp.palindromeLowCost_slab line 107
7. lemma OAI.ThorpNine.SparseSaving.Thorp.palindromeCost_family line 114
8. lemma OAI.ThorpNine.SparseSaving.Thorp.finiteMean_mul_sq_le line 129
9. lemma OAI.ThorpNine.SparseSaving.Thorp.finiteMean_mul_exp_le line 135
10. def OAI.ThorpNine.SparseSaving.Thorp.heightDecay line 153
11. lemma OAI.ThorpNine.SparseSaving.Thorp.heightDecay_nonneg line 156
12. lemma OAI.ThorpNine.SparseSaving.Thorp.heightDecay_antitone line 160
13. lemma OAI.ThorpNine.SparseSaving.Thorp.palindrome_family_mgf_decay line 171
14. theorem OAI.ThorpNine.SparseSaving.Thorp.palindrome_high_mgf line 182
15. lemma OAI.ThorpNine.SparseSaving.Thorp.palindrome_high_full_mgf line 199
16. theorem OAI.ThorpNine.SparseSaving.Thorp.palindrome_cost_mgf_cutoff line 211
17. lemma OAI.ThorpNine.SparseSaving.Thorp.cutoffMass_le line 237
18. lemma OAI.ThorpNine.SparseSaving.Thorp.palindromeLowCost_le line 248
19. theorem OAI.ThorpNine.SparseSaving.Thorp.palindrome_cost_mgf_coarse line 252
20. def OAI.ThorpNine.SparseSaving.Thorp.momentBase line 289
21. lemma OAI.ThorpNine.SparseSaving.Thorp.momentBase_one_le line 291
22. lemma OAI.ThorpNine.SparseSaving.Thorp.momentBase_log line 294
23. lemma OAI.ThorpNine.SparseSaving.Thorp.momentBase_pow line 300
24. lemma OAI.ThorpNine.SparseSaving.Thorp.palindromeRowMoment_le_cost line 304
25. theorem OAI.ThorpNine.SparseSaving.Thorp.palindrome_row_moment_coarse line 321
26. def OAI.ThorpNine.SparseSaving.Thorp.densityCutoff line 327
27. lemma OAI.ThorpNine.SparseSaving.Thorp.log_small_density line 329
28. lemma OAI.ThorpNine.SparseSaving.Thorp.densityCutoff_bounds line 337
29. lemma OAI.ThorpNine.SparseSaving.Thorp.densityCutoff_decay line 351
30. lemma OAI.ThorpNine.SparseSaving.Thorp.densityCutoff_power line 363
31. lemma OAI.ThorpNine.SparseSaving.Thorp.densityCutoff_sparse line 384
32. lemma OAI.ThorpNine.SparseSaving.Thorp.momentBase_log_exact line 399
33. lemma OAI.ThorpNine.SparseSaving.Thorp.densityCutoff_le_height line 403
34. def OAI.ThorpNine.SparseSaving.Thorp.densityTailConstant line 420
35. lemma OAI.ThorpNine.SparseSaving.Thorp.densityTailConstant_nonneg line 423
36. lemma OAI.ThorpNine.SparseSaving.Thorp.heightDecay_cutoff line 427
37. lemma OAI.ThorpNine.SparseSaving.Thorp.sparse_low_algebra line 436
38. lemma OAI.ThorpNine.SparseSaving.Thorp.palindrome_row_moment_small line 445
39. def OAI.ThorpNine.SparseSaving.Thorp.densityConstant line 482
40. lemma OAI.ThorpNine.SparseSaving.Thorp.densityConstant_pos line 485
41. theorem OAI.ThorpNine.SparseSaving.Thorp.palindrome_row_moment_bound line 491
42. lemma OAI.ThorpNine.SparseSaving.Thorp.palindromeRowMoment_nonneg line 526
43. theorem OAI.ThorpNine.SparseSaving.Thorp.palindrome_log_row_moment line 533
44. lemma OAI.ThorpNine.SparseSaving.Thorp.orbitSet_eq_of_agree line 546
45. def OAI.ThorpNine.SparseSaving.Thorp.survivingCycle line 569
46. def OAI.ThorpNine.SparseSaving.Thorp.perturbCycleMap line 578
47. lemma OAI.ThorpNine.SparseSaving.Thorp.perturbCycleMap_injective line 586
48. theorem OAI.ThorpNine.SparseSaving.Thorp.selectedCycle_perturb_le line 604
49. def OAI.ThorpNine.SparseSaving.Thorp.permDistance line 612
50. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_sum line 615
51. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_refl line 620
52. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_le line 623
53. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_symm line 626
54. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_triangle line 629
55. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_mul_left line 639
56. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_mul_right line 648
57. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_inv line 654
58. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_mul_le line 661
59. lemma OAI.ThorpNine.SparseSaving.Thorp.selectedCycle_distance_le line 666
60. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_alternating line 673
61. lemma OAI.ThorpNine.SparseSaving.Thorp.alternatingCycles_distance_le line 679
62. def OAI.ThorpNine.SparseSaving.Thorp.centralBlockPerm line 697
63. def OAI.ThorpNine.SparseSaving.Thorp.centralPalindromePerm line 702
64. lemma OAI.ThorpNine.SparseSaving.Thorp.centralPalindromePerm_step line 707
65. def OAI.ThorpNine.SparseSaving.Thorp.centralLevelCost line 726
66. def OAI.ThorpNine.SparseSaving.Thorp.centralSlabCost line 742
67. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_childLift line 746
68. def OAI.ThorpNine.SparseSaving.Thorp.centralDistance line 770
69. lemma OAI.ThorpNine.SparseSaving.Thorp.centralDistance_step line 773
70. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_centralBlock line 788
71. lemma OAI.ThorpNine.SparseSaving.Thorp.permDistance_centralPalindrome line 797
72. lemma OAI.ThorpNine.SparseSaving.Thorp.centralLevelCost_step line 804
73. lemma OAI.ThorpNine.SparseSaving.Thorp.centralLevelCost_perturb line 821
74. lemma OAI.ThorpNine.SparseSaving.Thorp.centralSlabCost_perturb line 851