Documentation

LeanPool.SumOfSetsInSeveralDimensions.LowerBoundFunction

The lower bound as a function of the dimension and the cardinalities #

The lower bound in Ruzsa's theorem for sets A and B with |A| = n ≥ |B| = m and A + B of affine dimension d is sumsetCardLowerBound d m n = n + ∑ t ∈ {1, …, m - 1}, min d (n - t), the function G_d(m, n) of the paper. The induction in the proof removes one point from A, from B, or from both, and the dimension stays the same or drops by one. This file proves the inequality between the values of the bound that each of these cases needs.

source
def SumOfSetsInSeveralDimensions.sumsetCardLowerBound (d m n : ℕ) :
ℕ

The lower bound G_d(m, n) of Ruzsa's theorem for the size of a sumset of affine dimension d of sets of sizes m ≤ n.

Equations
Instances For
    source
    theorem SumOfSetsInSeveralDimensions.sumsetCardLowerBound_eq (d m n : ℕ) :
    sumsetCardLowerBound d m n = n + ∑ t ∈ Finset.Icc 1 (m - 1), min d (n - t)

    The definition of sumsetCardLowerBound.

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

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

    source
    theorem SumOfSetsInSeveralDimensions.sumsetCardLowerBound_of_full_case {d m n p s : ℕ} (hm : 2 ≤ m) (hrec : sumsetCardLowerBound d (m - 1) (n - 1) ≤ p) (hcard : p + d + 1 ≤ s) :
    sumsetCardLowerBound d m n ≤ s

    The case in which one point is removed from each set and the dimension does not change: the sumset loses at least d + 1 points.

    source
    theorem SumOfSetsInSeveralDimensions.sumsetCardLowerBound_of_large_case {d m n p s : ℕ} (hm : 2 ≤ m) (hmn : m ≤ n) (hrec : sumsetCardLowerBound (d - 1) (m - 1) (n - 1) ≤ p) (hcard : n + p ≤ s) :
    sumsetCardLowerBound d m n ≤ s

    The case in which one point is removed from each set and the dimension drops by one: the sumset loses at least n points.

    source
    theorem SumOfSetsInSeveralDimensions.sumsetCardLowerBound_of_small_case {d m n p s : ℕ} (hm : 2 ≤ m) (hmn : m ≤ n) (hrec : sumsetCardLowerBound (d - 1) (m - 1) n ≤ p) (hcard : n + p ≤ s) :
    sumsetCardLowerBound d m n ≤ s

    The case in which one point is removed from the smaller set and the dimension drops by one: the sumset loses at least n points.

    source
    theorem SumOfSetsInSeveralDimensions.sumsetCardLowerBound_of_equal_right_case {d m p s : ℕ} (hm : 2 ≤ m) (hrec : sumsetCardLowerBound (d - 1) (m - 1) m ≤ p) (hcard : m + p ≤ s) :
    sumsetCardLowerBound d m m ≤ s

    The case in which the sets have the same size m, one point is removed from one of them and the dimension drops by one: the sumset loses at least m points.

    source
    theorem SumOfSetsInSeveralDimensions.sumsetCardLowerBound_of_strict_right_case {d m n p s : ℕ} (hm : 1 ≤ m) (hmn : m < n) (hrec : sumsetCardLowerBound (d - 1) m (n - 1) ≤ p) (hcard : m + p ≤ s) :
    sumsetCardLowerBound d m n ≤ s

    The case in which one point is removed from the strictly larger set and the dimension drops by one: the sumset loses at least m points.