OAI/Combinatorics/ListHadwiger/Concentration.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.FiniteConcentration.mean line 8
  2. lemma OAI.LinearListHadwiger.FiniteConcentration.mean_const line 10
  3. lemma OAI.LinearListHadwiger.FiniteConcentration.mean_sub line 13
  4. lemma OAI.LinearListHadwiger.FiniteConcentration.mean_mono line 17
  5. lemma OAI.LinearListHadwiger.FiniteConcentration.mean_sub_const line 21
  6. lemma OAI.LinearListHadwiger.FiniteConcentration.mean_const_sub line 26
  7. lemma OAI.LinearListHadwiger.FiniteConcentration.centered_bound line 31
  8. lemma OAI.LinearListHadwiger.FiniteConcentration.centered_mgf line 41
  9. def OAI.LinearListHadwiger.FiniteConcentration.mass line 94
  10. lemma OAI.LinearListHadwiger.FiniteConcentration.mass_nonneg line 97
  11. lemma OAI.LinearListHadwiger.FiniteConcentration.mass_sum line 101
  12. lemma OAI.LinearListHadwiger.FiniteConcentration.sum_cons line 107
  13. lemma OAI.LinearListHadwiger.FiniteConcentration.mass_cons line 113
  14. lemma OAI.LinearListHadwiger.FiniteConcentration.mean_cons line 118
  15. def OAI.LinearListHadwiger.FiniteConcentration.BoundedChanges line 124
  16. lemma OAI.LinearListHadwiger.FiniteConcentration.BoundedChanges.tail line 127
  17. lemma OAI.LinearListHadwiger.FiniteConcentration.BoundedChanges.head_mean line 140
  18. theorem OAI.LinearListHadwiger.FiniteConcentration.bounded_changes_mgf line 160
  19. def OAI.LinearListHadwiger.FiniteConcentration.probability line 216
  20. lemma OAI.LinearListHadwiger.FiniteConcentration.exponential_markov line 220
  21. lemma OAI.LinearListHadwiger.FiniteConcentration.probability_abs_le line 234
  22. theorem OAI.LinearListHadwiger.FiniteConcentration.bounded_changes_upper line 253
  23. lemma OAI.LinearListHadwiger.FiniteConcentration.BoundedChanges.neg line 276
  24. theorem OAI.LinearListHadwiger.FiniteConcentration.bounded_differences line 281