OAI/Combinatorics/ListHadwiger/Eligibility.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LinearListHadwiger.Sampling.parameter_range_cutoff line 8
  2. lemma OAI.LinearListHadwiger.Sampling.floor_parameter line 39
  3. lemma OAI.LinearListHadwiger.Sampling.sample_size_parameters line 60
  4. lemma OAI.LinearListHadwiger.Sampling.trial_count_parameters line 108
  5. theorem OAI.LinearListHadwiger.Sampling.concentration_numeric_cutoff line 132
  6. theorem OAI.LinearListHadwiger.Sampling.uniform_bounded_differences line 196
  7. theorem OAI.LinearListHadwiger.Sampling.source_uniform_concentration line 228
  8. lemma OAI.LinearListHadwiger.Sampling.attachment_size_parameters line 271
  9. lemma OAI.LinearListHadwiger.Sampling.attachment_budget line 297
  10. theorem OAI.LinearListHadwiger.Sampling.complement_failure line 330