OAI/Probability/StrongRayleigh/LimsupDrift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336AdditiveD139.limsup_le_limsup_add_of_unit_bounds line 14
  2. theorem OAI.Problem336AdditiveD139.abs_limsup_sub_limsup_le_of_unit_bounds line 31
  3. def OAI.Problem336AdditiveD139.limsupDrift line 47
  4. theorem OAI.Problem336AdditiveD139.limsupDrift_mem_unitInterval line 50
  5. theorem OAI.Problem336AdditiveD139.measurable_limsupDrift line 65
  6. theorem OAI.Problem336AdditiveD139.limsupDrift_abs_sub_le line 72
  7. theorem OAI.Problem336AdditiveD139.limsupDrift_reindex line 79
  8. theorem OAI.Problem336AdditiveD139.limsupDrift_leftTranslate line 88