OAI/Combinatorics/CycleDecomposition/BatchPreparation.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ErdosGallai.Batch.crossGraph_card line 20
  2. def OAI.ErdosGallai.Batch.edgePairEvent line 49
  3. lemma OAI.ErdosGallai.Batch.edgePairEvent_pair line 52
  4. def OAI.ErdosGallai.Batch.DisjointEdgePair line 60
  5. def OAI.ErdosGallai.Batch.pairErrors line 64
  6. def OAI.ErdosGallai.Batch.loopErrors line 67
  7. lemma OAI.ErdosGallai.Batch.loopErrors_average line 71
  8. lemma OAI.ErdosGallai.Batch.internal_pairErrors_average line 106
  9. lemma OAI.ErdosGallai.Batch.cross_pair_orientation line 136
  10. lemma OAI.ErdosGallai.Batch.cross_pairErrors_average line 157
  11. lemma OAI.ErdosGallai.Batch.mem_pairErrors line 195
  12. lemma OAI.ErdosGallai.Batch.mem_crossGraph line 202
  13. lemma OAI.ErdosGallai.Batch.two_paired_edges_placement line 208
  14. def OAI.ErdosGallai.Batch.wedgeCover line 228
  15. def OAI.ErdosGallai.Batch.internalCover line 232
  16. def OAI.ErdosGallai.Batch.crossCover line 235
  17. lemma OAI.ErdosGallai.Batch.all_collisions_covered line 239
  18. lemma OAI.ErdosGallai.Batch.all_loops_covered line 288
  19. def OAI.ErdosGallai.Batch.foldErrorBudget line 300
  20. lemma OAI.ErdosGallai.Batch.quotientDefect_le_budget line 306
  21. lemma OAI.ErdosGallai.Batch.fold_ratio_one line 342
  22. lemma OAI.ErdosGallai.Batch.fold_ratio_three line 345
  23. lemma OAI.ErdosGallai.Batch.choose_two_real_bound line 348
  24. lemma OAI.ErdosGallai.Batch.first_error_numeric line 353
  25. lemma OAI.ErdosGallai.Batch.internal_error_numeric line 363
  26. lemma OAI.ErdosGallai.Batch.cross_error_numeric line 382
  27. lemma OAI.ErdosGallai.Batch.first_errors_average line 397
  28. lemma OAI.ErdosGallai.Batch.internal_errors_average line 422
  29. lemma OAI.ErdosGallai.Batch.cross_errors_average line 429
  30. theorem OAI.ErdosGallai.Batch.folding_average_bound line 463
  31. theorem OAI.ErdosGallai.Batch.pair_folding line 484
  32. def OAI.ErdosGallai.Batch.heavyNeighbors line 515
  33. lemma OAI.ErdosGallai.Batch.mem_heavyNeighbors line 518
  34. lemma OAI.ErdosGallai.Batch.heavyNeighbors_disjoint_active line 521
  35. lemma OAI.ErdosGallai.Batch.heavyNeighbors_card_le line 531
  36. def OAI.ErdosGallai.Batch.heavyDesignated line 552
  37. lemma OAI.ErdosGallai.Batch.heavyDesignated_le line 555
  38. theorem OAI.ErdosGallai.Batch.heavyDesignated_pairwise line 558
  39. def OAI.ErdosGallai.Batch.trimHeavyGraph line 580
  40. lemma OAI.ErdosGallai.Batch.trimHeavyGraph_le line 585
  41. theorem OAI.ErdosGallai.Batch.trimHeavyGraph_neighbors line 587
  42. theorem OAI.ErdosGallai.Batch.trimHeavyGraph_degree line 604
  43. theorem OAI.ErdosGallai.Batch.trimHeavyGraph_ledger line 609
  44. structure OAI.ErdosGallai.Batch.TrimmedPath line 644
  45. lemma OAI.ErdosGallai.Batch.alternating_endpoint_mem line 650
  46. lemma OAI.ErdosGallai.Batch.alternating_snd_mem line 659
  47. lemma OAI.ErdosGallai.Batch.alternating_penultimate_mem line 668
  48. theorem OAI.ErdosGallai.Batch.trim_bipartite_path line 678
  49. lemma OAI.ErdosGallai.Batch.bipartite_path_length line 719
  50. lemma OAI.ErdosGallai.Batch.path_edgeFinset_card line 730
  51. theorem OAI.ErdosGallai.Batch.trim_bipartite_path_ledger line 735
  52. theorem OAI.ErdosGallai.Batch.close_trimmed_path line 770
  53. lemma OAI.ErdosGallai.Batch.endpoint_path_count_on line 798
  54. lemma OAI.ErdosGallai.Batch.heavy_paths line 829
  55. lemma OAI.ErdosGallai.Batch.folded_order_saving line 852
  56. structure OAI.ErdosGallai.Batch.PreparedBatch line 871
  57. lemma OAI.ErdosGallai.Batch.PreparedBatch.bad_subset line 898
  58. lemma OAI.ErdosGallai.Batch.PreparedBatch.retained_subset line 903
  59. theorem OAI.ErdosGallai.Batch.prepare_batch line 908