Nat.primeCounting'_add_le
theorem Nat.primeCounting'_add_le :
∀ {a k : ℕ}, 0 < a → a < k → ∀ (n : ℕ), (k + n).primeCounting' ≤ k.primeCounting' + a.totient * (n / a + 1) := by
sorry
This theorem provides an upper bound on the size of the `primeCounting'` function. Specifically, it states that for any positive number `a` that is less than `k`, and any natural number `n`, the value of `primeCounting'` at `(k + n)` is less than or equal to the sum of `primeCounting'` at `k` and the product of the totient of `a` and the quotient of `n` divided by `a` plus one. In essence, it bounds the growth of the `primeCounting'` function in terms of the totient function and simple arithmetic operations.
More concisely: For any positive number `a` less than `k` and natural number `n`, the value of `primeCounting'(k + n)` is bounded by `primeCounting'(k) + totient(a) * (n / a)`.
|
Nat.primesBelow_card_eq_primeCounting'
theorem Nat.primesBelow_card_eq_primeCounting' : ∀ (n : ℕ), n.primesBelow.card = n.primeCounting'
This theorem states that for every natural number `n`, the cardinality of the finite set `primesBelow n` (which contains all prime numbers less than `n`) is equal to the value of the function `primeCounting'` at `n`. In other words, the number of prime numbers less than `n` is the same whether we count them directly or calculate them using the `primeCounting'` function.
More concisely: For every natural number `n`, the number of primes less than `n` is equal to the value of the function `primeCounting'` at `n`.
|