Nat.exists_prime_lt_and_le_two_mul_eventually
theorem Nat.exists_prime_lt_and_le_two_mul_eventually : ∀ (n : ℕ), 512 ≤ n → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n := by
sorry
This theorem proves Bertrand's postulate for all natural numbers `n` that are greater than or equal to 512. Bertrand's postulate states that for any such `n`, there exists a prime number `p` that is greater than `n` and less than or equal to `2n`. In other words, for every sufficiently large natural number, there is at least one prime number between that number and twice that number.
More concisely: For all natural numbers `n` ≥ 512, there exists a prime number `p` such that n < p <= 2n.
|
Nat.exists_prime_lt_and_le_two_mul_succ
theorem Nat.exists_prime_lt_and_le_two_mul_succ :
∀ {n : ℕ} (q : ℕ) {p : ℕ},
p.Prime → p ≤ 2 * q → (n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n) → n < p → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
The theorem `Nat.exists_prime_lt_and_le_two_mul_succ` asserts that for any natural number `n`, if we have a prime number `p` such that `p` is less than or equal to twice `q` and `n` is less than `p`, then there exists a prime number `p` which is greater than `n` and less than or equal to twice `n`. This is assuming we can always find such a prime for any number less than `q`. This theorem essentially expresses Bertrand's postulate, which states that for every natural number `n`, there is always at least one prime number `p` between `n` and `2n`.
More concisely: Given any natural number `n` and a prime `p` less than or equal to 2 times some larger natural number `q` such that `n` is less than `p`, there exists a prime `p'` greater than `n` and less than or equal to 2 times `n`.
|
centralBinom_le_of_no_bertrand_prime
theorem centralBinom_le_of_no_bertrand_prime :
∀ (n : ℕ),
2 < n → (¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n) → n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
This theorem provides an upper bound on the central binomial coefficient in the context of Bertrand's postulate. Specifically, if there is no prime number, `p`, between `n` and `2 * n` (which would contradict Bertrand's postulate), then the central binomial coefficient of `n` is at most `(2 * n) ^ sqrt(2 * n) * 4 ^ (2 * n / 3)`. The theorem sets out the boundaries for the prime factors of the central binomial coefficient: primes up to `sqrt (2 * n)` contribute at most `2 * n` each; primes between `sqrt (2 * n)` and `2 * n / 3` contribute at most `4^(2 * n / 3)` in total; there are no primes between `2 * n / 3` and `n`, between `n` and `2 * n`, or above `2 * n`.
More concisely: If there is no prime number between n and 2 * n, then the central binomial coefficient of n is bounded above by (2 * n) ^ sqrt(2 * n) * 4 ^ (2 * n / 3).
|
bertrand_main_inequality
theorem bertrand_main_inequality : ∀ {n : ℕ}, 512 ≤ n → n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
This theorem represents the inequality that contradicts Bertrand's postulate for large enough natural numbers `n`. Specifically, it says that for any natural number `n` that is greater than or equal to 512, the product of `n`, the square root of `(2*n)` raised to the power of `2*n`, and `4` raised to the power of `2*n/3`, is less than or equal to `4` raised to the power of `n`.
More concisely: For any natural number `n` greater than or equal to 512, $(n \cdot (\sqrt{2 \cdot n})^{2 \cdot n} \cdot 4^{2 \cdot n / 3}) \leq 4^n$.
|
centralBinom_factorization_small
theorem centralBinom_factorization_small :
∀ (n : ℕ),
2 < n →
(¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n) →
n.centralBinom = (Finset.range (2 * n / 3 + 1)).prod fun p => p ^ n.centralBinom.factorization p
This theorem, `centralBinom_factorization_small`, states that for any natural number `n` greater than 2, if there does not exist a prime number `p` such that `n` is less than `p` and `p` is less than or equal to `2n` (i.e., Bertrand's postulate does not hold), then the prime factorization of the central binomial coefficient of `n` only contains prime factors less than or equal to `2n/3 + 1`. More specifically, the central binomial coefficient of `n` is equal to the product of each prime number `p` in the range 0 to `2n/3 + 1`, each raised to the power given by the factorization of the central binomial coefficient of `n`.
More concisely: For natural numbers `n` > 2 not obeying Bertrand's postulate, the prime factorization of the central binomial coefficient of `n` consists only of prime numbers less than or equal to `2n/3 + 1`.
|
Nat.bertrand
theorem Nat.bertrand : ∀ (n : ℕ), n ≠ 0 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
**Bertrand's Postulate Theorem**: For any positive natural number `n` that is not zero, there exists a prime number `p` with the properties that `p` is greater than `n` but `p` is also less than or equal to two times `n`.
In other words, this theorem assures that for every non-zero natural number, we can always find a prime number that is bigger than it but no more than twice as large. Prime numbers are defined in this case as elements of a commutative monoid with zero (such as a ring) which are not zero, not a unit, and if they divide the product of any two elements `a` and `b`, then they must divide at least one of `a` or `b`.
More concisely: For every positive integer `n` not equal to 1, there exists a prime number `p` such that `n < p <= 2*n`.
|
Bertrand.real_main_inequality
theorem Bertrand.real_main_inequality : ∀ {x : ℝ}, 512 ≤ x → x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x := by
sorry
The theorem `Bertrand.real_main_inequality` states that for any real number `x` that is equal to or larger than 512, the inequality `x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x` holds. This is a version of `Bertrand.main_inequality` that has been reified, or made explicit. However, this is not the best possible version of the theorem, as it can actually hold for values of `x` that are 464 or larger.
More concisely: For any real number `x` greater than or equal to 512, `x * (2*x) ^ (2*x)^(1/2) * 4 ^ (2*x/3) is dominated by 4 ^ x`.
|
Nat.exists_prime_lt_and_le_two_mul
theorem Nat.exists_prime_lt_and_le_two_mul : ∀ (n : ℕ), n ≠ 0 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
**Bertrand's Postulate**: This theorem states that for every non-zero natural number, there exists a prime number that is greater than this number but not more than double its value. In other words, given any positive natural number 'n', it's guaranteed that there is a prime number 'p' such that 'n' is less than 'p' and 'p' is less than or equal to 'n' times 2.
More concisely: For every natural number n > 1, there exists a prime number p with n < p <= 2n.
|