OAI/Combinatorics/BalancedRyser/Incidence/LocalLargePencils.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Balanced.Local.sum_event_union_le line 15
2. lemma OAI.Balanced.Local.sum_event_mono_of_pos line 34
3. lemma OAI.Balanced.Local.sum_event_at_least_le line 50
4. lemma OAI.Balanced.Local.retained_choice_eq_of_onLine line 77
5. theorem OAI.Balanced.Local.fixed_offset_incident_cylinder_le line 91
6. lemma OAI.Balanced.Local.card_slot line 125
7. lemma OAI.Balanced.Local.splitMultiplicity_le_incident_slots line 129
8. theorem OAI.Balanced.Local.fixed_offset_large_pencil_le line 137
9. theorem OAI.Balanced.Local.fixed_offset_some_large_pencil_le line 158
10. lemma OAI.Balanced.Local.selectedProbability_eq_sum line 181
11. lemma OAI.Balanced.Local.selectedProbability_nonneg line 196
12. theorem OAI.Balanced.Local.selected_some_large_pencil_le line 207
13. theorem OAI.Balanced.Local.large_pencil_uniform_error line 227