OAI/Combinatorics/BalancedRyser/Local/AlignmentStepLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.AlignedListProbability.conditioned_alignment_suffix_observed line 16
2. theorem OAI.Balanced.AlignedListProbability.conditioned_alignment_step line 45
3. theorem OAI.Balanced.AlignedListProbability.current_tuple_conditional_ratio line 93
4. abbrev OAI.Balanced.AlignedListProbability.CurrentFreeCoordinates line 127
5. def OAI.Balanced.AlignedListProbability.generateCurrentTupleOffsets line 130
6. theorem OAI.Balanced.AlignedListProbability.current_tuple_generated_probability line 138
7. theorem OAI.Balanced.AlignedListProbability.step_exposed_count line 158
8. theorem OAI.Balanced.AlignedListProbability.full_aligned_step_generated_probability line 166