Removing the origin from the summands

This is Lemma 2.1 of Ruzsa's paper. Let X, Y ⊆ ℝ^D be finite sets with at least two points that contain 0 and whose other elements are lexicographically positive. Write X' = X \ {0} and Y' = Y \ {0}, let d be the affine dimension of X + Y and let U be the vector span of X' + Y'. The lemma geometric_deletion_cases states that one of the following holds.

• X' + Y' has dimension d and |X + Y| ≥ |X' + Y'| + d + 1. The points of X + Y outside X' + Y' are 0 and the points of C = (X' ∪ Y') \ (X' + Y'). Every point of X + Y is a sum of points of C, by induction along the lexicographic order, so C has at least d points.
• X' + Y' has dimension d - 1 and |X + Y| ≥ |Y| + |X' + Y'|. Here X' has a point outside U, and Y is disjoint from X' + Y'.
• X' + Y has dimension d - 1 and |X + Y| ≥ |Y| + |X' + Y|. Here X' + Y' has dimension d - 2, and Y is disjoint from X' + Y.
• X + Y' has dimension d - 1 and |X + Y| ≥ |X| + |X + Y'|. Here X' ⊆ U, and X is disjoint from X + Y'.

The case in which the dimension does not drop

The cases in which the dimension drops

theorem SumOfSetsInSeveralDimensions.geometric_deletion_cases {D d : ℕ} {X Y : Finset (Fin D → ℝ)} (h0X : 0 ∈ X) (h0Y : 0 ∈ Y) (hposX : ∀ x ∈ X, x ≠ 0 → 0 < toLex x) (hposY : ∀ y ∈ Y, y ≠ 0 → 0 < toLex y) (hXcard : 2 ≤ X.card) (hYcard : 2 ≤ Y.card) (hdim : (X + Y).affineDim = d) : (X.erase 0 + Y.erase 0).affineDim = d ∧ (X.erase 0 + Y.erase 0).card + d + 1 ≤ (X + Y).card ∨ (X.erase 0 + Y.erase 0).affineDim = d - 1 ∧ Y.card + (X.erase 0 + Y.erase 0).card ≤ (X + Y).card ∨ (X.erase 0 + Y).affineDim = d - 1 ∧ Y.card + (X.erase 0 + Y).card ≤ (X + Y).card ∨ (X + Y.erase 0).affineDim = d - 1 ∧ X.card + (X + Y.erase 0).card ≤ (X + Y).card

Lemma 2.1 of Ruzsa. Let X and Y contain 0, have at least two points each, and have all other elements lexicographically positive, and let X + Y have affine dimension d. Then removing 0 from X, from Y or from both gives a sumset of dimension d with at least d + 1 fewer points, or a sumset of dimension d - 1 with at least |Y| or |X| fewer points, as listed in the statement.