OAI/Combinatorics/Progressions/Estimates/JointBooleanRegularizationChoice.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_joint_boolean_good_region line 17
2. theorem OAI.Erdos3.exists_joint_boolean_good_region_with_tests line 86
3. def OAI.Erdos3.jointBooleanRegularizationBudget line 128
4. theorem OAI.Erdos3.jointBoolean_regularization_choice_error line 135