Restricted signed sumsets

DefinitionRestricted sumset#✓fully proved

For a natural number \(h\) and a finite subset \(A\) of an additive commutative monoid \(G\), the restricted sumset \(h^{\wedge} A\) is the set of all sums \(\sum_{a \in B} a\) with \(B\) an \(h\)-element subset of \(A\), that is, the sums of \(h\) distinct elements of \(A\). In particular \(0^{\wedge} A = \{0\}\).

The source works in the integers; here \(G\) is an arbitrary additive commutative monoid.

public def restrictedSumset {G : Type*} [AddCommMonoid G] [DecidableEq G] (h : ℕ)
    (A : Finset G) : Finset G :=
  (A.powersetCard h).image (fun B => ∑ a ∈ B, a)
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Definition of restricted sumset.
Used by 9
Used byNathanson's bound for restricted sumsets and its inverse · Inverse theorem for the extremal restricted signed sumset of positive integers · Inverse theorem for the extremal restricted signed sumset of sets containing zero · Coefficient description of the restricted sumset · Decomposition of sums with at least \(r\) distinct terms · Dias da Silva–Hamidoune theorem · Nathanson's inverse theorem for restricted sumsets · Restricted twofold sumset of \(\{0, 1, 2\}\) · Subset sums with a bounded number of terms

DefinitionRestricted signed sumset#✓fully proved

For a natural number \(h\) and a finite set \(A\) of integers, the restricted signed sumset \(h^{\wedge}_{\pm} A\) is the set of all integers \(\sum_{a \in B} a - 2 \sum_{a \in N} a\), where \(B\) ranges over the \(h\)-element subsets of \(A\) and \(N\) ranges over the subsets of \(B\). These are the sums of the elements of \(B\) in which the elements of \(N\) are given a negative sign.

public def restrictedSignedSumset (h : ℕ) (A : Finset ℤ) : Finset ℤ :=
  ((A.powersetCard h).sigma (fun B => B.powerset)).image
    (fun p => ∑ a ∈ p.1, a - 2 * ∑ a ∈ p.2, a)
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Definition of restricted signed sumset.
Used by 23
Used byLower bound for restricted signed sumsets of arithmetic progressions · Restricted signed sumsets of arithmetic progressions with one more term than summands · Restricted signed sumsets of arithmetic progressions containing zero · The restricted signed 4-fold sumset of \(\{0, 1, 2, 4, 6\}\) · Restricted signed fourfold sumsets of five positive integers · Lower bound for restricted signed 4-fold sumsets of positive integers · Restricted signed 4-fold sumsets when exactly one gap differs from twice the minimum · Restricted signed fourfold sumsets when exactly two gaps differ from twice the least element · Restricted signed fourfold sumsets when exactly one gap equals twice the least element · Restricted signed fourfold sumsets when no gap equals twice the least element and the first and third gaps differ · Restricted signed fourfold sumsets when no gap equals twice the least element, the first and third gaps agree, and the last two gaps do not sum to twice the least element · Restricted signed fourfold sumsets when no gap equals twice the least element, the first and third gaps agree, and the last two gaps sum to twice the least element · Restricted signed 4-fold sumsets when no gap equals twice the minimum · Lower bound for restricted signed 4-fold sumsets of nonnegative sets containing zero · The restricted signed 4-fold sumset of \(\{1, 3, 5, 7, 9\}\) · Restricted signed sumsets of sets with Fibonacci-type growth · Restricted signed sumsets under gap conditions · Extending a restricted signed sumset bound from the first \(h+1\) elements · Lower bounds for restricted signed sumsets of nonnegative integers · The restricted signed 3-fold sumset of \(\{1, 2, 3, 4\}\) · Inverse theorem for the extremal restricted signed sumset of positive integers · Inverse theorem for the extremal restricted signed sumset of sets containing zero · Coefficient description of the restricted signed sumset

TheoremCoefficient description of the restricted sumset#✓fully proved

For a natural number \(h\), a finite set \(A\) of integers and an integer \(x\), \(x\) lies in the restricted sumset \(h^{\wedge} A\) if and only if there is a function \(c : \mathbb{Z} \to \mathbb{Z}\) with \(c(a) \in \{0, 1\}\) for every \(a \in A\), \(\sum_{a \in A} c(a) = h\) and \(x = \sum_{a \in A} c(a)\, a\).

public theorem mem_restrictedSumset_iff (h : ℕ) (A : Finset ℤ) (x : ℤ) :
    x ∈ restrictedSumset h A ↔
      ∃ c : ℤ → ℤ,
        (∀ a ∈ A, c a = 0 ∨ c a = 1) ∧
        ∑ a ∈ A, c a = (h : ℤ) ∧
        x = ∑ a ∈ A, c a * a
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Definition of restricted sumset.
Uses 1
Statement usesRestricted sumset

TheoremCoefficient description of the restricted signed sumset#✓fully proved

For a natural number \(h\), a finite set \(A\) of integers and an integer \(x\), \(x\) lies in the restricted signed sumset \(h^{\wedge}_{\pm} A\) if and only if there is a function \(c : \mathbb{Z} \to \mathbb{Z}\) with \(c(a) \in \{-1, 0, 1\}\) for every \(a \in A\), \(\sum_{a \in A} |c(a)| = h\) and \(x = \sum_{a \in A} c(a)\, a\).

public theorem mem_restrictedSignedSumset_iff (h : ℕ) (A : Finset ℤ) (x : ℤ) :
    x ∈ restrictedSignedSumset h A ↔
      ∃ c : ℤ → ℤ,
        (∀ a ∈ A, c a = -1 ∨ c a = 0 ∨ c a = 1) ∧
        ∑ a ∈ A, |c a| = (h : ℤ) ∧
        x = ∑ a ∈ A, c a * a
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Definition of restricted signed sumset.
Uses 1
Statement usesRestricted signed sumset

DefinitionSet of values of a finite integer sequence#✓fully proved

For a sequence \(a_0, \dots, a_{k-1}\) of integers, this is the finite set \(\{a_i : 0 \le i < k\}\) of its values.

No order or injectivity is assumed; the statements that use it assume what they need.

public def orderedFinset {k : ℕ} (a : Fin k → ℤ) : Finset ℤ :=
  Finset.univ.image a
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, notation for ordered finite sets.
Used by 15
Used byLower bound for restricted signed sumsets of arithmetic progressions · Restricted signed sumsets of arithmetic progressions with one more term than summands · Restricted signed sumsets of arithmetic progressions containing zero · Restricted signed 4-fold sumsets when exactly one gap differs from twice the minimum · Restricted signed fourfold sumsets when exactly two gaps differ from twice the least element · Restricted signed fourfold sumsets when exactly one gap equals twice the least element · Restricted signed fourfold sumsets when no gap equals twice the least element and the first and third gaps differ · Restricted signed fourfold sumsets when no gap equals twice the least element, the first and third gaps agree, and the last two gaps do not sum to twice the least element · Restricted signed fourfold sumsets when no gap equals twice the least element, the first and third gaps agree, and the last two gaps sum to twice the least element · Restricted signed 4-fold sumsets when no gap equals twice the minimum · Restricted signed sumsets of sets with Fibonacci-type growth · Restricted signed sumsets under gap conditions · Extending a restricted signed sumset bound from the first \(h+1\) elements · Inverse theorem for the extremal restricted signed sumset of positive integers · Inverse theorem for the extremal restricted signed sumset of sets containing zero

DefinitionInitial segment of a finite integer sequence#✓fully proved

For a sequence \(a_0, \dots, a_{k-1}\) of integers and a natural number \(n\), the initial segment of length \(n\) is the set \(\{a_i : 0 \le i < k,\ i < n\}\) of the values at indices below \(n\); it is the set of all values of the sequence when \(n \ge k\).

public def initialSegment {k : ℕ} (a : Fin k → ℤ) (n : ℕ) : Finset ℤ :=
  (Finset.univ.filter fun i : Fin k => (i : ℕ) < n).image a
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, notation for initial subsets.
Used by 3
Used byExtending a restricted signed sumset bound from the first \(h+1\) elements · Inverse theorem for the extremal restricted signed sumset of positive integers · Inverse theorem for the extremal restricted signed sumset of sets containing zero

DefinitionFinite integer sequences in arithmetic progression#✓fully proved

A sequence \(a_0, \dots, a_{k-1}\) of integers is an arithmetic progression with common difference \(d\) if \(d > 0\) and \(a_{i+1} = a_i + d\) for every \(i\) with \(i + 1 < k\).

The condition is stated on adjacent terms, so no nonemptiness assumption is needed to name a first term.

public def IsIndexedAP {k : ℕ} (a : Fin k → ℤ) (d : ℤ) : Prop :=
  0 < d ∧ ∀ (i j : Fin k), (i : ℕ) + 1 = (j : ℕ) → a j = a i + d
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, definition of arithmetic progression.
Used by 5
Used byLower bound for restricted signed sumsets of arithmetic progressions · Restricted signed sumsets of arithmetic progressions with one more term than summands · Restricted signed sumsets of arithmetic progressions containing zero · Inverse theorem for the extremal restricted signed sumset of positive integers · Inverse theorem for the extremal restricted signed sumset of sets containing zero

DefinitionDilation of a finite set of integers#✓fully proved

For an integer \(d\) and a finite set \(B\) of integers, the dilation \(d \cdot B\) is the set \(\{db : b \in B\}\).

public def scaleFinset (d : ℤ) (B : Finset ℤ) : Finset ℤ :=
  B.image (fun b => d * b)
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, dilation notation.
Used by 5
Used byRestricted signed fourfold sumsets of five positive integers · Lower bound for restricted signed 4-fold sumsets of positive integers · Inverse theorem for the extremal restricted signed sumset of positive integers · Inverse theorem for the extremal restricted signed sumset of sets containing zero · \(\{0, 1, 2, 4, 6\}\) is not a dilate of \(\{0, 1, 2, 3, 4\}\)

DefinitionThe first \(k\) odd positive integers#✓fully proved

For a natural number \(k\), this is the set of integers \(\{1, 3, \dots, 2k - 1\} = \{2i + 1 : 0 \le i < k\}\); it is empty when \(k = 0\).

public def oddProgression (k : ℕ) : Finset ℤ :=
  (Finset.range k).image (fun i : ℕ => 2 * (i : ℤ) + 1)
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, odd-progression notation.
Used by 3
Used byRestricted signed fourfold sumsets of five positive integers · Lower bound for restricted signed 4-fold sumsets of positive integers · Inverse theorem for the extremal restricted signed sumset of positive integers

DefinitionValues of a finite integer sequence after its first term#✓fully proved

For a sequence \(a_0, \dots, a_{k-1}\) of integers, this is the set \(\{a_i : 1 \le i < k\}\). When the sequence is strictly increasing, it is the set \(A' = A \setminus \{a_0\}\) obtained from \(A = \{a_0, \dots, a_{k-1}\}\) by removing its least element.

public def tailFinset {k : ℕ} (a : Fin k → ℤ) : Finset ℤ :=
  (Finset.univ.filter fun i : Fin k => 0 < (i : ℕ)).image a
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, notation A'.
Used by 2
Used byInverse theorem for the extremal restricted signed sumset of positive integers · Inverse theorem for the extremal restricted signed sumset of sets containing zero

DefinitionZero-based integer interval#✓fully proved

For a natural number \(k\), the integer interval \([0, k-1]\) is the set \(\{0, 1, \dots, k-1\}\) of integers \(i\) with \(0 \le i < k\); it is empty when \(k = 0\).

public def zeroInterval (k : ℕ) : Finset ℤ :=
  (Finset.range k).image (fun i : ℕ => (i : ℤ))
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, interval notation.
Used by 2
Used byInverse theorem for the extremal restricted signed sumset of sets containing zero · \(\{0, 1, 2, 4, 6\}\) is not a dilate of \(\{0, 1, 2, 3, 4\}\)

TheoremThe restricted signed 4-fold sumset of \(\{1, 3, 5, 7, 9\}\)#✓fully proved

The restricted signed 4-fold sumset \(4^{\wedge}_{\pm} \{1, 3, 5, 7, 9\}\) has exactly \(25\) elements.

This is an extremal five-element set of positive integers in Theorem 10 of the source: it attains that theorem's lower bound \(25\).

public theorem card_restrictedSignedSumset_four_odd_five :
    (restrictedSignedSumset 4 {1, 3, 5, 7, 9}).card = 25
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 10 example.
Uses 1
Statement usesRestricted signed sumset

TheoremThe restricted signed 4-fold sumset of \(\{0, 1, 2, 4, 6\}\)#✓fully proved

The restricted signed 4-fold sumset \(4^{\wedge}_{\pm} \{0, 1, 2, 4, 6\}\) has exactly \(21 = 8 \cdot 5 - 19\) elements.

This is the extremal value \(8k - 19\) at \(k = 5\) of the lower bound in Theorem 11 of the source. Since \(\{0, 1, 2, 4, 6\}\) differs from \(d \cdot \{0, 1, 2, 3, 4\}\) for every integer \(d\), it refutes the inverse sentence of that theorem (the counterexample is ours, not the paper's).

public theorem card_restrictedSignedSumset_four_counterexample :
    (restrictedSignedSumset 4 {0, 1, 2, 4, 6}).card = 21
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 11 (lower bound 8k - 19 at k = 5).
Uses 1
Statement usesRestricted signed sumset

Theorem\(\{0, 1, 2, 4, 6\}\) is not a dilate of \(\{0, 1, 2, 3, 4\}\)#✓fully proved

For every integer \(d\), the set \(\{0, 1, 2, 4, 6\}\) differs from the dilation \(d \cdot \{0, 1, 2, 3, 4\} = \{0, d, 2d, 3d, 4d\}\).

Indeed, \(1 = di\) with \(0 \le i \le 4\) forces \(d = \pm 1\), and then \(6\) is not of the form \(di\).

public theorem ne_scaleFinset_zeroInterval_five (d : ℤ) :
    ({0, 1, 2, 4, 6} : Finset ℤ) ≠ scaleFinset d (zeroInterval 5)
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 11 (inverse sentence, A = d * [0,k-1]).
Uses 2
Statement usesDilation of a finite set of integers · Zero-based integer interval

TheoremThe restricted signed 3-fold sumset of \(\{1, 2, 3, 4\}\)#✓fully proved

The restricted signed 3-fold sumset \(3^{\wedge}_{\pm} \{1, 2, 3, 4\}\) has exactly \(19\) elements.

public theorem card_restrictedSignedSumset_three_four :
    (restrictedSignedSumset 3 {1, 2, 3, 4}).card = 19
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Definition of restricted signed sumset.
Uses 1
Statement usesRestricted signed sumset

TheoremLower bounds for restricted signed sumsets of nonnegative integers#●ready to prove

Let \(h\) and \(k\) be integers with \(1 \le h \le k\), let \(A\) be a set of \(k\) nonnegative integers, and write \(h^{\wedge}_{\pm} A\) for the restricted signed \(h\)-fold sumset of \(A\). If \(0 \notin A\), then \(2|h^{\wedge}_{\pm} A| \ge 4(hk - h^2) + h(h+1) + 2\); if \(0 \in A\), then \(2|h^{\wedge}_{\pm} A| \ge 4(hk - h^2) + h(h-1) + 2\).

The source states these bounds divided by \(2\). Its remark that they are optimal for \(h = 1\), \(h = 2\) and \(h = k\) is not part of this statement.

public theorem_wanted card_restrictedSignedSumset_general_lower_bounds
    (h k : ℕ) (A : Finset ℤ) (hh : 0 < h) (hk : h ≤ k) (hcard : A.card = k)
    (hnonneg : ∀ a ∈ A, 0 ≤ a) :
    (0 ∉ A →
      2 * ((restrictedSignedSumset h A).card : ℤ) ≥
        4 * ((h : ℤ) * k - (h : ℤ) ^ 2) + (h : ℤ) * (h + 1) + 2) ∧
    (0 ∈ A →
      2 * ((restrictedSignedSumset h A).card : ℤ) ≥
        4 * ((h : ℤ) * k - (h : ℤ) ^ 2) + (h : ℤ) * (h - 1) + 2)
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 1.
Uses 1
Statement usesRestricted signed sumset

TheoremNathanson's bound for restricted sumsets and its inverse#●ready to prove

Let \(A\) be a nonempty finite set of \(k\) integers and let \(h\) be a natural number with \(1 \le h \le k\). Then the restricted sumset \(h^{\wedge} A\) has at least \(hk - h^2 + 1\) elements. Moreover, if \(k \ge 5\) and \(2 \le h \le k - 2\), then \(h^{\wedge} A\) has exactly \(hk - h^2 + 1\) elements if and only if there are integers \(a\) and \(d > 0\) such that \(A\) is the arithmetic progression of length \(k\) with first term \(a\) and difference \(d\), that is, \(A = \{a + nd : 0 \le n < k\}\).

public theorem_wanted card_restrictedSumset_ge_and_eq_iff_ap
    (h : ℕ) (A : Finset ℤ) (hA : A.Nonempty) (hh : 1 ≤ h) (hhA : h ≤ A.card) :
    ((restrictedSumset h A).card : ℤ) ≥ (h : ℤ) * A.card - (h : ℤ) ^ 2 + 1 ∧
    (5 ≤ A.card → 2 ≤ h → h ≤ A.card - 2 →
      (((restrictedSumset h A).card : ℤ) = (h : ℤ) * A.card - (h : ℤ) ^ 2 + 1 ↔
        ∃ a d : ℤ, 0 < d ∧ (A : Set ℤ).IsAPOfLengthWith A.card a d))
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 2.
Uses 2
Statement usesRestricted sumset · Set arithmetic progressions with given first term and difference

TheoremRestricted signed sumsets of arithmetic progressions with one more term than summands#●ready to prove

Let \(h \ge 3\) be a natural number and let \(a_1 < a_2 < \cdots < a_{h+1}\) be positive integers that form an arithmetic progression with common difference \(d > 0\), that is, \(a_{i+1} = a_i + d\) for \(1 \le i \le h\). Let \(A = \{a_1, \ldots, a_{h+1}\}\) and let \(h^{\wedge}_{\pm} A\) be the restricted signed sumset of \(A\). Then \(|h^{\wedge}_{\pm} A| \ge (h+1)^2\) if \(d = 2a_1\), and \(|h^{\wedge}_{\pm} A| \ge (h+1)^2 + 1\) otherwise. Moreover, \(|h^{\wedge}_{\pm} A| = (h+1)^2\) if and only if \(d = 2a_1\).

public theorem_wanted card_restrictedSignedSumset_ap_h_add_one
    (h : ℕ) (hh : 3 ≤ h) (a : Fin (h + 1) → ℤ) (d : ℤ)
    (ha : StrictMono a) (hpos : ∀ i, 0 < a i) (hap : IsIndexedAP a d) :
    (((restrictedSignedSumset h (orderedFinset a)).card : ℤ) ≥
      if d = 2 * a ⟨0, by omega⟩ then ((h + 1 : ℕ) : ℤ) ^ 2
      else ((h + 1 : ℕ) : ℤ) ^ 2 + 1) ∧
    (((restrictedSignedSumset h (orderedFinset a)).card : ℤ) =
        ((h + 1 : ℕ) : ℤ) ^ 2 ↔ d = 2 * a ⟨0, by omega⟩)
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 3.
Uses 3
Statement usesFinite integer sequences in arithmetic progression · Set of values of a finite integer sequence · Restricted signed sumset

TheoremLower bound for restricted signed sumsets of arithmetic progressions#●ready to prove

Let \(h \ge 3\) and \(k \ge h + 1\) be natural numbers, and let \(a_1 < a_2 < \cdots < a_k\) be integers with \(a_1 > 0\) that form an arithmetic progression with common difference \(d > 0\), that is, \(a_{i+1} = a_i + d\) for \(1 \le i < k\). Let \(A = \{a_1, \ldots, a_k\}\) and let \(h^{\wedge}_{\pm} A\) be the restricted signed sumset of \(A\). Then \(|h^{\wedge}_{\pm} A| \ge 2hk - h^2 + 1\) if \(d = 2a_1\), and \(|h^{\wedge}_{\pm} A| \ge 2hk - h^2 + 2\) otherwise. Moreover, \(|h^{\wedge}_{\pm} A| = 2hk - h^2 + 1\) if and only if \(d = 2a_1\).

public theorem_wanted card_restrictedSignedSumset_ap_ge
    (h k : ℕ) (hh : 3 ≤ h) (hk : h + 1 ≤ k) (a : Fin k → ℤ) (d : ℤ)
    (ha : StrictMono a) (hpos : 0 < a ⟨0, by omega⟩) (hap : IsIndexedAP a d) :
    (((restrictedSignedSumset h (orderedFinset a)).card : ℤ) ≥
      if d = 2 * a ⟨0, by omega⟩ then 2 * (h : ℤ) * k - (h : ℤ) ^ 2 + 1
      else 2 * (h : ℤ) * k - (h : ℤ) ^ 2 + 2) ∧
    (((restrictedSignedSumset h (orderedFinset a)).card : ℤ) =
        2 * (h : ℤ) * k - (h : ℤ) ^ 2 + 1 ↔ d = 2 * a ⟨0, by omega⟩)
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Corollary 1.
Uses 3
Statement usesFinite integer sequences in arithmetic progression · Set of values of a finite integer sequence · Restricted signed sumset

TheoremRestricted signed sumsets of arithmetic progressions containing zero#●ready to prove

Let \(h\) and \(k\) be natural numbers with \(4 \le h \le k - 1\), and let \(0 = a_1 < a_2 < \cdots < a_k\) be nonnegative integers that form an arithmetic progression with common difference \(d > 0\), that is, \(a_{i+1} = a_i + d\) for \(1 \le i < k\). Let \(A = \{a_1, \ldots, a_k\}\) and let \(h^{\wedge}_{\pm} A\) be the restricted signed sumset of \(A\). Then \(|h^{\wedge}_{\pm} A| = 2hk - h(h+1) + 1\).

public theorem_wanted card_restrictedSignedSumset_ap_zero
    (h k : ℕ) (hh : 4 ≤ h) (hk : h ≤ k - 1) (a : Fin k → ℤ) (d : ℤ)
    (ha : StrictMono a) (hnonneg : ∀ i, 0 ≤ a i)
    (hzero : a ⟨0, by omega⟩ = 0) (hap : IsIndexedAP a d) :
    ((restrictedSignedSumset h (orderedFinset a)).card : ℤ) =
      2 * (h : ℤ) * k - (h : ℤ) * (h + 1) + 1
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 4.
Uses 3
Statement usesFinite integer sequences in arithmetic progression · Set of values of a finite integer sequence · Restricted signed sumset

TheoremInverse theorem for the extremal restricted signed sumset of positive integers#●ready to prove

Let \(h\) and \(k\) be natural numbers with \(4 \le h \le k - 1\), and let \(A = \{a_1 < a_2 < \cdots < a_k\}\) be a set of \(k\) positive integers. Write \(A_{h+1} = \{a_1, \dots, a_{h+1}\}\), \(A' = \{a_2, \dots, a_k\}\) and \(-A' = \{-x : x \in A'\}\). Suppose that the restricted signed sumset \(h^{\wedge}_{\pm} A\) has exactly \(2hk - h^2 + 1\) elements and that at least one of the following holds: (a) there is \(d > 0\) with \(a_{i+1} = a_i + d\) for all \(1 \le i < k\); (b) \(A_{h+1} = \{b + nd : 0 \le n \le h\}\) for some integers \(b\) and \(d > 0\); (c) \(h^{\wedge}_{\pm} A_{h+1}\) has at least \((h+1)^2\) elements and \(4 \le h \le k - 3\); (d) \(h^{\wedge}_{\pm} A = h^{\wedge}(-A') \cup h^{\wedge}_{\pm} A_{h+1} \cup h^{\wedge} A'\), where \(h^{\wedge}\) is the restricted sumset, and \(A' = \{b + nd : 0 \le n < k - 1\}\) for some integers \(b\) and \(d > 0\); (e) \(h^{\wedge}_{\pm} A_{h+1}\) has at least \((h+1)^2\) elements and \(A' = \{b + nd : 0 \le n < k - 1\}\) for some integers \(b\) and \(d > 0\). Then \(A = a_1 \cdot \{1, 3, \dots, 2k - 1\} = \{(2i - 1) a_1 : 1 \le i \le k\}\).

MetaMathlibExt.eq_scaled_oddProgression_of_extremal · 19 lines 
public theorem_wanted eq_scaled_oddProgression_of_extremal
    (h k : ℕ) (hh : 4 ≤ h) (hk : h ≤ k - 1) (a : Fin k → ℤ)
    (ha : StrictMono a) (hpos : ∀ i, 0 < a i)
    (heq : ((restrictedSignedSumset h (orderedFinset a)).card : ℤ) =
      2 * (h : ℤ) * k - (h : ℤ) ^ 2 + 1)
    (hcase :
      (∃ d, IsIndexedAP a d) ∨
      (∃ b d, 0 < d ∧ (initialSegment a (h + 1) : Set ℤ).IsAPOfLengthWith (h + 1) b d) ∨
      (((restrictedSignedSumset h (initialSegment a (h + 1))).card : ℤ) ≥
          ((h + 1 : ℕ) : ℤ) ^ 2 ∧ 4 ≤ h ∧ h ≤ k - 3) ∨
      (restrictedSignedSumset h (orderedFinset a) =
          restrictedSumset h ((tailFinset a).image (-·)) ∪
            restrictedSignedSumset h (initialSegment a (h + 1)) ∪
            restrictedSumset h (tailFinset a) ∧
        ∃ b d, 0 < d ∧ (tailFinset a : Set ℤ).IsAPOfLengthWith (k - 1) b d) ∨
      (((restrictedSignedSumset h (initialSegment a (h + 1))).card : ℤ) ≥
          ((h + 1 : ℕ) : ℤ) ^ 2 ∧
        ∃ b d, 0 < d ∧ (tailFinset a : Set ℤ).IsAPOfLengthWith (k - 1) b d)) :
    orderedFinset a = scaleFinset (a ⟨0, by omega⟩) (oddProgression k)
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 5.
Uses 9
Statement usesFinite integer sequences in arithmetic progression · Initial segment of a finite integer sequence · The first \(k\) odd positive integers · Set of values of a finite integer sequence · Restricted signed sumset · Restricted sumset · Dilation of a finite set of integers · Values of a finite integer sequence after its first term · Set arithmetic progressions with given first term and difference

TheoremInverse theorem for the extremal restricted signed sumset of sets containing zero#●ready to prove

Let \(h\) and \(k\) be natural numbers with \(4 \le h \le k - 1\), and let \(A = \{a_0 < a_1 < \cdots < a_{k-1}\}\) be a set of \(k\) nonnegative integers with \(a_0 = 0\). Write \(A_h = \{a_0, \dots, a_h\}\), \(A' = \{a_1, \dots, a_{k-1}\}\) and \(-A' = \{-x : x \in A'\}\). Suppose that the restricted signed sumset \(h^{\wedge}_{\pm} A\) has exactly \(2hk - h(h+1) + 1\) elements and that at least one of the following holds: (a) there is \(d > 0\) with \(a_{i+1} = a_i + d\) for all \(0 \le i < k - 1\); (b) \(A_h = \{b + nd : 0 \le n \le h\}\) for some integers \(b\) and \(d > 0\); (c) \(h^{\wedge}_{\pm} A_h\) has at least \(h(h+1) + 1\) elements and \(4 \le h \le k - 3\); (d) \(h^{\wedge}_{\pm} A = h^{\wedge}(-A') \cup h^{\wedge}_{\pm} A_h \cup h^{\wedge} A'\), where \(h^{\wedge}\) is the restricted sumset, and \(A' = \{b + nd : 0 \le n < k - 1\}\) for some integers \(b\) and \(d > 0\); (e) \(h^{\wedge}_{\pm} A_h\) has at least \(h(h+1) + 1\) elements and \(A' = \{b + nd : 0 \le n < k - 1\}\) for some integers \(b\) and \(d > 0\). Then \(A = a_1 \cdot \{0, 1, \dots, k - 1\} = \{i a_1 : 0 \le i < k\}\).

MetaMathlibExt.eq_scaled_zeroInterval_of_extremal · 19 lines 
public theorem_wanted eq_scaled_zeroInterval_of_extremal
    (h k : ℕ) (hh : 4 ≤ h) (hk : h ≤ k - 1) (a : Fin k → ℤ)
    (ha : StrictMono a) (hnonneg : ∀ i, 0 ≤ a i) (hzero : a ⟨0, by omega⟩ = 0)
    (heq : ((restrictedSignedSumset h (orderedFinset a)).card : ℤ) =
      2 * (h : ℤ) * k - (h : ℤ) * (h + 1) + 1)
    (hcase :
      (∃ d, IsIndexedAP a d) ∨
      (∃ b d, 0 < d ∧ (initialSegment a (h + 1) : Set ℤ).IsAPOfLengthWith (h + 1) b d) ∨
      (((restrictedSignedSumset h (initialSegment a (h + 1))).card : ℤ) ≥
          (h : ℤ) * (h + 1) + 1 ∧ 4 ≤ h ∧ h ≤ k - 3) ∨
      (restrictedSignedSumset h (orderedFinset a) =
          restrictedSumset h ((tailFinset a).image (-·)) ∪
            restrictedSignedSumset h (initialSegment a (h + 1)) ∪
            restrictedSumset h (tailFinset a) ∧
        ∃ b d, 0 < d ∧ (tailFinset a : Set ℤ).IsAPOfLengthWith (k - 1) b d) ∨
      (((restrictedSignedSumset h (initialSegment a (h + 1))).card : ℤ) ≥
          (h : ℤ) * (h + 1) + 1 ∧
        ∃ b d, 0 < d ∧ (tailFinset a : Set ℤ).IsAPOfLengthWith (k - 1) b d)) :
    orderedFinset a = scaleFinset (a ⟨1, by omega⟩) (zeroInterval k)
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 6.
Uses 9
Statement usesFinite integer sequences in arithmetic progression · Initial segment of a finite integer sequence · Set of values of a finite integer sequence · Restricted signed sumset · Restricted sumset · Dilation of a finite set of integers · Values of a finite integer sequence after its first term · Zero-based integer interval · Set arithmetic progressions with given first term and difference

TheoremRestricted signed sumsets of sets with Fibonacci-type growth#●ready to prove

Let \(h \ge 3\) and let \(a_1 < a_2 < \dots < a_{h+1}\) be positive integers such that \(a_i \ge a_{i-1} + a_{i-2}\) for every \(i\) with \(4 \le i \le h + 1\). Write \(h^{\wedge}_{\pm} A\) for the restricted signed \(h\)-fold sumset of \(A = \{a_1, \dots, a_{h+1}\}\). Then \(|h^{\wedge}_{\pm} A| \ge (h+1)^2 + 1\).

public theorem_wanted card_restrictedSignedSumset_ge_of_fibonacci_growth
    (h : ℕ) (hh : 3 ≤ h) (a : Fin (h + 1) → ℤ) (ha : StrictMono a)
    (hpos : ∀ i, 0 < a i)
    (hgrowth : ∀ i : Fin (h - 2),
      a ⟨i + 3, by omega⟩ ≥ a ⟨i + 2, by omega⟩ + a ⟨i + 1, by omega⟩) :
    ((restrictedSignedSumset h (orderedFinset a)).card : ℤ) ≥
      ((h + 1 : ℕ) : ℤ) ^ 2 + 1
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 7.
Uses 2
Statement usesSet of values of a finite integer sequence · Restricted signed sumset

TheoremRestricted signed sumsets under gap conditions#●ready to prove

Let \(h \ge 3\) and let \(a_1 < a_2 < \dots < a_{h+1}\) be positive integers such that \(a_3 - a_2 < 2a_1\) and \(a_2 - a_1 < 2(a_i - a_{i-1})\) for every \(i\) with \(4 \le i \le h + 1\). Write \(h^{\wedge}_{\pm} A\) for the restricted signed \(h\)-fold sumset of \(A = \{a_1, \dots, a_{h+1}\}\). Then \(|h^{\wedge}_{\pm} A| \ge (h+1)^2 + 1\).

public theorem_wanted card_restrictedSignedSumset_ge_of_gap_conditions
    (h : ℕ) (hh : 3 ≤ h) (a : Fin (h + 1) → ℤ) (ha : StrictMono a)
    (hpos : ∀ i, 0 < a i)
    (hfirst : a ⟨2, by omega⟩ - a ⟨1, by omega⟩ < 2 * a ⟨0, by omega⟩)
    (hgaps : ∀ i : Fin (h - 2),
      a ⟨1, by omega⟩ - a ⟨0, by omega⟩ <
        2 * (a ⟨i + 3, by omega⟩ - a ⟨i + 2, by omega⟩)) :
    ((restrictedSignedSumset h (orderedFinset a)).card : ℤ) ≥
      ((h + 1 : ℕ) : ℤ) ^ 2 + 1
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 8.
Uses 2
Statement usesSet of values of a finite integer sequence · Restricted signed sumset

TheoremLower bound for restricted signed 4-fold sumsets of positive integers#●ready to prove

Let \(k \ge 5\), let \(A\) be a set of \(k\) positive integers, and write \(4^{\wedge}_{\pm} A\) for the restricted signed 4-fold sumset of \(A\). Then \(|4^{\wedge}_{\pm} A| \ge 8k - 15\). Moreover, \(|4^{\wedge}_{\pm} A| = 8k - 15\) if and only if \(A = m \cdot \{1, 3, \dots, 2k - 1\}\), where \(m = \min A\) and \(m \cdot B = \{mb : b \in B\}\).

The source states only that equality forces this form; the converse is included here.

public theorem_wanted card_restrictedSignedSumset_four_ge
    (k : ℕ) (A : Finset ℤ) (hk : 5 ≤ k) (hcard : A.card = k)
    (hpos : ∀ a ∈ A, 0 < a) :
    ((restrictedSignedSumset 4 A).card : ℤ) ≥ 8 * (k : ℤ) - 15 ∧
    (((restrictedSignedSumset 4 A).card : ℤ) = 8 * (k : ℤ) - 15 ↔
      ∃ m ∈ A, (∀ a ∈ A, m ≤ a) ∧ A = scaleFinset m (oddProgression k))
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 9.
Uses 3
Statement usesThe first \(k\) odd positive integers · Restricted signed sumset · Dilation of a finite set of integers

TheoremRestricted signed fourfold sumsets of five positive integers#●ready to prove

Let \(A\) be a set of five positive integers and let \(4^{\wedge}_{\pm} A\) be the restricted signed sumset of \(A\). For an integer \(m\) and a set \(B\) of integers write \(m \cdot B = \{mb : b \in B\}\). Then \(|4^{\wedge}_{\pm} A| \ge 25\), and \(|4^{\wedge}_{\pm} A| = 25\) if and only if \(A = m \cdot \{1, 3, 5, 7, 9\}\) for \(m = \min A\).

The source states the equality case only in the direction that equality forces this form; the converse is included here.

public theorem_wanted card_restrictedSignedSumset_four_five_ge
    (A : Finset ℤ) (hcard : A.card = 5) (hpos : ∀ a ∈ A, 0 < a) :
    ((restrictedSignedSumset 4 A).card : ℤ) ≥ 25 ∧
    (((restrictedSignedSumset 4 A).card : ℤ) = 25 ↔
      ∃ m ∈ A, (∀ a ∈ A, m ≤ a) ∧ A = scaleFinset m (oddProgression 5))
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 10.
Uses 3
Statement usesThe first \(k\) odd positive integers · Restricted signed sumset · Dilation of a finite set of integers

TheoremLower bound for restricted signed 4-fold sumsets of nonnegative sets containing zero#●ready to prove

Let \(k \ge 5\), let \(A\) be a set of \(k\) nonnegative integers with \(0 \in A\), and write \(4^{\wedge}_{\pm} A\) for the restricted signed 4-fold sumset of \(A\). Then \(|4^{\wedge}_{\pm} A| \ge 8k - 19\).

The inverse statement of the source, that equality forces \(A = d \cdot \{0, 1, \dots, k - 1\}\) for some integer \(d\) (where \(d \cdot B = \{db : b \in B\}\)), is omitted: \(A = \{0, 1, 2, 4, 6\}\) has \(|4^{\wedge}_{\pm} A| = 21 = 8 \cdot 5 - 19\) but is not of that form.

public theorem_wanted card_restrictedSignedSumset_four_nonnegative_ge
    (k : ℕ) (A : Finset ℤ) (hk : 5 ≤ k) (hcard : A.card = k)
    (hnonneg : ∀ a ∈ A, 0 ≤ a) (hzero : 0 ∈ A) :
    ((restrictedSignedSumset 4 A).card : ℤ) ≥ 8 * (k : ℤ) - 19
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Theorem 11.
Uses 1
Statement usesRestricted signed sumset

TheoremExtending a restricted signed sumset bound from the first \(h+1\) elements#●ready to prove

Let \(h \ge 3\) and \(k \ge h + 1\), let \(a_1 < a_2 < \dots < a_k\) be positive integers, and let \(t \ge 0\) be an integer. Put \(A = \{a_1, \dots, a_k\}\) and \(A_{h+1} = \{a_1, \dots, a_{h+1}\}\), and write \(h^{\wedge}_{\pm} B\) for the restricted signed \(h\)-fold sumset of a finite set \(B\). If \(|h^{\wedge}_{\pm} A_{h+1}| \ge (h+1)^2 + t\), then \(|h^{\wedge}_{\pm} A| \ge 2hk - h^2 + 1 + t\).

public theorem_wanted card_restrictedSignedSumset_ge_of_initialSegment
    (h k : ℕ) (hh : 3 ≤ h) (hk : h ≤ k - 1) (a : Fin k → ℤ) (t : ℤ)
    (ha : StrictMono a) (hpos : ∀ i, 0 < a i) (ht : 0 ≤ t)
    (hinitial : ((restrictedSignedSumset h (initialSegment a (h + 1))).card : ℤ) ≥
      ((h + 1 : ℕ) : ℤ) ^ 2 + t) :
    ((restrictedSignedSumset h (orderedFinset a)).card : ℤ) ≥
      2 * (h : ℤ) * k - (h : ℤ) ^ 2 + 1 + t
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Lemma 1.
Uses 3
Statement usesInitial segment of a finite integer sequence · Set of values of a finite integer sequence · Restricted signed sumset

TheoremRestricted signed 4-fold sumsets when exactly one gap differs from twice the minimum#●ready to prove

Let \(a_1 < a_2 < a_3 < a_4 < a_5\) be integers with \(a_1 > 0\), let \(A = \{a_1, \dots, a_5\}\), and write \(4^{\wedge}_{\pm} A\) for the restricted signed 4-fold sumset of \(A\). If exactly one of the four gaps \(a_{i+1} - a_i\) with \(i \in \{1, 2, 3, 4\}\) differs from \(2a_1\), then \(|4^{\wedge}_{\pm} A| \ge 26\).

public theorem_wanted card_restrictedSignedSumset_four_ge_of_one_exceptional_gap
    (a : Fin 5 → ℤ) (ha : StrictMono a) (hpos : 0 < a 0)
    (hgaps : (Finset.univ.filter fun i : Fin 4 =>
      a i.succ - a i.castSucc ≠ 2 * a 0).card = 1) :
    ((restrictedSignedSumset 4 (orderedFinset a)).card : ℤ) ≥ 26
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Lemma 3.
Uses 2
Statement usesSet of values of a finite integer sequence · Restricted signed sumset

TheoremRestricted signed fourfold sumsets when exactly two gaps differ from twice the least element#●ready to prove

Restricted signed fourfold sumsets when exactly two gaps differ from twice the least element. Let \(a_1 < a_2 < a_3 < a_4 < a_5\) be integers with \(a_1 > 0\), let \(A = \{a_1, \ldots, a_5\}\) and let \(4^{\wedge}_{\pm} A\) be the restricted signed sumset of \(A\). If exactly two of the four gaps \(a_{i+1} - a_i\) (\(1 \le i \le 4\)) differ from \(2a_1\), then \(|4^{\wedge}_{\pm} A| \ge 26\).

public theorem_wanted card_restrictedSignedSumset_four_ge_of_two_exceptional_gaps
    (a : Fin 5 → ℤ) (ha : StrictMono a) (hpos : 0 < a 0)
    (hgaps : (Finset.univ.filter fun i : Fin 4 =>
      a i.succ - a i.castSucc ≠ 2 * a 0).card = 2) :
    ((restrictedSignedSumset 4 (orderedFinset a)).card : ℤ) ≥ 26
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Lemma 4.
Uses 2
Statement usesSet of values of a finite integer sequence · Restricted signed sumset

TheoremRestricted signed fourfold sumsets when exactly one gap equals twice the least element#●ready to prove

Let \(a_1 < a_2 < a_3 < a_4 < a_5\) be integers with \(a_1 > 0\), let \(A = \{a_1, \ldots, a_5\}\) and let \(4^{\wedge}_{\pm} A\) be the restricted signed sumset of \(A\). If exactly one of the four gaps \(a_{i+1} - a_i\) (\(1 \le i \le 4\)) equals \(2a_1\), then \(|4^{\wedge}_{\pm} A| \ge 26\).

public theorem_wanted card_restrictedSignedSumset_four_ge_of_one_regular_gap
    (a : Fin 5 → ℤ) (ha : StrictMono a) (hpos : 0 < a 0)
    (hgaps : (Finset.univ.filter fun i : Fin 4 =>
      a i.succ - a i.castSucc = 2 * a 0).card = 1) :
    ((restrictedSignedSumset 4 (orderedFinset a)).card : ℤ) ≥ 26
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Lemma 5.
Uses 2
Statement usesSet of values of a finite integer sequence · Restricted signed sumset

TheoremRestricted signed fourfold sumsets when no gap equals twice the least element and the first and third gaps differ#●ready to prove

Restricted signed fourfold sumsets when no gap equals twice the least element and the first and third gaps differ. Let \(a_1 < a_2 < a_3 < a_4 < a_5\) be integers with \(a_1 > 0\), let \(A = \{a_1, \ldots, a_5\}\) and let \(4^{\wedge}_{\pm} A\) be the restricted signed sumset of \(A\). If none of the four gaps \(a_{i+1} - a_i\) (\(1 \le i \le 4\)) equals \(2a_1\) and \(a_4 - a_3 \ne a_2 - a_1\), then \(|4^{\wedge}_{\pm} A| \ge 26\).

public theorem_wanted card_restrictedSignedSumset_four_ge_of_unequal_outer_gaps
    (a : Fin 5 → ℤ) (ha : StrictMono a) (hpos : 0 < a 0)
    (hnone : ∀ i : Fin 4, a i.succ - a i.castSucc ≠ 2 * a 0)
    (hneq : a 3 - a 2 ≠ a 1 - a 0) :
    ((restrictedSignedSumset 4 (orderedFinset a)).card : ℤ) ≥ 26
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Lemma 6.
Uses 2
Statement usesSet of values of a finite integer sequence · Restricted signed sumset

TheoremRestricted signed fourfold sumsets when no gap equals twice the least element, the first and third gaps agree, and the last two gaps do not sum to twice the least element#●ready to prove

Restricted signed fourfold sumsets when no gap equals twice the least element, the first and third gaps agree, and the last two gaps do not sum to twice the least element. Let \(a_1 < a_2 < a_3 < a_4 < a_5\) be integers with \(a_1 > 0\), let \(A = \{a_1, \ldots, a_5\}\) and let \(4^{\wedge}_{\pm} A\) be the restricted signed sumset of \(A\). If none of the four gaps \(a_{i+1} - a_i\) (\(1 \le i \le 4\)) equals \(2a_1\), \(a_4 - a_3 = a_2 - a_1\) and \(a_5 - a_3 \ne 2a_1\), then \(|4^{\wedge}_{\pm} A| \ge 26\).

public theorem_wanted card_restrictedSignedSumset_four_ge_of_equal_outer_gaps_ne
    (a : Fin 5 → ℤ) (ha : StrictMono a) (hpos : 0 < a 0)
    (hnone : ∀ i : Fin 4, a i.succ - a i.castSucc ≠ 2 * a 0)
    (heq : a 3 - a 2 = a 1 - a 0) (hneq : a 4 - a 2 ≠ 2 * a 0) :
    ((restrictedSignedSumset 4 (orderedFinset a)).card : ℤ) ≥ 26
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Lemma 7.
Uses 2
Statement usesSet of values of a finite integer sequence · Restricted signed sumset

TheoremRestricted signed fourfold sumsets when no gap equals twice the least element, the first and third gaps agree, and the last two gaps sum to twice the least element#●ready to prove

Restricted signed fourfold sumsets when no gap equals twice the least element, the first and third gaps agree, and the last two gaps sum to twice the least element. Let \(a_1 < a_2 < a_3 < a_4 < a_5\) be integers with \(a_1 > 0\), let \(A = \{a_1, \ldots, a_5\}\) and let \(4^{\wedge}_{\pm} A\) be the restricted signed sumset of \(A\). If none of the four gaps \(a_{i+1} - a_i\) (\(1 \le i \le 4\)) equals \(2a_1\), \(a_4 - a_3 = a_2 - a_1\) and \(a_5 - a_3 = 2a_1\), then \(|4^{\wedge}_{\pm} A| \ge 26\).

public theorem_wanted card_restrictedSignedSumset_four_ge_of_equal_outer_gaps_eq
    (a : Fin 5 → ℤ) (ha : StrictMono a) (hpos : 0 < a 0)
    (hnone : ∀ i : Fin 4, a i.succ - a i.castSucc ≠ 2 * a 0)
    (heq : a 3 - a 2 = a 1 - a 0) (hsum : a 4 - a 2 = 2 * a 0) :
    ((restrictedSignedSumset 4 (orderedFinset a)).card : ℤ) ≥ 26
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Lemma 8.
Uses 2
Statement usesSet of values of a finite integer sequence · Restricted signed sumset

TheoremRestricted signed 4-fold sumsets when no gap equals twice the minimum#●ready to prove

Let \(a_1 < a_2 < a_3 < a_4 < a_5\) be integers with \(a_1 > 0\), let \(A = \{a_1, \dots, a_5\}\), and write \(4^{\wedge}_{\pm} A\) for the restricted signed 4-fold sumset of \(A\). If \(a_{i+1} - a_i \ne 2a_1\) for every \(i \in \{1, 2, 3, 4\}\), then \(|4^{\wedge}_{\pm} A| \ge 26\).

public theorem_wanted card_restrictedSignedSumset_four_ge_of_no_regular_gap
    (a : Fin 5 → ℤ) (ha : StrictMono a) (hpos : 0 < a 0)
    (hnone : ∀ i : Fin 4, a i.succ - a i.castSucc ≠ 2 * a 0) :
    ((restrictedSignedSumset 4 (orderedFinset a)).card : ℤ) ≥ 26
Sources
  • Mohan, Raj Kumar Mistri, Ram Krishna Pandey, Some Direct and Inverse Problems for the Restricted Signed Sumset in the Set of Integers, INTEGERS 24 (2024), Article A81, Lemma 9.
Uses 2
Statement usesSet of values of a finite integer sequence · Restricted signed sumset
15 fully proved20 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.