OAI/Combinatorics/ParityLifts/Flowers.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Sparsification.singletons_pairwise line 10
2. lemma OAI.Sparsification.pairwise_degree_le_one line 17
3. lemma OAI.Sparsification.singleton_degree_le_one line 26
4. lemma OAI.Sparsification.erase_image_injective line 29
5. lemma OAI.Sparsification.flower_two_of_degree line 37
6. lemma OAI.Sparsification.no_two_flower_degree line 66
7. lemma OAI.Sparsification.rank_two_sunflower line 73

   Source documentation

   The rank-two sunflower bound, proved directly by a largest disjoint family.

   lemma rank_two_sunflower {F : CNF α} {h : ℕ} (hsize : ∀ C ∈ F, C.card = 2)
       (hcard : 2 * h ^ 2 < F.card) :
       Nonempty (Flower F 0 2 h) ∨ Nonempty (Flower F 1 1 h) := by
   …

   Mentions: OAI.Sparsification.CNF, OAI.Sparsification.Flower

8. lemma OAI.Sparsification.Flower.reattach line 160
9. def OAI.Sparsification.triples line 182
10. lemma OAI.Sparsification.no_three_flower_degree line 184
11. lemma OAI.Sparsification.width_three_count line 220
12. lemma OAI.Sparsification.sparse_leaf_density line 247