Part of: The odd primes in order, the mod-4 digit each contributes, the constant they define, and the Chebyshev race sum.
The prime race constant \varrho is the sum of the series
\varrho \;=\; \sum_{k \ge 0} \frac{b_k}{2^{\,k+1}} \;=\; 0.7004001\ldots,
which converges absolutely by comparison with the geometric series. Since each b_k is
0 or 1, the series is exactly the place-value reading of the binary numeral
0.b_0 b_1 b_2 \ldots_2 — and these are genuinely the binary digits of \varrho:
infinitely many b_k are 0 (Dirichlet's theorem), so the digit string is not
eventually all 1s and no carry ambiguity arises. Reading successive digit prefixes as
binary integers recovers the OEIS sequence A362583, which is why we call \varrho the
A362583 constant. The theorem of this blueprint is that \varrho is irrational.
Lean code for Definition ϱ
-
⟲
def ϱ : ℝ
Real : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.def ϱ : ℝ
Real : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.
⟲:= ∑' kℕ : ℕ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.
, (bitA362583.bit (k : ℕ) : ℕ`k`-th bit of the constant: `1` iff the `k`-th odd prime is `≡ 3 (mod 4)`.
The `b_{k+1}` of the 1-based bit sequence; first values `1 0 1 1 0 0 1 1`
(primes `3, 5, 7, 11, 13, 17, 19, 23`). kℕ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) / 2ℝ ^ (kℕ + 1ℕ)