OAI/Combinatorics/CycleDecomposition/Sampling.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.Sampling.indicator_mem_Icc line 15
  2. lemma OAI.ErdosGallai.Sampling.mgf_indicator line 18
  3. lemma OAI.ErdosGallai.Sampling.mgf_indicator_sum_bound line 30
  4. lemma OAI.ErdosGallai.Sampling.exp_neg_half_bound line 53
  5. lemma OAI.ErdosGallai.Sampling.exp_half_bound line 61
  6. theorem OAI.ErdosGallai.Sampling.bernoulli_sum_lower_tail line 66
  7. theorem OAI.ErdosGallai.Sampling.bernoulli_sum_upper_tail line 89
  8. def OAI.ErdosGallai.Sampling.sampleMeasure line 117
  9. instance OAI.ErdosGallai.Sampling.sampleMeasure_probability line 120
  10. def OAI.ErdosGallai.Sampling.sampleVertices line 124
  11. def OAI.ErdosGallai.Sampling.sampleIndicator line 126
  12. lemma OAI.ErdosGallai.Sampling.sampleIndicator_measurable line 128
  13. lemma OAI.ErdosGallai.Sampling.sampleIndicator_values line 131
  14. lemma OAI.ErdosGallai.Sampling.sampleIndicator_indep line 135
  15. lemma OAI.ErdosGallai.Sampling.sampleIndicator_integral line 140
  16. lemma OAI.ErdosGallai.Sampling.sampleIndicator_sum line 147
  17. lemma OAI.ErdosGallai.Sampling.sample_card_lower_tail line 154
  18. lemma OAI.ErdosGallai.Sampling.sample_card_upper_tail line 161
  19. lemma OAI.ErdosGallai.Sampling.sample_miss_probability line 168
  20. lemma OAI.ErdosGallai.Sampling.sample_miss_bound line 196
  21. lemma OAI.ErdosGallai.Sampling.sample_contains_probability line 205
  22. lemma OAI.ErdosGallai.Sampling.sample_contains_real_probability line 229
  23. lemma OAI.ErdosGallai.Sampling.sample_blocks_independent line 234
  24. def OAI.ErdosGallai.Sampling.blockIndicator line 250
  25. lemma OAI.ErdosGallai.Sampling.blockIndicator_values line 253
  26. lemma OAI.ErdosGallai.Sampling.blockIndicator_integral line 258
  27. lemma OAI.ErdosGallai.Sampling.sample_blocks_lower_tail line 264
  28. lemma OAI.ErdosGallai.Sampling.sample_weight_sum line 276
  29. lemma OAI.ErdosGallai.Sampling.sample_weight_integral line 284
  30. lemma OAI.ErdosGallai.Sampling.nonnegative_markov_quarter line 292
  31. lemma OAI.ErdosGallai.Sampling.sample_weight_markov line 301
  32. theorem OAI.ErdosGallai.Sampling.exists_small_weighted_hitting_set line 312
  33. lemma OAI.ErdosGallai.Sampling.exists_avoiding_finite_events line 369