OAI/Combinatorics/CycleDecomposition/CoupledResolution.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.Batch.Splitting.indicator_mem_Icc line 19
  2. lemma OAI.ErdosGallai.Batch.Splitting.mgf_indicator line 22
  3. lemma OAI.ErdosGallai.Batch.Splitting.mgf_indicator_sum_bound line 34
  4. lemma OAI.ErdosGallai.Batch.Splitting.exp_neg_half_bound line 57
  5. lemma OAI.ErdosGallai.Batch.Splitting.exp_half_bound line 65
  6. theorem OAI.ErdosGallai.Batch.Splitting.bernoulli_sum_lower_tail line 70
  7. theorem OAI.ErdosGallai.Batch.Splitting.bernoulli_sum_upper_tail line 93
  8. def OAI.ErdosGallai.Batch.Splitting.CutExpansion line 121
  9. lemma OAI.ErdosGallai.Batch.Splitting.boundary_sym2_injective line 125
  10. def OAI.ErdosGallai.Batch.Splitting.edgeColorMeasure line 136
  11. instance OAI.ErdosGallai.Batch.Splitting.edgeColorMeasure_probability line 140
  12. def OAI.ErdosGallai.Batch.Splitting.colorIndicator line 145
  13. lemma OAI.ErdosGallai.Batch.Splitting.colorIndicator_indep line 148
  14. lemma OAI.ErdosGallai.Batch.Splitting.colorIndicator_integral line 153
  15. def OAI.ErdosGallai.Batch.Splitting.colorGraph line 162
  16. instance OAI.ErdosGallai.Batch.Splitting.colorGraph_decidable line 168
  17. lemma OAI.ErdosGallai.Batch.Splitting.colorGraph_interedges line 172
  18. lemma OAI.ErdosGallai.Batch.Splitting.color_cut_sum line 181
  19. lemma OAI.ErdosGallai.Batch.Splitting.color_cut_lower_tail line 188
  20. lemma OAI.ErdosGallai.Batch.Splitting.cutExpansion_of_small_cuts line 225
  21. lemma OAI.ErdosGallai.Batch.Splitting.sum_nonempty_subsets_power line 243
  22. theorem OAI.ErdosGallai.Batch.Splitting.edge_splitting_failure_bound line 253
  23. theorem OAI.ErdosGallai.Batch.Splitting.edge_splitting_of_error_lt_one line 312
  24. lemma OAI.ErdosGallai.Batch.Splitting.tendsto_monomial_exp_neg_power line 344
  25. def OAI.ErdosGallai.Batch.Splitting.edgeSplittingScaleError line 353
  26. lemma OAI.ErdosGallai.Batch.Splitting.edgeSplittingScaleError_tendsto line 356
  27. theorem OAI.ErdosGallai.Batch.Splitting.edge_splitting_uniform line 367
  28. def OAI.ErdosGallai.Batch.inductionPhi line 403
  29. lemma OAI.ErdosGallai.Batch.inductionPhi_one line 406
  30. lemma OAI.ErdosGallai.Batch.inductionPhi_bounds line 408
  31. lemma OAI.ErdosGallai.Batch.inductionPhi_monotone line 414
  32. lemma OAI.ErdosGallai.Batch.inductionPhi_nonconstant line 427
  33. def OAI.ErdosGallai.Batch.inductionDelta line 437
  34. lemma OAI.ErdosGallai.Batch.inductionDelta_pos line 439
  35. theorem OAI.ErdosGallai.Batch.induction_potential_gain line 447
  36. lemma OAI.ErdosGallai.Batch.induction_cutoff_absorption line 468
  37. theorem OAI.ErdosGallai.Batch.induction_cost_absorbed line 483
  38. lemma OAI.ErdosGallai.Batch.cutExpansionOn_of_induce line 521
  39. lemma OAI.ErdosGallai.Batch.cutExpansionOn_mono line 539
  40. theorem OAI.ErdosGallai.Batch.uniform_two_routers_on line 547
  41. lemma OAI.ErdosGallai.Batch.decompositionCost_adjoin_same line 604
  42. lemma OAI.ErdosGallai.Batch.decompositionCost_assemble_same line 622
  43. def OAI.ErdosGallai.Batch.routerRemainder line 638
  44. lemma OAI.ErdosGallai.Batch.routerRemainder_edges line 641
  45. lemma OAI.ErdosGallai.Batch.routerRemainder_le line 645
  46. lemma OAI.ErdosGallai.Batch.protected_le_remainder line 648
  47. lemma OAI.ErdosGallai.Batch.protected_avoids_used line 654
  48. lemma OAI.ErdosGallai.Batch.batch_remainder_ledger line 669
  49. lemma OAI.ErdosGallai.Batch.prepared_quotient_cost line 708
  50. theorem OAI.ErdosGallai.Batch.uniform_coupled_resolution_cost line 738