OAI/Probability/StrongRayleigh/DyadicTail.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336AdditiveD139.DyadicTail.measure_abs_gt_le_of_fourth_moment line 16
  2. theorem OAI.Problem336AdditiveD139.DyadicTail.measure_exists_abs_gt_le_of_fourth_moment line 37
  3. theorem OAI.Problem336AdditiveD139.DyadicTail.ae_eventually_forall_abs_le_of_summable_fourth_moments line 60
  4. theorem OAI.Problem336AdditiveD139.DyadicTail.dyadic_fourth_moment_cost line 75
  5. theorem OAI.Problem336AdditiveD139.DyadicTail.ae_eventually_dyadic_abs_le line 88
  6. theorem OAI.Problem336AdditiveD139.DyadicTail.ae_all_eventually_dyadic_abs_le line 103
  7. theorem OAI.Problem336AdditiveD139.DyadicTail.exists_geometric_bound_of_eventually line 113
  8. theorem OAI.Problem336AdditiveD139.DyadicTail.ae_exists_dyadic_geometric_bound line 140