Core Definitions for the Krafft Sieve

This module establishes the foundational definitions for the sieve:

• $\mathcal{P}_n$: The target set of primes.
• $q$: The primorial $q = \prod_{p \in \mathcal{P}_n} p$.
• $\mathcal{A}_n$: The target interval.
• $g_i, c$: Local and global hit counters.
• $sum1, sum2$: Weighted sums over the interval.

def KrafftSieve.primeWindow (n : ℕ) : Finset ℕ

Definition of the set of primes primeWindow. Let $\mathcal{P}_n$ denote the set of primes $p$ such that $5 \le p < 6n+2$.

Equations

• KrafftSieve.primeWindow n = {p ∈ Finset.range (6 * n + 2) | 5 ≤ p ∧ Nat.Prime p}

def KrafftSieve.q (n : ℕ) : ℕ

Definition of the primorial q. Define the primorial $q = \prod_{p \in \mathcal{P}_n} p$.

Equations

• KrafftSieve.q n = ∏ p ∈ KrafftSieve.primeWindow n, p

def KrafftSieve.w (n : ℕ) : ℕ

Definition of w as the cardinality of primeWindow. Let $w = |\mathcal{P}_n|$ be the number of distinct prime factors of $q$.

Equations

• KrafftSieve.w n = (KrafftSieve.primeWindow n).card

def KrafftSieve.primesList (n : ℕ) : List ℕ

Definition of the sorted list of primes and the accessor function p_i. Index the primes in $\mathcal{P}_n$ as $p_1, p_2, \dots, p_w$.

Equations

• KrafftSieve.primesList n = (KrafftSieve.primeWindow n).sort fun (x1 x2 : ℕ) => x1 ≤ x2

def KrafftSieve.p (n : ℕ) (i : Fin (w n)) : ℕ

Access the $i$-th prime $p_i$. Note that we use 0-based indexing for the implementation, so $p_0$ corresponds to the user's $p_1$.

Equations

• KrafftSieve.p n i = (KrafftSieve.primesList n).get (Fin.cast ⋯ i)

def KrafftSieve.krafftResidue (n : ℕ) (i : Fin (w n)) : ℕ

Define r^K Define the Krafft tuple r^K such that for each 1 <= i <= w, r^K_i = floor((p_i+1)/6).

Equations

• KrafftSieve.krafftResidue n i = (KrafftSieve.p n i + 1) / 6

def KrafftSieve.evalInterval (n : ℕ) : Finset ℕ

Define evalInterval Define the target interval of indices: evalInterval = {x in N | 6n^2 - 2n <= x <= 6n^2 + 10n + 3}.

Equations

• KrafftSieve.evalInterval n = Finset.Icc (6 * n ^ 2 - 2 * n) (6 * n ^ 2 + 10 * n + 3)

noncomputable def KrafftSieve.g (n : ℕ) (i : Fin (w n)) (x : ZMod (q n)) : ℝ

Define the local hit function g_i(x) Define the local hit function $g_i : \mathbb{Z}/q\mathbb{Z} \to \mathbb{R}$ for each prime index $i \in \{1, \dots, w\}$.

• $g_i(x) = 1$ if $x \equiv r^K_i \pmod{p_i}$ or $x \equiv -r^K_i \pmod{p_i}$.
• Otherwise, $g_i(x) = 0$.

Equations

• KrafftSieve.g n i x = if x.cast = ↑(KrafftSieve.krafftResidue n i) ∨ x.cast = -↑(KrafftSieve.krafftResidue n i) then 1 else 0

noncomputable def KrafftSieve.c (n : ℕ) (x : ZMod (q n)) : ℝ

Define the global additive hit counter c(x) Define the global additive hit counter $c : \mathbb{Z}/q\mathbb{Z} \to \mathbb{R}$ as the sum of all local hits: $$ c(x) = \sum_{i=1}^w g_i(x) $$

Equations

• KrafftSieve.c n x = ∑ i : Fin (KrafftSieve.w n), KrafftSieve.g n i x

noncomputable def KrafftSieve.sum1 (n : ℕ) (W : ZMod (q n) → ℝ) : ℝ

Define the total weighted mass of the interval sum1(n, W) Define the total weighted mass of the interval $sum1(n, W)$: $$ sum1(n, W) = \sum_{x \in \mathcal{A}_n} W(x) $$

Equations

• KrafftSieve.sum1 n W = ∑ x ∈ KrafftSieve.evalInterval n, W ↑x

noncomputable def KrafftSieve.sum2 (n : ℕ) (W : ZMod (q n) → ℝ) : ℝ

Define the weighted hit count sum2(n, W) Define the weighted hit count $sum2(n, W)$: $$ sum2(n, W) = \sum_{x \in \mathcal{A}_n} W(x) c(x) $$

Equations

• KrafftSieve.sum2 n W = ∑ x ∈ KrafftSieve.evalInterval n, W ↑x * KrafftSieve.c n ↑x