OAI/Combinatorics/Ryser/Incidence/PopularOverlap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Incidence.sum_membership_indicator line 16
2. theorem OAI.RyserCoveringCounterexample.Incidence.sum_overlap_multiplicity line 26
3. theorem OAI.RyserCoveringCounterexample.Incidence.sum_sq_overlap_multiplicity line 36
4. theorem OAI.RyserCoveringCounterexample.Incidence.overlap_energy_lower line 75
5. theorem OAI.RyserCoveringCounterexample.Incidence.popular_card_lower line 96
6. theorem OAI.RyserCoveringCounterexample.Incidence.exists_popular_intersections line 120