An Arithmetic Sum Associated with the Classical Theta Function

Reference: arxiv/2501.03234 An Arithmetic Sum Associated with the Classical Theta Function by Bruce C. Berndt, Raghavendra N. Bhat, Jeffrey L. Meyer, Likun Xie, Alexandru Zaharescu

def Arxiv.«2501.03234».S' (h k : ℕ) : ℤ

Define the sum $$S'(h, k) := \sum_{j=1}^{k-1}(-1)^{j + 1 + \lfloor \frac{hj}{k}\rfloor}.$$

Equations

• Arxiv.«2501.03234».S' h k = ∑ j ∈ Finset.Ico 1 k, (-1) ^ (j + 1 + ⌊↑h * ↑j / ↑k⌋₊)

def Arxiv.«2501.03234».S (k : ℕ) : ℤ

Define the sum $$S(k) := \sum_{h=1}^{k-1}S'(h, k)$$

Equations

• Arxiv.«2501.03234».S k = ∑ h ∈ Finset.Ico 1 k, Arxiv.«2501.03234».S' h k

theorem Arxiv.«2501.03234».S_fst_10 : List.map S (List.range 10) = [0, 0, 1, 2, 5, 4, 7, 10, 11, 8]

Note that in Table 1 in https://arxiv.org/abs/2501.03234v1, there seems to be an error: 11 appears twice. The first 10 values of $S$.

theorem Arxiv.«2501.03234».conjecture_1_1 (k : ℕ) (hprim : Nat.Prime k) (hodd : Odd k) : 0 < S k

Conjecture 1.1: For any odd prime $k$, the sum associated with the classical theta function $θ_3$, $S(k)$ is positive.

theorem Arxiv.«2501.03234».conjecture_4_1 (k : ℕ) (hprim : Nat.Prime k) (hodd : Odd k) (hgt : k > 5) : ↑k < S k

Conjecture 4.1: For any prime $k$ larger than $5$, $S(k) > k$.

theorem Arxiv.«2501.03234».conjecture_4_2 (k : ℕ) (hprim : Nat.Prime k) (hodd : Odd k) (hgt : k > 233) : 2 * ↑k < S k

Conjecture 4.2: For any prime $k$ larger than $233$, $S(k) > 2k$.

theorem Arxiv.«2501.03234».conjecture_4_3 (k : ℕ) (hprim : Nat.Prime k) (hodd : Odd k) (hgt : k > 3119) : 3 * ↑k < S k

Conjecture 4.3: For any prime $k$ larger than $3119$, $S(k) > 3k$.

theorem Arxiv.«2501.03234».conjecture_4_4 (n : ℕ) : ∀ᶠ (k : ℕ) in Filter.atTop, Nat.Prime k → Odd k → ↑n * ↑k < S k

Conjecture 4.4: Given a natural number $n ∈ ℕ$, for all large enough odd prime $k$ (depending on $n$), $nk < S(k)$.

theorem Arxiv.«2501.03234».conjecture_4_4_def_0 (hc1_1 : ∀ (k : ℕ), Nat.Prime k → Odd k → 0 < S k) : ∀ᶠ (k : ℕ) in Filter.atTop, Nat.Prime k → Odd k → ↑0 * ↑k < S k

Conjecture 1.1 → Conjecture 4.4: If conjecture 1.1 holds true, then this implies a special case of conjecture 4.4 where $n = 0$. In this case the lower bound for the odd prime $k$ would be $0$.

theorem Arxiv.«2501.03234».conjecture_4_4_def_1 (hc4_1 : ∀ (k : ℕ), Nat.Prime k → Odd k → k > 5 → ↑k < S k) : ∀ᶠ (k : ℕ) in Filter.atTop, Nat.Prime k → Odd k → ↑1 * ↑k < S k

Conjecture 4.1 → Conjecture 4.4: If conjecture 4.1 holds true, then this implies a special case of conjecture 4.4 where $n = 1$. In this case the lower bound would be $5$.

theorem Arxiv.«2501.03234».conjecture_4_4_def_2 (hc4_2 : ∀ (k : ℕ), Nat.Prime k → Odd k → k > 233 → 2 * ↑k < S k) : ∀ᶠ (k : ℕ) in Filter.atTop, Nat.Prime k → Odd k → ↑2 * ↑k < S k

Conjecture 4.2 → Conjecture 4.4: If conjecture 4.2 holds true, then this implies a special case of conjecture 4.4 for $n = 2$. For this scenario, the lower bound is now $233$.

theorem Arxiv.«2501.03234».conjecture_4_4_def_3 (hc4_3 : ∀ (k : ℕ), Nat.Prime k → Odd k → k > 3119 → 3 * ↑k < S k) : ∀ᶠ (k : ℕ) in Filter.atTop, Nat.Prime k → Odd k → ↑3 * ↑k < S k

Conjecture 4.3 → Conjecture 4.4: If conjecture 4.3 holds true, then a special case of conjecture 4.4 for $n = 3$ is obtained, and the lower bound is $3119$.