feat(NumberTheory): Chebyshev's lower bound on primorial#37299
feat(NumberTheory): Chebyshev's lower bound on primorial#37299XC0R wants to merge 5 commits intoleanprover-community:masterfrom
Conversation
Prove primorial(n) ≥ 2^(n/2) for n ≥ 2, the lower bound complement to primorial_le_four_pow. First formalization of this result. Main theorems: - two_pow_le_primorial: 2^n ≤ primorial(2n) for n ≥ 29 - two_pow_div_two_le_primorial: 2^(n/2) ≤ primorial(n) for n ≥ 2
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary e960b84129Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
github-actions
bot
added
the
t-number-theory
|
I think this should eventually go into |
|
Noted, happy to move it into |
|
The character-per-line limit looks smaller than Mathlib's default. Could you format the code to make it look about the same width as the rest of the codebase? |
MichaelStollBayreuth
left a comment
MichaelStollBayreuth
left a comment
There was a problem hiding this comment.
Here are some suggestions (unfortunately the layout has changed whie I was working on the review). I'll continue at a later time.
|
|
||
| public import Mathlib.Data.Nat.Choose.Factorization | ||
| public import Mathlib.NumberTheory.Primorial | ||
|
|
There was a problem hiding this comment.
No empty lines between public import statements (but an empty line separating them from plain imports, which is done here).
| We prove `2 ^ (n / 2) ≤ n#` for all `n ≥ 2`, where `n#` denotes the | ||
| primorial (product of all primes ≤ n). This is the lower bound complement | ||
| to `primorial_le_four_pow` (which gives the upper bound `n# ≤ 4^n`). | ||
|
|
There was a problem hiding this comment.
It would be good to mention that this is weaker than (√2)^n ≤ n# when n is odd.
| Central binomial decomposition: from `4^n < n * C(2n,n)` (Mathlib's | ||
| `Nat.four_pow_lt_mul_centralBinom`) and `v_p(C(2n,n)) ≤ log_p(2n)` | ||
| (Mathlib's `Nat.factorization_choose_le_log`), we bound `C(2n,n)` above |
There was a problem hiding this comment.
| Central binomial decomposition: from `4^n < n * C(2n,n)` (Mathlib's | |
| `Nat.four_pow_lt_mul_centralBinom`) and `v_p(C(2n,n)) ≤ log_p(2n)` | |
| (Mathlib's `Nat.factorization_choose_le_log`), we bound `C(2n,n)` above | |
| Central binomial decomposition: from `4^n < n * C(2n,n)` (`Nat.four_pow_lt_mul_centralBinom`) and `v_p(C(2n,n)) ≤ log_p(2n)` (`Nat.factorization_choose_le_log`), we bound `C(2n,n)` above |
We are within Mathlib here!
|
|
||
| The key analytical step shows `(log₂(2n)+1) * (√(2n)+2) ≤ n` for | ||
| `n > 400` by factoring through `r = √n`: | ||
| - `2*(L+1) ≤ r` via `2n < 2^(r/2)` (exponential beats polynomial) |
| The key analytical step shows `(log₂(2n)+1) * (√(2n)+2) ≤ n` for | ||
| `n > 400` by factoring through `r = √n`: | ||
| - `2*(L+1) ≤ r` via `2n < 2^(r/2)` (exponential beats polynomial) | ||
| - `√(2n)+2 ≤ 2*r` via `zify` + `nlinarith` |
There was a problem hiding this comment.
Mentioning tactics here does not really add information (they will be visible in the proof).
| (2 * n) ^ (Nat.sqrt (2 * n) + 1).primesBelow.card * | ||
| (2 * n)# := by | ||
| set s := Nat.sqrt (2 * n) | ||
| let S := {p ∈ Finset.range (2 * n + 1) | Nat.Prime p} |
There was a problem hiding this comment.
| let S := {p ∈ Finset.range (2 * n + 1) | Nat.Prime p} | |
| let S := (2 * n + 1).primesBelow |
Since this exists, it makes sense to use it.
| (Nat.centralBinom n) h, _root_.pow_zero] | ||
| rw [← Nat.prod_pow_factorization_centralBinom n, ← hS, | ||
| ← Finset.prod_filter_mul_prod_filter_not S (· ≤ s)] | ||
| apply Nat.mul_le_mul |
There was a problem hiding this comment.
| apply Nat.mul_le_mul | |
| gcongr |
is more idiomatic; it avoids mentioning a lemma name and makes clear what is going on.
| · refine (Finset.prod_le_prod' fun p _ => | ||
| (?_ : f p ≤ 2 * n)).trans ?_ | ||
| · exact Nat.pow_factorization_choose_le | ||
| (by omega : 0 < 2 * n) | ||
| rw [Finset.prod_const] | ||
| apply Nat.pow_le_pow_right (by omega) | ||
| apply Finset.card_le_card | ||
| intro p hp | ||
| obtain ⟨h1, _⟩ := Finset.mem_filter.1 hp | ||
| rw [Nat.mem_primesBelow] | ||
| exact ⟨by omega, (Finset.mem_filter.mp h1).2⟩ |
There was a problem hiding this comment.
You can add
lemma Nat.primesBelow_filter_lt {m n : ℕ} (h : m ≤ n) :
n.primesBelow.filter (· < m) = m.primesBelow := by
grind [primesBelow]
lemma Nat.primesBelow_filter_le {m n : ℕ} (h : m < n) :
n.primesBelow.filter (· ≤ m) = (m + 1).primesBelow := by
convert primesBelow_filter_lt (show m + 1 ≤ n by lia) using 2
grindto Mathlib.NumberTheory.SmoothNumbers; then this part of the proof reduces to
| · refine (Finset.prod_le_prod' fun p _ => | |
| (?_ : f p ≤ 2 * n)).trans ?_ | |
| · exact Nat.pow_factorization_choose_le | |
| (by omega : 0 < 2 * n) | |
| rw [Finset.prod_const] | |
| apply Nat.pow_le_pow_right (by omega) | |
| apply Finset.card_le_card | |
| intro p hp | |
| obtain ⟨h1, _⟩ := Finset.mem_filter.1 hp | |
| rw [Nat.mem_primesBelow] | |
| exact ⟨by omega, (Finset.mem_filter.mp h1).2⟩ | |
| · rw [primesBelow_filter_le (sqrt_le_self (2 * n) |>.trans_lt (lt_add_one _))] | |
| exact Finset.prod_le_pow_card _ _ _ fun _ _ ↦ pow_factorization_choose_le (by lia) |
| · calc ∏ p ∈ S.filter (¬ · ≤ s), f p | ||
| ≤ ∏ p ∈ S.filter (¬ · ≤ s), p := by | ||
| apply Finset.prod_le_prod' fun p hp => ?_ | ||
| obtain ⟨h1, _⟩ := Finset.mem_filter.1 hp | ||
| have hp_prime := (Finset.mem_filter.1 h1).2 | ||
| dsimp only [f] | ||
| refine (Nat.pow_le_pow_right hp_prime.pos | ||
| ?_).trans (pow_one p).le | ||
| exact Nat.factorization_choose_le_one | ||
| (Nat.sqrt_lt'.mp (by omega)) | ||
| _ ≤ (2 * n)# := by | ||
| unfold primorial | ||
| apply Finset.prod_le_prod_of_subset_of_one_le' | ||
| · intro p hp | ||
| obtain ⟨h1, _⟩ := Finset.mem_filter.1 hp | ||
| rw [Finset.mem_filter, Finset.mem_range] | ||
| at h1 ⊢ | ||
| exact ⟨h1.1, h1.2⟩ | ||
| · intro p hp _ | ||
| exact (Finset.mem_filter.1 hp).2.one_le |
There was a problem hiding this comment.
This part of the argument can be simplified a bit (it is still basically the same proof, though), for example as follows.
| · calc ∏ p ∈ S.filter (¬ · ≤ s), f p | |
| ≤ ∏ p ∈ S.filter (¬ · ≤ s), p := by | |
| apply Finset.prod_le_prod' fun p hp => ?_ | |
| obtain ⟨h1, _⟩ := Finset.mem_filter.1 hp | |
| have hp_prime := (Finset.mem_filter.1 h1).2 | |
| dsimp only [f] | |
| refine (Nat.pow_le_pow_right hp_prime.pos | |
| ?_).trans (pow_one p).le | |
| exact Nat.factorization_choose_le_one | |
| (Nat.sqrt_lt'.mp (by omega)) | |
| _ ≤ (2 * n)# := by | |
| unfold primorial | |
| apply Finset.prod_le_prod_of_subset_of_one_le' | |
| · intro p hp | |
| obtain ⟨h1, _⟩ := Finset.mem_filter.1 hp | |
| rw [Finset.mem_filter, Finset.mem_range] | |
| at h1 ⊢ | |
| exact ⟨h1.1, h1.2⟩ | |
| · intro p hp _ | |
| exact (Finset.mem_filter.1 hp).2.one_le | |
| · rw [primorial, ← primesBelow] | |
| have H : ∀ p ∈ {x ∈ (2 * n + 1).primesBelow | ¬x ≤ s}, f p ≤ p := by | |
| intro p hp | |
| nth_rewrite 2 [← pow_one p] | |
| exact pow_le_pow_right₀ (by grind) <| factorization_choose_le_one <| sqrt_lt'.mp (by grind) | |
| refine Finset.prod_le_prod' H |>.trans ?_ | |
| exact Finset.prod_le_prod_of_subset_of_one_le (filter_subset ..) (by lia) | |
| fun p hp _ ↦ (prime_of_mem_primesBelow hp).one_le |
Most of the simplification comes from using grind to do the fairly obvious (but slightly tedious) parts.
In the end, one can also eliminate the definition of S; then the first part of the proof becomes
set s := sqrt (2 * n)
let f x := x ^ (centralBinom n).factorization x
have hS : ∏ x ∈ (2 * n + 1).primesBelow, f x = ∏ x ∈ Finset.range (2 * n + 1), f x := by
refine Finset.prod_filter_of_ne fun p _ h ↦ ?_
contrapose! h; dsimp only [f]
rw [factorization_eq_zero_of_not_prime _ h, pow_zero]
rw [← prod_pow_factorization_centralBinom, ← hS,
← Finset.prod_filter_mul_prod_filter_not _ (· ≤ s)]| private theorem numerical_bound_small (n : ℕ) | ||
| (hn : 29 ≤ n) (hn2 : n ≤ 400) : | ||
| n * (2 * n) ^ | ||
| (Nat.sqrt (2 * n) + 1).primesBelow.card ≤ 2 ^ n := by |
There was a problem hiding this comment.
| private theorem numerical_bound_small (n : ℕ) | |
| (hn : 29 ≤ n) (hn2 : n ≤ 400) : | |
| n * (2 * n) ^ | |
| (Nat.sqrt (2 * n) + 1).primesBelow.card ≤ 2 ^ n := by | |
| private theorem numerical_bound_small {n : ℕ} (hn : 29 ≤ n) (hn2 : n ≤ 400) : | |
| n * (2 * n) ^ (sqrt (2 * n) + 1).primesBelow.card ≤ 2 ^ n := by |
See above.
This proof is very slow. There should be a faster argument.
Here is one possibility (trade-off between code length and code speed).
private theorem numerical_bound_small {n : ℕ} (hn : 29 ≤ n) (hn2 : n ≤ 400) :
n * (2 * n) ^ (sqrt (2 * n) + 1).primesBelow.card ≤ 2 ^ n := by
rcases le_or_gt n 84 with h₁ | h₁
· interval_cases n <;> (norm_num [primesBelow]; decide)
rcases le_or_gt n 264 with h₂ | h₂
· have : #((2 * n).sqrt + 1).primesBelow ≤ 8 := by
rw [show 8 = #((2 * 264).sqrt + 1).primesBelow by norm_num [primesBelow]; decide]
refine card_le_card <| Finset.filter_subset_filter Prime <| Finset.range_subset_range.mpr ?_
gcongr
grw [this]
· calc
_ ≤ 264 * (2 * 264) ^ 8 := by gcongr
_ ≤ 2 ^ 85 := by norm_num
_ ≤ 2 ^ n := pow_le_pow_right₀ (by lia) (by lia)
· lia
have : #((2 * n).sqrt + 1).primesBelow ≤ 9 := by
rw [show 9 = #((2 * 400).sqrt + 1).primesBelow by norm_num [primesBelow]; decide]
refine card_le_card <| Finset.filter_subset_filter Prime <| Finset.range_subset_range.mpr ?_
gcongr
grw [this]
· calc
_ ≤ 400 * (2 * 400) ^ 9 := by gcongr
_ ≤ 2 ^ 100 := by norm_num
_ ≤ 2 ^ n := pow_le_pow_right₀ (by lia) (by lia)
· lia…cal_bound - Remove redundant prime_pow_factorization_centralBinom_le (already in Mathlib) - Make theorem parameters implicit where deducible - Replace omega with lia throughout - Drop Nat. prefix where namespace is open - Add primesBelow_filter_lt and primesBelow_filter_le to SmoothNumbers - Simplify centralBinom proof using new helpers and grind - Replace slow interval_cases numerical_bound_small with 3-interval approach - Move proof remarks from docstrings to comments - Generalize two_pow_div_two_le_primorial to all n (no hypothesis needed) - Note odd-n weakness in module docstring
| exact numerical_bound_large (by lia) | ||
|
|
||
| /-- **Chebyshev's lower bound (even form)**: `2 ^ n ≤ (2n)#` for `n ≥ 29`. -/ | ||
| theorem two_pow_le_primorial {n : ℕ} (hn : 29 ≤ n) : 2 ^ n ≤ (2 * n)# := by |
There was a problem hiding this comment.
The 29 ≤ n assumption can be removed. This should be done in a separate lemma two_pow_le_primorial while renaming this lemma to two_pow_le_primorial_of_le.
Remove the `29 ≤ n` hypothesis from `two_pow_le_primorial` by adding a computational base case for `n ≤ 28`. The previous version is retained as `two_pow_le_primorial_of_le`. Addresses review suggestion by Parcly-Taxel.
4 participants
Summary
Prove
primorial(n) ≥ 2^(n/2)for alln ≥ 2(Chebyshev's 1852 lower bound). This is the lower bound complement toprimorial_le_four_pow. Addresses the TODO atChebyshev.leanline 50: "Prove Chebyshev's lower bound."New file:
Mathlib/NumberTheory/PrimorialLowerBound.leanMain theorems:
two_pow_le_primorial:2 ^ n ≤ primorial (2 * n)forn ≥ 29two_pow_div_two_le_primorial:2 ^ (n / 2) ≤ primorial nforn ≥ 2Key intermediates:
centralBinom_le_pow_mul_primorial:C(2n,n) ≤ (2n)^{π(√(2n)+1)} * primorial(2n)eight_mul_sq_add_le_two_pow:8u² + 16u + 8 ≤ 2^uforu ≥ 10Proof technique
Central binomial decomposition: from
four_pow_lt_mul_centralBinomandfactorization_choose_le_log, boundC(2n,n)above by(2n)^{π(√(2n)+1)} * primorial(2n). Rearranging givesprimorial(2n) ≥ 2^nforn ≥ 29. Base cases bynorm_num+decide, largenanalytically via√nfactoring.AI disclosure
Claude (Anthropic) was used as a coding assistant for Lean tactic exploration, file structuring, and CI debugging. All proof strategy, mathematical content, and final code have been reviewed and are understood by the author.