OAI/Combinatorics/BalancedRyser/Probability/LogTail.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BalancedRyser.polynomial_mul_ratio_pow_le_inv line 12
  2. theorem OAI.BalancedRyser.tendsto_log_cutoff_atTop line 43
  3. theorem OAI.BalancedRyser.tendsto_polynomial_mul_cutoff_tail line 48
  4. theorem OAI.BalancedRyser.tendsto_polynomial_mul_log_cutoff_tail line 69
  5. theorem OAI.BalancedRyser.tendsto_large_pencil_union_bound line 78
  6. theorem OAI.BalancedRyser.choose_le_exp_mul_div_pow line 85
  7. theorem OAI.BalancedRyser.slot_choose_mul_pow_le line 102
  8. theorem OAI.BalancedRyser.tendsto_polynomial_mul_slot_choose_tail line 127
  9. theorem OAI.BalancedRyser.choose_le_pow_mul_exp_div line 142
  10. theorem OAI.BalancedRyser.affine_line_subset_count_le line 155
  11. theorem OAI.BalancedRyser.eventually_log_le_power_cutoff line 166
  12. theorem OAI.BalancedRyser.tendsto_polynomial_mul_power_cutoff_tail line 180