OAI/Probability/ThorpRouting/Smoothing/Main.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThorpNine.Smoothing.Thorp.palindrome_family_mgf line 10
  2. lemma OAI.ThorpNine.Smoothing.Thorp.pow_four_ge line 46
  3. lemma OAI.ThorpNine.Smoothing.Thorp.sum_family_decay line 51
  4. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeLevelCost_step_add line 76
  5. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeLowCost_sum line 94
  6. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeLowCost_slab line 107
  7. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeCost_family line 114
  8. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_mul_sq_le line 129
  9. lemma OAI.ThorpNine.Smoothing.Thorp.finiteMean_mul_exp_le line 135
  10. def OAI.ThorpNine.Smoothing.Thorp.heightDecay line 153
  11. lemma OAI.ThorpNine.Smoothing.Thorp.heightDecay_nonneg line 156
  12. lemma OAI.ThorpNine.Smoothing.Thorp.heightDecay_antitone line 160
  13. lemma OAI.ThorpNine.Smoothing.Thorp.palindrome_family_mgf_decay line 171
  14. theorem OAI.ThorpNine.Smoothing.Thorp.palindrome_high_mgf line 182
  15. lemma OAI.ThorpNine.Smoothing.Thorp.palindrome_high_full_mgf line 199
  16. theorem OAI.ThorpNine.Smoothing.Thorp.palindrome_cost_mgf_cutoff line 211
  17. lemma OAI.ThorpNine.Smoothing.Thorp.cutoffMass_le line 237
  18. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeLowCost_le line 248
  19. theorem OAI.ThorpNine.Smoothing.Thorp.palindrome_cost_mgf_coarse line 252
  20. def OAI.ThorpNine.Smoothing.Thorp.momentBase line 289
  21. lemma OAI.ThorpNine.Smoothing.Thorp.momentBase_one_le line 291
  22. lemma OAI.ThorpNine.Smoothing.Thorp.momentBase_log line 294
  23. lemma OAI.ThorpNine.Smoothing.Thorp.momentBase_pow line 300
  24. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeRowMoment_le_cost line 304
  25. theorem OAI.ThorpNine.Smoothing.Thorp.palindrome_row_moment_coarse line 321
  26. def OAI.ThorpNine.Smoothing.Thorp.densityCutoff line 327
  27. lemma OAI.ThorpNine.Smoothing.Thorp.log_small_density line 329
  28. lemma OAI.ThorpNine.Smoothing.Thorp.densityCutoff_bounds line 337
  29. lemma OAI.ThorpNine.Smoothing.Thorp.densityCutoff_decay line 351
  30. lemma OAI.ThorpNine.Smoothing.Thorp.densityCutoff_power line 363
  31. lemma OAI.ThorpNine.Smoothing.Thorp.densityCutoff_sparse line 384
  32. lemma OAI.ThorpNine.Smoothing.Thorp.momentBase_log_exact line 399
  33. lemma OAI.ThorpNine.Smoothing.Thorp.densityCutoff_le_height line 403
  34. def OAI.ThorpNine.Smoothing.Thorp.densityTailConstant line 420
  35. lemma OAI.ThorpNine.Smoothing.Thorp.densityTailConstant_nonneg line 423
  36. lemma OAI.ThorpNine.Smoothing.Thorp.heightDecay_cutoff line 427
  37. lemma OAI.ThorpNine.Smoothing.Thorp.sparse_low_algebra line 436
  38. lemma OAI.ThorpNine.Smoothing.Thorp.palindrome_row_moment_small line 445
  39. def OAI.ThorpNine.Smoothing.Thorp.densityConstant line 482
  40. lemma OAI.ThorpNine.Smoothing.Thorp.densityConstant_pos line 485
  41. theorem OAI.ThorpNine.Smoothing.Thorp.palindrome_row_moment_bound line 491
  42. lemma OAI.ThorpNine.Smoothing.Thorp.palindromeRowMoment_nonneg line 526
  43. theorem OAI.ThorpNine.Smoothing.Thorp.palindrome_log_row_moment line 533
  44. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.mean_nonneg line 553
  45. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.mean_rpow_concave line 556
  46. def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.act line 568
  47. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.act_nonneg line 571
  48. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.act_rpow_le line 576
  49. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.act_one_to_p line 584
  50. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.act_b_to_pb line 633
  51. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.kernel_pow_nonneg line 650
  52. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.kernel_pow_row line 661
  53. def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.rowDensity line 672
  54. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.rowDensity_nonneg line 676
  55. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.rowDensity_succ line 680
  56. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.rowDensity_mean line 687
  57. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.rowDensity_moment_iter line 692
  58. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.rowDensity_second_moment line 719
  59. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.symmetric_kernel_smoothing line 741
  60. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.density_exponent_numeric line 773
  61. def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.PermLaw.kernel line 785
  62. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.PermLaw.nonneg line 789
  63. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.PermLaw.row line 792
  64. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.PermLaw.inverse line 797
  65. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.PermLaw.col line 806
  66. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.PermLaw.mul line 811
  67. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.PermLaw.conjugate line 829
  68. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.mul_nonneg_entries line 847
  69. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.mul_row line 852
  70. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.mul_col line 859
  71. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.bound_mul_left line 866
  72. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.bound_mul_right line 875
  73. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.sandwich_power line 883
  74. def OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.tuplePerm line 897
  75. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.tuplePerm_apply line 904
  76. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.tuplePerm_mul line 908
  77. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.tuplePerm_inverse line 914
  78. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.tupleProbability_kernel line 920
  79. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.sweepKernel_law line 932
  80. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.reflectedKernel_conjugate line 937
  81. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.sweepKernel_nonneg line 960
  82. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.sweepKernel_row line 963
  83. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.sweepKernel_col line 968
  84. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.reflected_nonneg line 973
  85. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.reflected_row line 978
  86. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.reflected_col line 982
  87. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.reflected_symmetric line 986
  88. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.reflected_moment line 989
  89. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.tuples_card line 1005
  90. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.canonical_pointwise line 1008
  91. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.both_pointwise line 1021
  92. lemma OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.regular_trace_bound line 1038
  93. theorem OAI.ThorpNine.Smoothing.Thorp.StrongSmoothing.strong_smoothing line 1055