OAI/Combinatorics/CycleDecomposition/CollisionEstimates.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.Batch.neighborsIn line 19
  2. def OAI.ErdosGallai.Batch.internalGraph line 22
  3. lemma OAI.ErdosGallai.Batch.neighborsIn_le_degree line 27
  4. lemma OAI.ErdosGallai.Batch.neighborsIn_eq_sum line 35
  5. lemma OAI.ErdosGallai.Batch.sum_incidence_to_set line 40
  6. lemma OAI.ErdosGallai.Batch.internalGraph_degree line 54
  7. lemma OAI.ErdosGallai.Batch.internalGraph_degree_sum line 72
  8. lemma OAI.ErdosGallai.Batch.internal_edge_bound line 79
  9. lemma OAI.ErdosGallai.Batch.incidence_bound line 90
  10. lemma OAI.ErdosGallai.Batch.wedge_count_bound line 98
  11. def OAI.ErdosGallai.Batch.betweenCount line 121
  12. lemma OAI.ErdosGallai.Batch.betweenCount_comm line 123
  13. lemma OAI.ErdosGallai.Batch.betweenCount_bound line 134
  14. lemma OAI.ErdosGallai.Batch.disjoint_neighbor_sum_le line 144
  15. lemma OAI.ErdosGallai.Batch.betweenCount_row_bound line 159
  16. lemma OAI.ErdosGallai.Batch.cross_error_row line 175
  17. def OAI.ErdosGallai.Batch.CollisionPairs line 205
  18. lemma OAI.ErdosGallai.Batch.mem_collisionPairs line 209
  19. lemma OAI.ErdosGallai.Batch.collisionPairs_mono line 214
  20. lemma OAI.ErdosGallai.Batch.pair_mem_collisionPairs line 221
  21. theorem OAI.ErdosGallai.Batch.prune_collisions line 232
  22. theorem OAI.ErdosGallai.Batch.prune_bad_images line 268
  23. def OAI.ErdosGallai.Batch.quotientDefect line 289
  24. theorem OAI.ErdosGallai.Batch.simple_quotient_representatives line 295
  25. lemma OAI.ErdosGallai.Batch.familyPaired_symm line 334
  26. lemma OAI.ErdosGallai.Batch.familyPaired_local line 339
  27. lemma OAI.ErdosGallai.Batch.familyPaired_same_set line 351
  28. def OAI.ErdosGallai.Batch.vertexPairEvent line 359
  29. lemma OAI.ErdosGallai.Batch.vertexPairEvent_pair line 362
  30. lemma OAI.ErdosGallai.Batch.finiteAverage_filter_card line 375
  31. lemma OAI.ErdosGallai.Batch.vertexPairEvent_average line 387
  32. def OAI.ErdosGallai.Batch.wedgeErrors line 404
  33. lemma OAI.ErdosGallai.Batch.wedgeErrors_average line 408
  34. lemma OAI.ErdosGallai.Batch.mem_internalGraph line 425
  35. def OAI.ErdosGallai.Batch.crossGraph line 430
  36. lemma OAI.ErdosGallai.Batch.distinct_edge_cases line 436
  37. lemma OAI.ErdosGallai.Batch.internal_collision_average line 470
  38. lemma OAI.ErdosGallai.Batch.cross_collision_average line 504