OAI/Probability/ThorpRouting/HighTail/Main.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.HighTail.Thorp.palindrome_slab_adapted_mul_le line 10
2. def OAI.ThorpNine.HighTail.Thorp.familyEnd line 21
3. lemma OAI.ThorpNine.HighTail.Thorp.familyEnd_two line 23
4. lemma OAI.ThorpNine.HighTail.Thorp.familyEnd_ge line 28
5. def OAI.ThorpNine.HighTail.Thorp.palindromeFamilyCost line 36
6. lemma OAI.ThorpNine.HighTail.Thorp.palindromeFamilyCost_adapted line 40
7. theorem OAI.ThorpNine.HighTail.Thorp.palindrome_family_mgf line 48
8. lemma OAI.ThorpNine.HighTail.Thorp.pow_four_ge line 84
9. lemma OAI.ThorpNine.HighTail.Thorp.sum_family_decay line 89
10. lemma OAI.ThorpNine.HighTail.Thorp.palindromeLevelCost_step_add line 114
11. lemma OAI.ThorpNine.HighTail.Thorp.palindromeLowCost_sum line 132
12. lemma OAI.ThorpNine.HighTail.Thorp.palindromeLowCost_slab line 145
13. lemma OAI.ThorpNine.HighTail.Thorp.palindromeCost_family line 152
14. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_mul_sq_le line 167
15. lemma OAI.ThorpNine.HighTail.Thorp.finiteMean_mul_exp_le line 173
16. def OAI.ThorpNine.HighTail.Thorp.heightDecay line 191
17. lemma OAI.ThorpNine.HighTail.Thorp.heightDecay_nonneg line 194
18. lemma OAI.ThorpNine.HighTail.Thorp.heightDecay_antitone line 198
19. lemma OAI.ThorpNine.HighTail.Thorp.palindrome_family_mgf_decay line 209
20. theorem OAI.ThorpNine.HighTail.Thorp.palindrome_high_mgf line 220
21. lemma OAI.ThorpNine.HighTail.Thorp.palindrome_high_full_mgf line 237
22. theorem OAI.ThorpNine.HighTail.Thorp.palindrome_cost_mgf_cutoff line 249
23. lemma OAI.ThorpNine.HighTail.Thorp.cutoffMass_le line 275
24. lemma OAI.ThorpNine.HighTail.Thorp.palindromeLowCost_le line 286
25. theorem OAI.ThorpNine.HighTail.Thorp.palindrome_cost_mgf_coarse line 290
26. def OAI.ThorpNine.HighTail.Thorp.momentBase line 327
27. lemma OAI.ThorpNine.HighTail.Thorp.momentBase_one_le line 329
28. lemma OAI.ThorpNine.HighTail.Thorp.momentBase_log line 332
29. lemma OAI.ThorpNine.HighTail.Thorp.momentBase_pow line 338
30. lemma OAI.ThorpNine.HighTail.Thorp.palindromeRowMoment_le_cost line 342
31. theorem OAI.ThorpNine.HighTail.Thorp.palindrome_row_moment_coarse line 359
32. def OAI.ThorpNine.HighTail.Thorp.densityCutoff line 365
33. lemma OAI.ThorpNine.HighTail.Thorp.log_small_density line 367
34. lemma OAI.ThorpNine.HighTail.Thorp.densityCutoff_bounds line 375
35. lemma OAI.ThorpNine.HighTail.Thorp.densityCutoff_decay line 389
36. lemma OAI.ThorpNine.HighTail.Thorp.densityCutoff_power line 401
37. lemma OAI.ThorpNine.HighTail.Thorp.densityCutoff_sparse line 422
38. lemma OAI.ThorpNine.HighTail.Thorp.momentBase_log_exact line 437
39. lemma OAI.ThorpNine.HighTail.Thorp.densityCutoff_le_height line 441
40. def OAI.ThorpNine.HighTail.Thorp.densityTailConstant line 458
41. lemma OAI.ThorpNine.HighTail.Thorp.densityTailConstant_nonneg line 461
42. lemma OAI.ThorpNine.HighTail.Thorp.heightDecay_cutoff line 465
43. lemma OAI.ThorpNine.HighTail.Thorp.sparse_low_algebra line 474
44. lemma OAI.ThorpNine.HighTail.Thorp.palindrome_row_moment_small line 483
45. def OAI.ThorpNine.HighTail.Thorp.densityConstant line 520
46. lemma OAI.ThorpNine.HighTail.Thorp.densityConstant_pos line 523
47. theorem OAI.ThorpNine.HighTail.Thorp.palindrome_row_moment_bound line 529
48. lemma OAI.ThorpNine.HighTail.Thorp.palindromeRowMoment_nonneg line 564
49. theorem OAI.ThorpNine.HighTail.Thorp.palindrome_log_row_moment line 571
50. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.family_weighted line 588
51. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.low_switch_height line 636
52. def OAI.ThorpNine.HighTail.Thorp.HighHeight.lowCoins line 643
53. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.lowCoins_adapted line 647
54. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.lowCoins_assemble line 652
55. def OAI.ThorpNine.HighTail.Thorp.HighHeight.lowEvent line 657
56. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.lowEvent_nonneg line 660
57. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.lowEvent_adapted line 664
58. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.lowEvent_mean_mul line 668
59. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.lowEvent_mean line 678
60. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.family_partial line 682
61. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.highCost_family line 701
62. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.highCost_levels line 714
63. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.high_partial line 731
64. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.high_unconditional line 752
65. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.cost_small line 760
66. theorem OAI.ThorpNine.HighTail.Thorp.HighHeight.cost_bound_pos line 797
67. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.cost_bound line 832
68. def OAI.ThorpNine.HighTail.Thorp.HighHeight.tailConstant line 842
69. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.tailConstant_pos line 845
70. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.decay_bound line 849
71. def OAI.ThorpNine.HighTail.Thorp.HighHeight.constant line 868
72. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.constant_pos line 870
73. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.log_mgf_le line 873
74. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.high_log line 879
75. lemma OAI.ThorpNine.HighTail.Thorp.HighHeight.sparse_log line 897
76. theorem OAI.ThorpNine.HighTail.Thorp.HighHeight.high_tail line 910