OAI/Combinatorics/BalancedRyser/Probability/RootSuccess.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.TupleAlignment.successfulOffsets_probability line 9
2. theorem OAI.Balanced.TupleAlignment.successfulOffsets_outer_probability line 22
3. theorem OAI.Balanced.TupleAlignment.tuplePoint_success_probability line 33
4. abbrev OAI.Balanced.TupleAlignment.RootPrescription line 56
5. def OAI.Balanced.TupleAlignment.RootPrescription.tuple line 59
6. theorem OAI.Balanced.TupleAlignment.RootPrescription.injective line 64
7. theorem OAI.Balanced.TupleAlignment.card_rootPrescription line 70
8. theorem OAI.Balanced.TupleAlignment.sum_success_probabilities line 80
9. def OAI.Balanced.TupleAlignment.rootSuccessCount line 91
10. theorem OAI.Balanced.TupleAlignment.mean_rootSuccessCount line 97