OAI/Combinatorics/Progressions/Geometry/BoxOverlapSize.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.weight_correlating_large_overlaps line 11
2. theorem OAI.Erdos3.weight_correlating_large_box_overlaps line 42
3. theorem OAI.Erdos3.box_gowers_lower_bound_of_overlaps line 74
4. theorem OAI.Erdos3.side_gt_of_prod_gt line 137
5. theorem OAI.Erdos3.box_overlap_side_gt_of_card_gt line 151
6. theorem OAI.Erdos3.cardinality_ge_overlap_weight line 165