erdos-69

$\displaystyle \sum_{n=0}^{\infty}\frac{\uparrow\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{\uparrow p}-1}$

The series of ω(n)/2^n over all n ≥ 0, with ω(n) the number of distinct prime factors of n, equals the sum over primes p of 1/(2^p − 1). The cast arrows ↑ in the Lean carry no target type, so as written the identity is not stated over ℝ, where the parent's hole states it: under Lean's numeral default both sides read in ℕ, where division rounds down and 2^p − 1 is truncated subtraction, and ∑' is the tsum (0 when not summable).

$\displaystyle \sum_{n=0}^{\infty}\frac{\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{p}-1}$

The series of ω(n)/2^n over all n ≥ 0, with ω(n) the number of distinct prime factors of n (so ω(0) = ω(1) = 0), equals the sum over primes p of 1/(2^p − 1), both sides in ℝ. Every series is Mathlib's tsum over ℝ, which is 0 when the family is not summable.

$\displaystyle \Bigl(\sum_{n=0}^{\infty}\frac{\uparrow\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{\uparrow p}-1}\Bigr) \;\Rightarrow\; \sum_{p\ \text{prime}}\frac{1}{2^{p}-1}\notin\mathbb{Q}$

If the series of ω(n)/2^n equals the sum over primes of 1/(2^p − 1), then that prime sum, taken in ℝ, is irrational. In the hypothesis the cast arrows ↑ carry no target type, so as written it is not the identity over ℝ that the parent's hole states: under Lean's numeral default both of its sides read in ℕ, where division rounds down and 2^p − 1 is truncated subtraction; only the conclusion, being Irrational, is over ℝ (∑' is the tsum, 0 when not summable).

$\displaystyle \Bigl(\sum_{n=0}^{\infty}\frac{\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{p}-1}\Bigr) \;\Rightarrow\; \sum_{p\ \text{prime}}\frac{1}{2^{p}-1}\notin\mathbb{Q}$

If the series of ω(n)/2^n over n ≥ 0 equals the sum over primes p of 1/(2^p − 1), then that prime sum is irrational, everything in ℝ with ω(n) the number of distinct prime factors of n. Every series is Mathlib's tsum over ℝ, which is 0 when the family is not summable, and Irrational x means x is not the cast of a rational.

$\displaystyle \Bigl(\sum_{n=0}^{\infty}\frac{\uparrow\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{\uparrow p}-1}\Bigr) \Rightarrow \forall b\in\mathbb{N},\ b>0\ \ \exists N\in\mathbb{N}\ \ \forall z\in\mathbb{Z}:\ \uparrow b\cdot\sum_{j=0}^{\infty}\frac{\uparrow\omega(N+1+j)}{2^{j+1}} \ne \uparrow z$

If the series of ω(n)/2^n equals the sum over primes of 1/(2^p − 1), then for every b ≥ 1 there is an N such that b times the tail ∑_{j≥0} ω(N+1+j)/2^{j+1} is no integer z. Every cast arrow ↑ in the Lean carries no target type, so as written neither the hypothesis nor the tail is stated over ℝ, where the parent's hole states them: their domain is whatever Lean's defaults assign (ℕ for a bare numeral, where division rounds down and 2^p − 1 is truncated subtraction), and ∑' is the tsum (0 when not summable).

$\displaystyle \Bigl(\sum_{n=0}^{\infty}\frac{\omega(n)}{2^{n}} = \sum_{p\ \text{prime}}\frac{1}{2^{p}-1}\Bigr) \Rightarrow \forall b\in\mathbb{N},\ b>0\ \ \exists N\in\mathbb{N}\ \ \forall z\in\mathbb{Z}:\ b\cdot\sum_{j=0}^{\infty}\frac{\omega(N+1+j)}{2^{j+1}} \ne z$

If the series of ω(n)/2^n over n ≥ 0 equals the sum over primes p of 1/(2^p − 1), then for every positive natural b there is a natural N such that b times the rescaled tail ∑_{j≥0} ω(N+1+j)/2^{j+1} is not an integer, everything in ℝ with ω(n) the number of distinct prime factors of n. Every series is Mathlib's tsum over ℝ, which is 0 when the family is not summable.

$\displaystyle \forall N,k\in\mathbb{N}:\quad \sum_{j=0}^{\infty}\frac{\omega(N+1+j)}{2^{j+1}} = \sum_{j=0}^{k-1}\frac{\omega(N+1+j)}{2^{j+1}} + \frac{1}{2^{k}}\sum_{j=0}^{\infty}\frac{\omega(N+k+1+j)}{2^{j+1}}$

Under the hypothesis that the Lambert identity ∑_{n≥0} ω(n)/2^n = ∑_p 1/(2^p − 1) holds, the rescaled tail T(N) equals its first k terms plus T(N+k)/2^k, for all naturals N and k. Here T(M) denotes the rescaled tail ∑_{j≥0} ω(M+1+j)/2^{j+1}, a tsum over ℝ (0 if not summable), and ω(n) is the number of distinct prime factors of n.

$\displaystyle \forall M\in\mathbb{N}:\quad 0 < \sum_{j=0}^{\infty}\frac{\omega(M+1+j)}{2^{j+1}}$

Under the hypotheses that the Lambert identity ∑_{n≥0} ω(n)/2^n = ∑_p 1/(2^p − 1) holds and that every rescaled tail splits as T(N) = ∑_{j<k} ω(N+1+j)/2^{j+1} + T(N+k)/2^k, the tail T(M) is strictly positive for every natural M. Here T(M) denotes the rescaled tail ∑_{j≥0} ω(M+1+j)/2^{j+1}, a tsum over ℝ (0 if not summable), and ω(n) is the number of distinct prime factors of n.

$\displaystyle \forall M\in\mathbb{N}:\quad \sum_{j=0}^{\infty}\frac{\omega(M+1+j)}{2^{j+1}} \le \log_{2}(M+1) + 1$

Under the hypotheses that the Lambert identity ∑_{n≥0} ω(n)/2^n = ∑_p 1/(2^p − 1) holds, that every rescaled tail splits as T(N) = ∑_{j<k} ω(N+1+j)/2^{j+1} + T(N+k)/2^k, and that every T(M) is positive, the tail T(M) is at most log₂(M+1) + 1 for every natural M, with log₂ Mathlib's Real.logb 2. Here T(M) denotes the rescaled tail ∑_{j≥0} ω(M+1+j)/2^{j+1}, a tsum over ℝ (0 if not summable), and ω(n) is the number of distinct prime factors of n.

$\displaystyle \forall b\in\mathbb{N},\ b>0\ \ \exists N,k\in\mathbb{N}:\quad \Bigl(b\sum_{j=0}^{k-1}\omega(N+1+j)\,2^{\,k-1-j}\Bigr)\bmod 2^{k} \;+\; b\bigl(\log_{2}(N+k+1)+1\bigr) < 2^{k}$

Under the hypotheses that the Lambert identity ∑_{n≥0} ω(n)/2^n = ∑_p 1/(2^p − 1) holds, that every rescaled tail splits as T(N) = ∑_{j<k} ω(N+1+j)/2^{j+1} + T(N+k)/2^k, that every T(M) is positive, and that T(M) ≤ log₂(M+1) + 1 for every M, for every positive natural b there are naturals N and k such that the residue mod 2^k of the integer b·∑_{j<k} ω(N+1+j)·2^{k−1−j}, plus b(log₂(N+k+1) + 1), is less than 2^k. The sum, the product and the residue are computed in ℕ (with k − 1 − j truncated subtraction, which is 0 when k = 0) and then cast to ℝ, where log₂ is Real.logb 2; here T(M) denotes the rescaled tail ∑_{j≥0} ω(M+1+j)/2^{j+1}, a tsum over ℝ (0 if not summable), and ω(n) is the number of distinct prime factors of n.

$\displaystyle \forall n\in\mathbb{N},\ C\in\mathbb{R}:\quad \Bigl(\forall k\in\mathbb{N},\ \omega(n+1+k) \le C\,(k+1)\Bigr) \Rightarrow \sum_{j=0}^{\infty}\frac{\omega(n+1+j)}{2^{j+1}} \le 2C$

If, for a natural n and a real C, ω(n+1+k) ≤ C(k+1) for every natural k, then the tail ∑_{j≥0} ω(n+1+j)/2^{j+1} is at most 2C, with ω(n) the number of distinct prime factors of n. Every series is Mathlib's tsum over ℝ, which is 0 when the family is not summable.

$\displaystyle \sum_{p\ \text{prime}}\frac{1}{2^{p}-1} < \infty$

The family p ↦ 1/(2^p − 1), indexed by the primes and valued in ℝ, is summable in Mathlib's sense (unconditionally; for a nonnegative real family this is ordinary convergence).

$\displaystyle \exists C\ge 0\ \ \forall x\in\mathbb{N},\ x\ge 2:\quad \Bigl\lvert \sum_{p\le x,\ p\ \text{prime}}\frac{1}{p} - \log\log x \Bigr\rvert \le C$

There is a nonnegative real C such that for every natural x ≥ 2 the sum of 1/p over the primes p ≤ x differs from log log x by at most C, with log the natural logarithm (Mathlib's Real.log) and the primes p ≤ x the finset Nat.primesLE x.

$\displaystyle \forall k\in\mathbb{N},\ \forall c:\mathbb{N}\to\mathbb{N}\ \ \exists N\in\mathbb{N}\ \ \forall j<k:\quad c(j) \le \omega(N+1+j)$

For every length k and every sequence of naturals c there is a natural N with c(j) ≤ ω(N+1+j) for each j < k, where ω(n) is the number of distinct prime factors of n.

$\displaystyle \frac{1}{T}\sum_{t=0}^{T-1}\Bigl\lvert q\,D_a(b+Qt) - \operatorname{round}\bigl(q\,D_a(b+Qt)\bigr)\Bigr\rvert \le q\sum_{p\mid a}\Bigl(\frac{1}{p}+\frac{1}{T}\Bigr),\qquad D_a(m) = \sum_{k=0}^{\infty}\frac{\omega\bigl(a(m+k+1)\bigr)}{2^{k+1}}$

For naturals q and an integer z with q·∑_{n≥0} ω(n)/2^n = z, and for naturals a, Q, b, T with a ≠ 0, T > 0 and every prime factor p of a coprime to Q, the average over t < T of the distance from q·D_a(b+Qt) to its nearest integer is at most q times the sum over the prime factors p of a of 1/p + 1/T. Everything is in ℝ: ω(n) is the number of distinct prime factors of n, round is Mathlib's rounding (half rounds up), the sum over p ∣ a runs over a.primeFactors, and each series is a tsum (0 when not summable).

$\displaystyle \forall a,m\in\mathbb{N},\ a\ne 0:\quad \sum_{k=0}^{\infty}\frac{\omega\bigl(a(m+k+1)\bigr)}{2^{k+1}} = \sum_{k=0}^{\infty}\frac{\omega(m+k+1)}{2^{k+1}} + \omega(a) - \sum_{p\mid a}\frac{2^{\,m \bmod p}}{2^{p}-1}$

For a nonzero natural a and any natural m, the tail of ω along the multiples a(m+k+1) equals the undilated tail plus ω(a) minus, for each prime factor p of a, 2^{m mod p}/(2^p − 1), all in ℝ, with ω(n) the number of distinct prime factors of n and the last sum over a.primeFactors. Every series is Mathlib's tsum over ℝ, which is 0 when the family is not summable.

$\displaystyle \exists p>0,\ N_0\ \ \forall n,n'\ge N_0,\ n\equiv n' \pmod p\ \ \exists z\in\mathbb{Z}:\quad \sum_{j=0}^{\infty}\frac{f(n+1+j)}{2^{j+1}} - \sum_{j=0}^{\infty}\frac{f(n'+1+j)}{2^{j+1}} = z$

For every f : ℕ → ℕ and rational q, if the family f(n)/2^n is summable in ℝ and q equals its sum ∑_{n≥0} f(n)/2^n, then there are a positive natural p and a natural N₀ such that any two tails taken from n, n' ≥ N₀ with n ≡ n' (mod p) differ by an integer. The tails are tsums over ℝ (0 when not summable); the hypotheses are the "if" part and the display is the conclusion.

$\displaystyle \forall P,j\in\mathbb{N},\ 2\le P,\ j\le P:\quad \sum_{p\mid 1+P\#\,(1+j)}\frac{1}{p} \le \frac{5}{\log P}$

For naturals P ≥ 2 and j ≤ P, the sum of 1/p over the prime factors p of 1 + P#·(1+j) is at most 5/log P, where P# is the primorial (the product of the primes at most P), the sum runs over (…).primeFactors, and log is the natural logarithm, all in ℝ.

$\displaystyle \sum_{n=0}^{\infty}\bigl[n\ \text{prime}\bigr]\Bigl(\frac{1}{2}\Bigr)^{n} \notin\mathbb{Q}$

The real number whose binary expansion has a 1 in place n exactly when n is prime, the sum over n ≥ 0 of (1/2)^n for prime n and 0 otherwise, is irrational. The series is a tsum over ℝ (0 when not summable), and Irrational x means x is not the cast of a rational.

$\displaystyle \forall m\in\mathbb{N},\ m\ge 1:\quad \sum_{n=0}^{\infty}\bigl[\omega(n)=m\bigr]\Bigl(\frac{1}{2}\Bigr)^{n} \notin\mathbb{Q}$

For every natural m ≥ 1, the real number with a binary 1 in place n exactly when n has m distinct prime factors, the sum over n ≥ 0 of (1/2)^n when ω(n) = m and 0 otherwise, is irrational. The series is a tsum over ℝ (0 when not summable), and Irrational x means x is not the cast of a rational.

$\displaystyle \sum_{n=0}^{\infty}\frac{\omega(n)}{n!} \notin\mathbb{Q}$

The sum over n ≥ 0 of ω(n)/n!, with ω(n) the number of distinct prime factors of n (so the n = 0 and n = 1 terms vanish), is irrational in ℝ. Every series is Mathlib's tsum over ℝ, which is 0 when the family is not summable, and Irrational x means x is not the cast of a rational.

$\displaystyle \forall b\in\mathbb{N},\ b\ge 2:\quad \sum_{p\ \text{prime}}\frac{1}{b^{p}} \notin\mathbb{Q}$

For every natural base b ≥ 2, the sum over the primes p of 1/b^p, in ℝ, is irrational. The series is a tsum over ℝ (0 when not summable), and Irrational x means x is not the cast of a rational.