OAI/Combinatorics/ListHadwiger/PaletteSampling.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LinearListHadwiger.Sampling.complement_failure_thousand line 9
  2. def OAI.LinearListHadwiger.Sampling.coin line 82
  3. lemma OAI.LinearListHadwiger.Sampling.coin_nonneg line 84
  4. lemma OAI.LinearListHadwiger.Sampling.coin_sum line 87
  5. def OAI.LinearListHadwiger.Sampling.chosen line 90
  6. lemma OAI.LinearListHadwiger.Sampling.chosen_marginal line 92
  7. lemma OAI.LinearListHadwiger.Sampling.chosen_mean line 101
  8. lemma OAI.LinearListHadwiger.Sampling.chosen_bounded_change line 107
  9. lemma OAI.LinearListHadwiger.Sampling.chosen_concentration line 127
  10. theorem OAI.LinearListHadwiger.Sampling.exists_sparse_split line 138
  11. lemma OAI.LinearListHadwiger.Sampling.sparse_split_numeric_cutoff line 218
  12. theorem OAI.LinearListHadwiger.Sampling.sparse_split_cutoff line 264
  13. theorem OAI.LinearListHadwiger.Sampling.sparse_split_on_cutoff line 293