OAI/Combinatorics/CycleDecomposition/EdgeSplitting.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.Splitting.indicator_mem_Icc line 19
  2. lemma OAI.ErdosGallai.Splitting.mgf_indicator line 22
  3. lemma OAI.ErdosGallai.Splitting.mgf_indicator_sum_bound line 34
  4. lemma OAI.ErdosGallai.Splitting.exp_neg_half_bound line 57
  5. lemma OAI.ErdosGallai.Splitting.exp_half_bound line 65
  6. theorem OAI.ErdosGallai.Splitting.bernoulli_sum_lower_tail line 70
  7. theorem OAI.ErdosGallai.Splitting.bernoulli_sum_upper_tail line 93
  8. def OAI.ErdosGallai.Splitting.CutExpansion line 121
  9. lemma OAI.ErdosGallai.Splitting.boundary_sym2_injective line 125
  10. def OAI.ErdosGallai.Splitting.edgeColorMeasure line 136
  11. instance OAI.ErdosGallai.Splitting.edgeColorMeasure_probability line 140
  12. def OAI.ErdosGallai.Splitting.colorIndicator line 145
  13. lemma OAI.ErdosGallai.Splitting.colorIndicator_indep line 148
  14. lemma OAI.ErdosGallai.Splitting.colorIndicator_integral line 153
  15. def OAI.ErdosGallai.Splitting.colorGraph line 162
  16. instance OAI.ErdosGallai.Splitting.colorGraph_decidable line 168
  17. lemma OAI.ErdosGallai.Splitting.colorGraph_interedges line 172
  18. lemma OAI.ErdosGallai.Splitting.color_cut_sum line 181
  19. lemma OAI.ErdosGallai.Splitting.color_cut_lower_tail line 188
  20. lemma OAI.ErdosGallai.Splitting.cutExpansion_of_small_cuts line 225
  21. lemma OAI.ErdosGallai.Splitting.sum_nonempty_subsets_power line 243
  22. theorem OAI.ErdosGallai.Splitting.edge_splitting_failure_bound line 253
  23. theorem OAI.ErdosGallai.Splitting.edge_splitting_of_error_lt_one line 312
  24. lemma OAI.ErdosGallai.Splitting.tendsto_monomial_exp_neg_power line 344
  25. def OAI.ErdosGallai.Splitting.edgeSplittingScaleError line 353
  26. lemma OAI.ErdosGallai.Splitting.edgeSplittingScaleError_tendsto line 356
  27. theorem OAI.ErdosGallai.Splitting.edge_splitting_uniform line 367