Vosper's theorem

DefinitionArithmetic progressions with a common difference#✓fully proved

Let \(G\) be an additive commutative monoid and let \(A\) and \(B\) be finite subsets of \(G\). We say that \(A\) and \(B\) are arithmetic progressions with a common difference if there are \(d, a, b \in G\) such that \(A = \{a + nd : n \in \mathbb{N},\ n < |A|\}\) and \(B = \{b + nd : n \in \mathbb{N},\ n < |B|\}\), where \(nd\) is the sum of \(n\) copies of \(d\). The two progressions may have different initial terms and different lengths.

def AreFiniteArithmeticProgressionsWithCommonDifference {G : Type*} [AddCommMonoid G] [DecidableEq G]
    (A B : Finset G) : Prop :=
  ∃ d a b : G, (A : Set G).IsAPOfLengthWith A.card a d ∧
    (B : Set G).IsAPOfLengthWith B.card b d
Sources
  • Fabián Arias, Jerson Borja, and Samuel Anaya, Counting Integers Representable as Sums of k-th Powers Modulo n, Journal of Integer Sequences 26 (2023), Article 23.8.1, Theorem [Vosper] theo_Vosper condition (iii), lines 256–267, https://cs.uwaterloo.ca/journals/JIS/VOL26/Borja/borja4.tex: "A and B are arithmetic progressions with the same common difference".
Uses 1 · Used by 1
Statement usesSet arithmetic progressions with given first term and difference
Used byVosper's theorem

TheoremVosper's theorem#✓fully proved

Let \(p\) be a prime and let \(A\) and \(B\) be nonempty subsets of \(\mathbb{Z}/p\mathbb{Z}\) whose sumset \(A + B = \{a + b : a \in A, b \in B\}\) is not all of \(\mathbb{Z}/p\mathbb{Z}\). Then \(|A + B| = |A| + |B| - 1\) if and only if one of the following holds: (i) \(\min(|A|, |B|) = 1\); (ii) \(|A + B| = p - 1\) and there is an element \(c \in \mathbb{Z}/p\mathbb{Z}\) such that the complement of \(A + B\) is \(\{c\}\) and \(B\) is the complement of \(c - A = \{c - a : a \in A\}\); or (iii) \(A\) and \(B\) are arithmetic progressions with the same common difference, that is, there are \(d, a_0, b_0 \in \mathbb{Z}/p\mathbb{Z}\) with \(A = \{a_0 + n d : 0 \le n < |A|\}\) and \(B = \{b_0 + n d : 0 \le n < |B|\}\).

theorem vosper_eq_iff {p : ℕ} [Fact (Nat.Prime p)]
    (A B : Finset (ZMod p)) (hA : A.Nonempty) (hB : B.Nonempty)
    (hAB : A + B ≠ Finset.univ) :
    (A + B).card = A.card + B.card - 1 ↔
      (min A.card B.card = 1 ∨
        ((A + B).card = p - 1 ∧
          ∃ c : ZMod p,
            Finset.filter (fun x => x ∉ (A + B)) Finset.univ = {c} ∧
              B = Finset.filter
                (fun x => x ∉ Finset.image (fun a => c - a) A) Finset.univ) ∨
        AreFiniteArithmeticProgressionsWithCommonDifference A B)
Sources
Uses 2
Statement usesArithmetic progressions with a common difference
Proof usesSet arithmetic progressions with given first term and difference
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.