OAI/Combinatorics/Progressions/Estimates/UniformFamilyMemberNet.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_uniform_family_member_net line 12
  2. theorem OAI.Erdos3.exists_uniform_family_member_net_half line 34
  3. theorem OAI.Erdos3.exists_uniform_family_member_net_with_bounds line 41
  4. theorem OAI.Erdos3.exists_finite_uniform_family_member_net line 56
  5. theorem OAI.Erdos3.exists_uniform_family_member_nets_exp_log line 66
  6. theorem OAI.Erdos3.uniformFamilyMemberNet_half_log_budget line 89
  7. theorem OAI.Erdos3.exists_uniform_family_member_net_of_polynomial_log line 109
  8. theorem OAI.Erdos3.exists_uniform_family_member_nets_polynomial_log line 123