OAI/Combinatorics/ListHadwiger/SamplingBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.Sampling.remainder line 10
  2. lemma OAI.LinearListHadwiger.Sampling.mem_remainder line 14
  3. lemma OAI.LinearListHadwiger.Sampling.probability_not line 26
  4. lemma OAI.LinearListHadwiger.Sampling.remainder_survival_eq line 37
  5. lemma OAI.LinearListHadwiger.Sampling.remainder_survival_power line 74
  6. theorem OAI.LinearListHadwiger.Sampling.remainder_survival_bound line 85
  7. lemma OAI.LinearListHadwiger.Sampling.remainder_sdiff_subset line 114
  8. lemma OAI.LinearListHadwiger.Sampling.inter_sdiff_subset_left line 129
  9. lemma OAI.LinearListHadwiger.Sampling.inter_remainder_difference_bound line 135
  10. lemma OAI.LinearListHadwiger.Sampling.card_abs_sub_le_differences line 147
  11. lemma OAI.LinearListHadwiger.Sampling.remainder_card_bounded_changes line 158
  12. lemma OAI.LinearListHadwiger.Sampling.remainder_fractional_bounded_changes line 164
  13. theorem OAI.LinearListHadwiger.Sampling.remainder_fractional_concentration line 173
  14. theorem OAI.LinearListHadwiger.Sampling.bounded_differences_general line 192
  15. def OAI.LinearListHadwiger.Sampling.unionRemainders line 237
  16. lemma OAI.LinearListHadwiger.Sampling.unionRemainders_sdiff_subset line 241
  17. lemma OAI.LinearListHadwiger.Sampling.unionRemainders_card_bounded_changes line 265
  18. theorem OAI.LinearListHadwiger.Sampling.unionRemainders_concentration line 277