OAI/Combinatorics/BalancedRyser/Probability/TupleExposure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.oldGeneratorIndices line 14
2. theorem OAI.Balanced.image_oldGeneratorIndices line 18
3. theorem OAI.Balanced.card_oldGeneratorIndices line 30
4. theorem OAI.Balanced.tuplePoint_eq_of_fixedGeneratorPosition line 37
5. theorem OAI.Balanced.fixedTuplePositions_table line 49
6. theorem OAI.Balanced.tuple_reuseSaving_le_countingExponent line 59
7. theorem OAI.Balanced.Configuration.exists_six_tuple_reuse_order line 66