OAI/Combinatorics/ListHadwiger/Thinning.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LinearListHadwiger.Sampling.complement_numeric_cutoff line 8
  2. theorem OAI.LinearListHadwiger.Sampling.source_complement line 118
  3. lemma OAI.LinearListHadwiger.Sampling.source_B_choice line 162
  4. lemma OAI.LinearListHadwiger.Sampling.survival_log_bound line 166
  5. theorem OAI.LinearListHadwiger.Sampling.source_sparseness line 189
  6. theorem OAI.LinearListHadwiger.Sampling.polynomial_tail_cutoff line 254
  7. lemma OAI.LinearListHadwiger.Sampling.decomposition_tail_cutoff line 272
  8. lemma OAI.LinearListHadwiger.Sampling.private_tail_cutoff line 288
  9. lemma OAI.LinearListHadwiger.Sampling.source_q_pos line 313
  10. theorem OAI.LinearListHadwiger.Sampling.source_fixed_region line 320