Nat.Primes.not_summable_one_div
theorem Nat.Primes.not_summable_one_div : ¬Summable fun p => 1 / ↑↑p
The theorem `Nat.Primes.not_summable_one_div` states that the sum of the reciprocals of the prime numbers diverges. In other words, there is not a finite number to which the sum of the reciprocals of all prime numbers converges. Here, `1 / ↑↑p` represents the reciprocal of a prime number `p`. The notation `¬Summable` signifies that the sequence is not summable, meaning it doesn't converge to a finite sum.
More concisely: The sum of the reciprocals of the prime numbers diverges, i.e., it is not a convergent series.
|
Nat.Primes.summable_rpow
theorem Nat.Primes.summable_rpow : ∀ {r : ℝ}, (Summable fun p => ↑↑p ^ r) ↔ r < -1
The theorem states that for any real number `r`, the infinite series over the powers of primes `p` raised to the `r` (denoted as `p^r`), converges if and only if `r` is less than `-1`. Here, convergence of a series means that the series has a sum (finite), and primes `p` are considered as natural numbers.
More concisely: The real number series sum of prime powers raised to the power `r` converges if and only if `r` is strictly negative.
|
not_summable_one_div_on_primes
theorem not_summable_one_div_on_primes : ¬Summable ({p | p.Prime}.indicator fun n => 1 / ↑n)
The theorem `not_summable_one_div_on_primes` states that the sum of the reciprocals of all prime numbers does not converge. In mathematical terms, given the set of all prime numbers, taking the reciprocal of each prime and trying to compute the infinite sum of these reciprocals does not result in a finite number. This is analogous to the harmonic series, which also diverges.
More concisely: The infinite sum of the reciprocals of all prime numbers diverges.
|
one_half_le_sum_primes_ge_one_div
theorem one_half_le_sum_primes_ge_one_div :
∀ (k : ℕ), 1 / 2 ≤ ((4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow).sum fun p => 1 / ↑p
This theorem states that for any natural number `k`, the sum of the reciprocals of all prime numbers `p` that lie in the range `k ≤ p ≤ 4^(π(k-1)+1)` (where `π` is the prime-counting function) is at least `1/2`. Here, the prime numbers are considered as real numbers. The sum is calculated over the set difference of the primes below `(4 ^ (k.primesBelow.card + 1)).succ` and the primes below `k`.
More concisely: For any natural number `k`, the sum of reciprocals of primes in the range [`k`, `4^(π(k) + 1)`] is greater than or equal to `1/2`.
|
Nat.roughNumbersUpTo_card_le'
theorem Nat.roughNumbersUpTo_card_le' :
∀ (N k : ℕ), ↑(N.roughNumbersUpTo k).card ≤ ↑N * (N.succ.primesBelow \ k.primesBelow).sum fun p => 1 / ↑p := by
sorry
This theorem states that for any natural numbers `N` and `k`, the cardinality (or size) of the set of `k`-rough numbers less than or equal to `N` is less than or equal to `N` times the sum of reciprocals of the primes between `k` and `N` inclusive. Here, a `k`-rough number is a number that has no prime divisors less than `k`.
More concisely: For any natural numbers N and k, the number of k-rough numbers less than or equal to N does not exceed N times the sum of the reciprocals of primes between k and N.
|