OAI/Combinatorics/Progressions/Estimates/FiniteGradedBranchPrefixLog.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.prod_range_le_uniform_pow line 17
  2. theorem OAI.Erdos3.sum_graded_sizes_le line 25
  3. def OAI.Erdos3.finiteGradedBranchLevel line 47
  4. theorem OAI.Erdos3.finiteGradedBranchLevel_mem_zero line 53
  5. theorem OAI.Erdos3.finiteGradedBranchLevel_mem_succ line 58
  6. theorem OAI.Erdos3.finiteGradedBranchLevel_child_mem line 65
  7. theorem OAI.Erdos3.finiteGradedBranchLevel_card_le_product line 72
  8. theorem OAI.Erdos3.finiteGradedBranchLevel_all_valid line 99
  9. theorem OAI.Erdos3.finiteGradedBranchLevel_nonempty line 116
  10. theorem OAI.Erdos3.finiteGradedBranchLevel_exists_valid line 135
  11. theorem OAI.Erdos3.finiteGradedBranchLevel_card_le_pow line 154
  12. def OAI.Erdos3.finiteGradedBranchVertices line 164
  13. theorem OAI.Erdos3.finiteGradedBranchVertices_mem_iff line 169
  14. theorem OAI.Erdos3.finiteGradedBranchVertices_card_le line 178
  15. theorem OAI.Erdos3.finiteGradedBranchLevel_card_le_exp_sum line 201
  16. theorem OAI.Erdos3.finiteGradedBranchVertices_card_le_sum_exp_prefixes line 231
  17. theorem OAI.Erdos3.finiteGradedBranchVertices_card_le_mul_exp_sum line 250