The values of the lower bound

The formulas (1.5), (1.6) and (1.7) of Ruzsa's paper for G_d(m, n) = sumsetCardLowerBound d m n when m ≤ n. Write t = n - m.

• sumsetCardLowerBound_of_add_le: if t ≥ d - 1, then G_d(m, n) = n + d * (m - 1). The paper states this for t ≥ d.
• two_mul_sumsetCardLowerBound_add_add, two_mul_sumsetCardLowerBound_add: if t < d < n, then 2 * G_d(m, n) = 2 * n * (d + 1) - d * (d + 1) - t * (t + 1) and 2 * G_d(m, n) = 2 * (n + d * (m - 1)) - (d - t) * (d - t - 1).
• two_mul_sumsetCardLowerBound_of_le: if 1 ≤ m ≤ n ≤ d, then 2 * G_d(m, n) = 2 * n + (m - 1) * (2 * n - m).

theorem SumOfSetsInSeveralDimensions.sumsetCardLowerBound_add_one {d m n : ℕ} (hm : 1 ≤ m) : sumsetCardLowerBound d (m + 1) n = sumsetCardLowerBound d m n + min d (n - m)

G_d(m + 1, n) = G_d(m, n) + min d (n - m) for m ≥ 1.

theorem SumOfSetsInSeveralDimensions.sumsetCardLowerBound_of_add_le {d m n : ℕ} (h : m + d ≤ n + 1) : sumsetCardLowerBound d m n = n + d * (m - 1)

Formula (1.5). If m + d ≤ n + 1, then G_d(m, n) = n + d * (m - 1).

theorem SumOfSetsInSeveralDimensions.two_mul_sumsetCardLowerBound_add_add {d m n : ℕ} (hmn : m ≤ n) (hnm : n < m + d) (hdn : d < n) : 2 * sumsetCardLowerBound d m n + d * (d + 1) + (n - m) * (n - m + 1) = 2 * n * (d + 1)

Formula (1.6). If m ≤ n < m + d and d < n, then 2 * G_d(m, n) + d * (d + 1) + (n - m) * (n - m + 1) = 2 * n * (d + 1).

theorem SumOfSetsInSeveralDimensions.two_mul_sumsetCardLowerBound_add {d m n : ℕ} (hmn : m ≤ n) (hnm : n < m + d) (hdn : d < n) : 2 * sumsetCardLowerBound d m n + (d - (n - m)) * (d - (n - m) - 1) = 2 * (n + d * (m - 1))

Formula (1.6), first form. If m ≤ n < m + d and d < n, then 2 * G_d(m, n) + (d - t) * (d - t - 1) = 2 * (n + d * (m - 1)), where t = n - m.

theorem SumOfSetsInSeveralDimensions.two_mul_sumsetCardLowerBound_of_le {d m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) (hnd : n ≤ d) : 2 * sumsetCardLowerBound d m n = 2 * n + (m - 1) * (2 * n - m)

Formula (1.7). If 1 ≤ m ≤ n ≤ d, then 2 * G_d(m, n) = 2 * n + (m - 1) * (2 * n - m).