OAI/Combinatorics/Progressions/Lattices/ProductiveAbsoluteCRTPatches.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.IntegerVectorAPFree.mono line 14
2. theorem OAI.Erdos3.IntegerVectorAPFree.affine_preimage line 20
3. theorem OAI.Erdos3.BooleanCubeKernel.joint_sample_progression_free line 44
4. theorem OAI.Erdos3.IntegerVectorAPFree.affine_residue_support line 76
5. theorem OAI.Erdos3.BooleanCubeKernel.joint_residue_sample_progression_free line 96
6. theorem OAI.Erdos3.PolynomialPatch.positive_score_target_lt_one line 127
7. theorem OAI.Erdos3.exists_absolute_crt_threshold_rule line 141
8. theorem OAI.Erdos3.exists_productive_absolute_crt_patches line 195