Davenport constant of \(\mathbb{Z}_p\) with \(k\)-th power unit weights is at most \(k\) to Weighted zero-sum free pairs for \(k\)-th power weights modulo a prime

TheoremDavenport constant of \(\mathbb{Z}_p\) with \(k\)-th power unit weights is at most \(k\)#●ready to prove

Let \(k\) be an odd prime and \(p\) a prime with \(p \equiv 1 \pmod{k}\) and \(p \not\equiv 1 \pmod{k^2}\). Let \(\mathbb{Z}_p = \mathbb{Z}/p\mathbb{Z}\) and let \(U(p)^k\) be the set of \(k\)-th powers of units of \(\mathbb{Z}_p\). Then every sequence \(x_1, \dots, x_k\) of \(k\) elements of \(\mathbb{Z}_p\) has a \(U(p)^k\)-weighted zero-sum subsequence: there are a nonempty set \(I \subseteq \{1, \dots, k\}\) and weights \(a_i \in U(p)^k\) for \(i \in I\) with \(\sum_{i \in I} a_i x_i = 0\). In other words, \(D_{U(p)^k}(p) \le k\), where \(D_A(p)\) is the least positive \(\ell\) such that every sequence of \(\ell\) elements of \(\mathbb{Z}_p\) has an \(A\)-weighted zero-sum subsequence.

public theorem_wanted davenport_unit_pow_le {k p : ℕ} (hk : k.Prime) (hk2 : k ≠ 2)
    (hp : p.Prime) (hpk : p % k = 1) (hpk2 : p % k ^ 2 ≠ 1) :
    k ∈ davenportSet (ZMod p) (ZMod p) {x : ZMod p | ∃ u : ZMod p, IsUnit u ∧ x = u ^ k}

Sources

Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Theorem 7.5.

TheoremWeighted zero-sum free pairs in a field#●ready to prove

Let \(F\) be a field, let \(A\) be a subgroup of the multiplicative group \(F^*\), and let \(x, y \in F\) be nonzero. Then the sequence \((x_1, x_2) = (x, y)\) has no \(A\)-weighted zero-sum subsequence, that is, there is no nonempty set \(I \subseteq \{1, 2\}\) with elements \(a_i \in A\) for \(i \in I\) such that \(\sum_{i \in I} a_i x_i = 0\), if and only if \(x\) and \(-y\) lie in different cosets of \(A\) in \(F^*\).

A zero term is by itself a zero-sum subsequence, so the cosets are taken for nonzero \(x\) and \(y\).

public theorem_wanted pair_no_weightedZeroSum_iff {F : Type*} [Field F] (A : Subgroup Fˣ)
    {x y : F} (hx : x ≠ 0) (hy : y ≠ 0) :
    (¬ ∃ I : Finset (Fin 2), I.Nonempty ∧ ∃ a : Fin 2 → F,
      (∀ i ∈ I, a i ∈ ((↑) : Fˣ → F) '' A) ∧ ∑ i ∈ I, a i * ![x, y] i = 0) ↔
      (QuotientGroup.mk (Units.mk0 x hx) : Fˣ ⧸ A) ≠
        QuotientGroup.mk (Units.mk0 (-y) (neg_ne_zero.mpr hy))

Sources

Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Lemma 7.6.

TheoremWeighted zero-sum free pairs for a proper subgroup of \(F^\times\)#●ready to prove

Let \(F\) be a field and \(A\) a proper subgroup of the multiplicative group \(F^\times\). Then some sequence \(x_1, x_2\) in \(F\) has no \(A\)-weighted zero-sum subsequence: there is no nonempty \(I \subseteq \{1, 2\}\) with weights \(a_i \in A\) for \(i \in I\) such that \(\sum_{i \in I} a_i x_i = 0\).

Hence the weighted Davenport constant \(D_A(F)\), the least positive \(k\) such that every sequence of length \(k\) in \(F\) has an \(A\)-weighted zero-sum subsequence, is at least \(3\) when it exists.

public theorem_wanted davenport_proper_subgroup_ge_three {F : Type*} [Field F]
    (A : Subgroup Fˣ) (hA : A ≠ ⊤) :
    2 ∉ davenportSet F F (((↑) : Fˣ → F) '' A)

Sources

Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Corollary 7.7.

TheoremWeighted zero-sum free pairs for \(k\)-th power weights modulo a prime#●ready to prove

Let \(k \ge 2\), let \(p\) be a prime with \(p \equiv 1 \pmod k\), and let \(U(p)^k = \{u^k : u \in \mathbb{Z}_p^\times\}\). Then some sequence \(x_1, x_2\) in \(\mathbb{Z}_p\) has no \(U(p)^k\)-weighted zero-sum subsequence: there is no nonempty \(I \subseteq \{1, 2\}\) with weights \(a_i \in U(p)^k\) for \(i \in I\) such that \(\sum_{i \in I} a_i x_i = 0\).

Hence the weighted Davenport constant \(D_{U(p)^k}(p)\), the least positive \(k'\) such that every sequence of length \(k'\) in \(\mathbb{Z}_p\) has a \(U(p)^k\)-weighted zero-sum subsequence, is at least \(3\).

public theorem_wanted davenport_unit_pow_ge_three {k p : ℕ} (hk : 2 ≤ k) (hp : p.Prime)
    (hpk : p % k = 1) :
    2 ∉ davenportSet (ZMod p) (ZMod p) {x : ZMod p | ∃ u : ZMod p, IsUnit u ∧ x = u ^ k}

Sources

Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Corollary 7.8.

4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.