OAI/Combinatorics/CycleDecomposition/BatchIndexing.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ErdosGallai.Indexing.batchWeight line 20
  2. lemma OAI.ErdosGallai.Indexing.batchWeight_nonneg line 22
  3. lemma OAI.ErdosGallai.Indexing.indexed_batch_construction line 25
  4. lemma OAI.ErdosGallai.Indexing.batch_tail_mass line 123
  5. theorem OAI.ErdosGallai.Indexing.indexed_batch_partition line 134
  6. theorem OAI.ErdosGallai.Indexing.cover_card_le line 166
  7. theorem OAI.ErdosGallai.Indexing.disjoint_piece_inter line 172
  8. theorem OAI.ErdosGallai.Indexing.active_occurrences line 181
  9. theorem OAI.ErdosGallai.Indexing.skipped_occurrences_bound line 258
  10. lemma OAI.ErdosGallai.Indexing.list_pairwise_get line 281
  11. lemma OAI.ErdosGallai.Indexing.list_sum_get line 288
  12. structure OAI.ErdosGallai.Indexing.GraphBatches line 295
  13. theorem OAI.ErdosGallai.Indexing.materialize_batches line 311
  14. def OAI.ErdosGallai.Indexing.goodVertices line 397
  15. lemma OAI.ErdosGallai.Indexing.bad_vertices_degree_bound line 400
  16. structure OAI.ErdosGallai.Indexing.ActiveFamily line 413
  17. theorem OAI.ErdosGallai.Indexing.choose_active_family line 430
  18. lemma OAI.ErdosGallai.Indexing.thirds_le_halves line 486