OAI/Combinatorics/BalancedRyser/Probability/RescaledDrift.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.condExp_div_const_ae line 17
  2. theorem OAI.Balanced.conditional_rescaled_increment_eq line 26
  3. theorem OAI.Balanced.abs_conditional_rescaled_increment_le line 41
  4. theorem OAI.Balanced.conditional_rescaled_increment_le line 51
  5. theorem OAI.Balanced.le_conditional_rescaled_increment line 61
  6. theorem OAI.Balanced.conditional_rescaled_increment_eq_zero line 71
  7. theorem OAI.Balanced.rescaled_increment_identity line 81
  8. theorem OAI.Balanced.abs_rescaled_increment_le line 86
  9. theorem OAI.Balanced.ae_abs_rescaled_increment_le line 107