OAI/Combinatorics/Progressions/Estimates/RelativeChildSliceGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.ResidueBoxSlice.coordinate_progression_subset line 14
2. theorem OAI.Erdos3.ResidueBoxSlice.stride_lt_two_div_density line 33
3. theorem OAI.Erdos3.ResidueBoxSlice.stride_le_exp_cost line 52
4. theorem OAI.Erdos3.ResidueBoxSlice.normalized_endpoint_geometry line 70
5. theorem OAI.Erdos3.ResidueBoxSlice.commonStrideBox_subset line 88
6. theorem OAI.Erdos3.ResidueBoxSlice.commonStrideBox_eq_parameter_image line 97