OAI/Combinatorics/CycleDecomposition/SamplingCuts.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.Sampling.cutColor line 13
  2. lemma OAI.ErdosGallai.Sampling.cutColor_lt line 16
  3. lemma OAI.ErdosGallai.Sampling.same_cutColor_blocks_disjoint line 22
  4. lemma OAI.ErdosGallai.Sampling.blockIndicator_sum_card line 44
  5. lemma OAI.ErdosGallai.Sampling.sampled_matching_lower_tail line 52
  6. lemma OAI.ErdosGallai.Sampling.sum_cutColor_class_card line 77
  7. theorem OAI.ErdosGallai.Sampling.sampled_bipartite_cut_lower_tail line 86
  8. def OAI.ErdosGallai.Sampling.neighborsIn line 191
  9. lemma OAI.ErdosGallai.Sampling.card_interedges_eq_sum_neighborsIn line 194
  10. lemma OAI.ErdosGallai.Sampling.neighborsIn_partition_card line 199
  11. lemma OAI.ErdosGallai.Sampling.interedges_sym2_injective line 217
  12. lemma OAI.ErdosGallai.Sampling.cut_perturbation_card line 226
  13. lemma OAI.ErdosGallai.Sampling.card_le_add_symmDiff line 263
  14. lemma OAI.ErdosGallai.Sampling.sdiff_card_le_add_symmDiff line 271
  15. lemma OAI.ErdosGallai.Sampling.cut_card_lower_of_neighbors line 281
  16. lemma OAI.ErdosGallai.Sampling.bad_sampled_cut_size_and_exceptional line 292
  17. def OAI.ErdosGallai.Sampling.neighborhoodUnion line 329
  18. lemma OAI.ErdosGallai.Sampling.neighborhoodUnion_leakage line 332
  19. lemma OAI.ErdosGallai.Sampling.hitting_neighborhoodUnion line 345
  20. theorem OAI.ErdosGallai.Sampling.exists_approximating_witness line 354
  21. def OAI.ErdosGallai.Sampling.CutExpansion line 411
  22. def OAI.ErdosGallai.Sampling.CutExpansionOn line 415
  23. theorem OAI.ErdosGallai.Sampling.cutExpansionOn_of_witnesses line 419
  24. lemma OAI.ErdosGallai.Sampling.cutExpansion_minDegree line 505
  25. lemma OAI.ErdosGallai.Sampling.sample_neighbors_lower_tail line 523
  26. lemma OAI.ErdosGallai.Sampling.card_small_subsets_le line 545
  27. def OAI.ErdosGallai.Sampling.witnessFamily line 567
  28. lemma OAI.ErdosGallai.Sampling.card_witnessFamily_le line 570
  29. lemma OAI.ErdosGallai.Sampling.sampled_witness_cut_lower_tail line 575
  30. def OAI.ErdosGallai.Sampling.SampleGood line 608
  31. theorem OAI.ErdosGallai.Sampling.vertex_sampling_failure_bound line 613