OAI/Combinatorics/BalancedRyser/Probability/AcyclicProductBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.DependencyExtraction.coordinateSwap line 11
2. theorem OAI.Balanced.DependencyExtraction.expect_coordinate_refresh line 23
3. theorem OAI.Balanced.DependencyExtraction.expect_mul_le_of_coordinate_bound line 36
4. theorem OAI.Balanced.DependencyExtraction.expect_prod_le_of_ranked_dependencies line 56
5. theorem OAI.Balanced.DependencyExtraction.uniform_event_bound_of_ranked_dependencies line 103
6. theorem OAI.Balanced.DependencyExtraction.uniform_event_bound_of_dependency_relation line 132
7. theorem OAI.Balanced.DependencyExtraction.uniform_probability_eq_filter_card line 150