Sum of sets in several dimensions
Lean 4 formalization of Ruzsa's lower bound for sumsets in ℝ^D: if A and B are finite sets with B nonempty and |B| ≤ |A|, and A + B has affine dimension d, then |A + B| ≥ |A| + Σ_{t=1}^{|B|-1} min(d, |A| - t). For d ≥ 1 and |A| ≥ d + 1 the bound is attained in ℝ^d. The closed form |A + B| ≥ |A| + d|B| - d(d+1)/2, the asymmetric form of Freiman's lemma, is derived from the bound, and so is the bound 2κ - 1, for a real κ, on the Freiman dimension of a set X with |X + X| ≤ κ|X|.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000031
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000031/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000031/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'