OAI/Combinatorics/BalancedRyser/Probability/SimultaneousDrift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.simultaneous_bounded_drift line 14
  2. def OAI.Balanced.predictableDriftSum line 43
  3. theorem OAI.Balanced.upper_tail_of_drift_le line 57
  4. theorem OAI.Balanced.lower_tail_of_le_drift line 72
  5. theorem OAI.Balanced.abs_tail_of_abs_drift_le line 87
  6. theorem OAI.Balanced.selection_azuma_exponent line 106
  7. theorem OAI.Balanced.tendsto_nat_pow_mul_exp_neg_rpow line 125
  8. theorem OAI.Balanced.tendsto_selection_simultaneous_error line 137