OAI/Probability/ThorpRouting/Tail/HeightDecay.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

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