Digit recursion for weighted sums of a completely multiplicative function

Let χ : ℕ → ℤ be completely multiplicative, periodic modulo q on the residues 1, …, q - 1, with χ q = s and ∑_{n=1}^{q-1} χ n = 0, and let S m = ∑_{n=1}^{m} n χ(n). Then S satisfies a recursion along the base-q digits, so zeros of S propagate digit by digit. The file also proves the complete-sequence (subset-sum) lemma and a version for pairs.

The declaration names are those cited by the paper and its blueprint (namespace SegmentoII).

Main results

• SegmentoII.digit_recursion: S (q k + r) = s q S k + k (T_q + q C r) + T r for r < q.
• SegmentoII.zero_step, SegmentoII.zeros_from_digits: if every base-q digit of m lies in the digit set R = {r < q | T_q + q C r = 0 ∧ T r = 0}, then S m = 0.
• SegmentoII.complete_list, SegmentoII.complete_range: if each term is at most 1 plus the sum of the earlier ones, every integer up to the total is a subset sum.
• SegmentoII.pairs_subset_sum: the version with an odd extra term q₀ and pairs (u j, u j + 2 d j).

References

• C. Marín, Zeros of weighted partial sums of completely multiplicative functions: Dirichlet characters, the Euler factor at 2 and Conrey's sine series, Zenodo (2026), doi:10.5281/zenodo.22847374.

def SegmentoII.S (χ : ℕ → ℤ) (m : ℕ) : ℤ

S m = ∑_{n=1}^{m} n χ(n).

Equations

• SegmentoII.S χ m = ∑ n ∈ Finset.Icc 1 m, ↑n * χ n

def SegmentoII.C (χ : ℕ → ℤ) (r : ℕ) : ℤ

C r = ∑_{n=1}^{r} χ(n).

Equations

• SegmentoII.C χ r = ∑ n ∈ Finset.Icc 1 r, χ n

def SegmentoII.T (χ : ℕ → ℤ) (r : ℕ) : ℤ

T r = ∑_{n=1}^{r} n χ(n) (same as S; used for r < q).

Equations

• SegmentoII.T χ r = ∑ n ∈ Finset.Icc 1 r, ↑n * χ n

def SegmentoII.Tq (χ : ℕ → ℤ) (q : ℕ) : ℤ

Tq = T (q-1).

Equations

• SegmentoII.Tq χ q = SegmentoII.T χ (q - 1)

theorem SegmentoII.S_zero (χ : ℕ → ℤ) : S χ 0 = 0

theorem SegmentoII.T_zero (χ : ℕ → ℤ) : T χ 0 = 0

theorem SegmentoII.C_zero (χ : ℕ → ℤ) : C χ 0 = 0

theorem SegmentoII.S_succ (χ : ℕ → ℤ) (n : ℕ) : S χ (n + 1) = S χ n + (↑n + 1) * χ (n + 1)

theorem SegmentoII.T_succ (χ : ℕ → ℤ) (n : ℕ) : T χ (n + 1) = T χ n + (↑n + 1) * χ (n + 1)

theorem SegmentoII.C_succ (χ : ℕ → ℤ) (n : ℕ) : C χ (n + 1) = C χ n + χ (n + 1)

theorem SegmentoII.digit_recursion (q : ℕ) (hq : 2 ≤ q) (χ : ℕ → ℤ) (s : ℤ) (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < q → χ (j * q + r) = χ r) (hs : χ q = s) (hsum0 : C χ (q - 1) = 0) (k r : ℕ) (hr : r < q) : S χ (q * k + r) = s * ↑q * S χ k + ↑k * (Tq χ q + ↑q * C χ r) + T χ r

Theorem 1 (digit recursion). For r < q: S (q*k + r) = s*q*S k + k*(Tq + q*C r) + T r.

def SegmentoII.InR (χ : ℕ → ℤ) (q r : ℕ) : Prop

The digit set R = {r | r < q ∧ Tq + q*C r = 0 ∧ T r = 0}.

Equations

• SegmentoII.InR χ q r = (r < q ∧ SegmentoII.Tq χ q + ↑q * SegmentoII.C χ r = 0 ∧ SegmentoII.T χ r = 0)

theorem SegmentoII.zero_step (q : ℕ) (hq : 2 ≤ q) (χ : ℕ → ℤ) (s : ℤ) (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < q → χ (j * q + r) = χ r) (hs : χ q = s) (hsum0 : C χ (q - 1) = 0) (k r : ℕ) (hk : S χ k = 0) (hR : InR χ q r) : S χ (q * k + r) = 0

Theorem 2 (zeros from digits), one step.

theorem SegmentoII.zeros_from_digits (q : ℕ) (hq : 2 ≤ q) (χ : ℕ → ℤ) (s : ℤ) (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < q → χ (j * q + r) = χ r) (hs : χ q = s) (hsum0 : C χ (q - 1) = 0) (m : ℕ) (hm : ∀ d ∈ q.digits m, InR χ q d) : S χ m = 0

Theorem 2 (zeros from digits), corollary. If every base-q digit of m lies in R, then S m = 0.

theorem SegmentoII.complete_list (d : List ℕ) (hd : ∀ (l₁ : List ℕ) (a : ℕ) (l₂ : List ℕ), d = l₁ ++ a :: l₂ → a ≤ 1 + l₁.sum) (x : ℕ) : x ≤ d.sum → ∃ (l : List ℕ), l.Sublist d ∧ l.sum = x

Theorem 3 (complete sequence), list form. If each entry is at most 1 + the sum of the earlier entries, every x ≤ d.sum is the sum of a sublist of d. (The hypothesis "every entry ≥ 1" is not needed and has been dropped.)

theorem SegmentoII.complete_range (d : ℕ → ℕ) (t : ℕ) (hd : ∀ j < t, d j ≤ 1 + ∑ i ∈ Finset.range j, d i) (y : ℕ) : y ≤ ∑ i ∈ Finset.range t, d i → ∃ A ⊆ Finset.range t, ∑ i ∈ A, d i = y

Theorem 3 (complete sequence), indexed form (d j, j < t, subsets of range t).

theorem SegmentoII.choice_sum (t : ℕ) (d u v : ℕ → ℕ) (hv : ∀ (j : ℕ), v j = u j + 2 * d j) (A : Finset ℕ) (hA : A ⊆ Finset.range t) : (∑ j ∈ Finset.range t, if j ∈ A then v j else u j) = ∑ j ∈ Finset.range t, u j + 2 * ∑ j ∈ A, d j

Choosing v j on A and u j off A adds 2 * ∑_A d to U = ∑ u.

theorem SegmentoII.pairs_subset_sum (t : ℕ) (d u v : ℕ → ℕ) (q0 : ℕ) (hq0 : Odd q0) (hv : ∀ (j : ℕ), v j = u j + 2 * d j) (hd : ∀ j < t, d j ≤ 1 + ∑ i ∈ Finset.range j, d i) (x : ℕ) (hx1 : ∑ j ∈ Finset.range t, u j + q0 - 1 ≤ x) (hx2 : x ≤ ∑ j ∈ Finset.range t, u j + 2 * ∑ j ∈ Finset.range t, d j + 1) : ∃ (b : Bool), ∃ A ⊆ Finset.range t, x = (if b = true then q0 else 0) + ∑ j ∈ Finset.range t, if j ∈ A then v j else u j

Theorem 3, pairs version. Pairs (u j, v j) with v j = u j + 2 d j, d complete, q0 odd, U = ∑ u, H = ∑ d. Every x ∈ [U + q0 - 1, U + 2H + 1] is a sum of a selection: optionally q0, plus one element from each pair (v j for j ∈ A, u j otherwise). (For distinct q0, u j, v j this is a subset sum of {q0, u j, v j}; the hypothesis q0 ≤ 2H + 1 is not needed and has been dropped.)