OAI/Combinatorics/BalancedRyser/Probability/FreshWitnessProbability.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.FreshWitnessProbability.offsetLaw_uniform line 16
2. def OAI.Balanced.FreshWitnessProbability.exposedLaw line 21
3. theorem OAI.Balanced.FreshWitnessProbability.exposedLaw_map_fresh line 27
4. theorem OAI.Balanced.FreshWitnessProbability.prescribed_offsets_probability line 45
5. theorem OAI.Balanced.FreshWitnessProbability.prescribed_point_incidence_probability line 62
6. theorem OAI.Balanced.FreshWitnessProbability.probability_exists_le_sum line 83
7. theorem OAI.Balanced.FreshWitnessProbability.oriented_pairs_probability line 96
8. theorem OAI.Balanced.FreshWitnessProbability.paired_witnesses_probability_le line 127