{"id":"palomar/PALOMAR-2026-10-22-000031","url":"https://github.com/gdahia/SumOfSetsInSeveralDimensions/tree/1f8da867debcce675e07cac515ea9598c1245a92","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000031-v1.json","repo":"https://github.com/gdahia/SumOfSetsInSeveralDimensions","tags":["math.CO","math.NT","msc:11P70","msc:11B13","msc:11B75","sumsets","freiman-lemma","discrete-geometry","lean-formalization"],"score":0,"title":"Sum of sets in several dimensions","trust":"high","domain":"math.CO","source":"palomar","authors":["Gabriel Dahia"],"reviews":0,"subject":"math.CO","summary":"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|.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Sum of sets in several dimensions","identifier":"https://doi.org/10.1007/BF01302969","relationship":"formalizes"}]}