Part of: The odd primes in order, the mod-4 digit each contributes, the constant they define, and the Chebyshev race sum.
DefinitionraceSum
The Chebyshev race sum is the integer
S(N) \;=\; \sum_{\substack{p \le N \\ p \text{ prime}}} \begin{cases} +1 & p \equiv 1 \pmod 4 \\ -1 & p \equiv 3 \pmod 4 \\ \;\;\,0 & p = 2, \end{cases}
i.e. S(N) = \sum_{p \le N} \chi_4(p) — but stated with plain remainder arithmetic rather
than a character, per the statement-hygiene principle. The convention "primes \le N"
matches Mathlib's prime-counting function \pi(N) (Nat.primeCounting), which the race-sum
theorems quantify against.
Lean code for Definition raceSum
-
⟲
def raceSum (N
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : ℤInt : TypeThe integers. This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for `Int` that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).def raceSum (N
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : ℤInt : TypeThe integers. This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for `Int` that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).
⟲:= ∑ pℕ ∈ (Finset.rangeFinset.range (n : ℕ) : Finset ℕ`range n` is the set of natural numbers less than `n`. (Nℕ + 1ℕ)).filterFinset.filter.{u_1} {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : Finset α`Finset.filter p s` is the set of elements of `s` that satisfy `p`.
For example, one can use `s.filter (· ∈ t)` to get the intersection of `s` with `t : Set α`
as a `Finset α` (when a `DecidablePred (· ∈ t)` instance is available). Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number. , raceKernelA362583.raceKernel (n : ℕ) : ℤThe summand of the Chebyshev race sum: `+1` on `n ≡ 1 (mod 4)`, `-1` on
`n ≡ 3 (mod 4)`, `0` otherwise. At a prime `p` this is `χ₄(p)`. pℕ