OAI/Combinatorics/BalancedRyser/Local/LocalAsymptotics.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.LocalAsymptotics.summable_polynomial_mul_pow_div_factorial line 12
  2. theorem OAI.Balanced.LocalAsymptotics.tendsto_log_pow_div line 24
  3. theorem OAI.Balanced.LocalAsymptotics.tendsto_ceil_log_pow_div line 29
  4. theorem OAI.Balanced.LocalAsymptotics.tendsto_ceil_log_cube_div_nat line 45
  5. theorem OAI.Balanced.LocalAsymptotics.large_pencil_tail_le_inv line 50
  6. theorem OAI.Balanced.LocalAsymptotics.tendsto_large_pencil_tail line 80
  7. theorem OAI.Balanced.LocalAsymptotics.tendsto_large_pencil_tail_nat line 92
  8. theorem OAI.Balanced.LocalAsymptotics.sum_polynomial_mul_pow_div_factorial_le line 98
  9. theorem OAI.Balanced.LocalAsymptotics.tendsto_weighted_log_bound line 105
  10. theorem OAI.Balanced.LocalAsymptotics.tendsto_plane_weighted_pencil_sum line 120
  11. theorem OAI.Balanced.LocalAsymptotics.pencil_common_factor_le line 131