OAI/Combinatorics/BalancedRyser/Local/LocalPrescriptionCounting.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.Local.prescriptionSlots line 16
2. def OAI.Balanced.Local.PencilPrescriptionOccurs line 19
3. abbrev OAI.Balanced.Local.PencilPrescriptions line 25
4. def OAI.Balanced.Local.prescriptionOccurs line 28
5. def OAI.Balanced.Local.prescriptionRead line 32
6. theorem OAI.Balanced.Local.orderedBadPencil_has_representative line 36
7. theorem OAI.Balanced.Local.selectedProbability_le_encodedOrder_sum line 64
8. theorem OAI.Balanced.Local.bad_pencil_probability_le_canonical_sum line 83
9. theorem OAI.Balanced.Local.pencilPrescription_probability_le line 103
10. theorem OAI.Balanced.Local.bad_pencil_probability_le_canonical_offset_sum line 140
11. theorem OAI.Balanced.Local.exists_canonical_offset_bound line 160
12. theorem OAI.Balanced.Local.canonical_offset_sum_eq line 174
13. theorem OAI.Balanced.Local.bad_pencil_probability_le_direction_bound line 210
14. theorem OAI.Balanced.Local.bad_pencil_probability_le_common_factor line 248