Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(number_theory): Bertrand's postulate, slightly different approach #8002

Closed
wants to merge 507 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
507 commits
Select commit Hold shift + click to select a range
657d6c6
remove more lemmas
BoltonBailey Jan 13, 2022
040b122
install tighter binomial bound
BoltonBailey Jan 13, 2022
a28242e
remove unneded code
BoltonBailey Jan 13, 2022
50a9633
log_four_nonzero lemma
BoltonBailey Jan 13, 2022
e5a4045
delete commented code
BoltonBailey Jan 13, 2022
931d2c0
golf
BoltonBailey Jan 13, 2022
d1ca5eb
golf
BoltonBailey Jan 13, 2022
551b92f
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Jan 15, 2022
5e979d9
refactor
BoltonBailey Jan 15, 2022
ef94528
imporve docs on final theorem
BoltonBailey Jan 15, 2022
45654c7
add todos
BoltonBailey Jan 15, 2022
5c19c32
eliminate lemma
BoltonBailey Jan 15, 2022
0daf3e8
delete more lemmas
BoltonBailey Jan 15, 2022
b5293c4
golf foo proof
BoltonBailey Jan 15, 2022
96f62b4
unfactor foo
BoltonBailey Jan 15, 2022
eb14cbf
change primes
BoltonBailey Jan 15, 2022
3ce2dcb
delete unneeded or recursively provided imports
BoltonBailey Jan 15, 2022
c884644
calc formatting
BoltonBailey Jan 15, 2022
64311e4
dot notation
BoltonBailey Jan 16, 2022
765e53a
translate to sqrt
BoltonBailey Jan 16, 2022
cfe790d
infix notation
BoltonBailey Jan 16, 2022
c6a0063
infix notation
BoltonBailey Jan 16, 2022
7ffc811
congr
BoltonBailey Jan 16, 2022
c4ebb75
remove simps
BoltonBailey Jan 16, 2022
e3c8387
Update docstring
Smaug123 Jan 19, 2022
c1270da
Merge remote-tracking branch 'origin/master' into prime-power-central…
Smaug123 Jan 19, 2022
b8761a6
Merge branch 'prime-power-central-binom' into bertrand-2
Smaug123 Jan 19, 2022
09275d8
Start using stuff from dependency branch
Smaug123 Jan 19, 2022
75a1843
add references
BoltonBailey Jan 21, 2022
60d15b1
Merge branch 'bertrand-2' of github.com:leanprover-community/mathlib …
BoltonBailey Jan 21, 2022
7813c61
fix lines too long
BoltonBailey Jan 21, 2022
1fd1ee5
more reference edits
BoltonBailey Jan 21, 2022
0f0f5de
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Feb 1, 2022
e9914e0
unfactored small lemmas
BoltonBailey Feb 1, 2022
e048743
move proof sketch
BoltonBailey Feb 1, 2022
ac5fa3d
add sections
BoltonBailey Feb 1, 2022
1738190
found lemma in library
BoltonBailey Feb 1, 2022
77c47a2
fix lines too long
BoltonBailey Feb 1, 2022
bca6166
remove nat namespacing
BoltonBailey Feb 1, 2022
43deed6
remove real namespacing
BoltonBailey Feb 1, 2022
d9452e8
golf
BoltonBailey Feb 1, 2022
1248ae7
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Apr 14, 2022
0d0508d
Apply suggestions from code review
Smaug123 Apr 18, 2022
2ee94e5
Docstring lint
Smaug123 Apr 18, 2022
205ac88
Merge branch 'master' into prime-power-central-binom
Smaug123 Apr 18, 2022
8e2a320
Add better docstrings and renames
Smaug123 Apr 18, 2022
3137fa4
Remove unnecessary lemma
Smaug123 Apr 18, 2022
75db8d9
Use variables
Smaug123 Apr 20, 2022
c76a2b4
Merge branch 'prime-power-central-binom' into bertrand-2
Smaug123 Apr 20, 2022
b9a2ca5
Golf
Smaug123 Apr 20, 2022
d320e55
Lint a bit
Smaug123 Apr 20, 2022
a5e974d
More style things, and add to 100.yaml
Smaug123 Apr 20, 2022
d735a46
Tighten the bounds a lot
Smaug123 Apr 21, 2022
2da98ba
Better comments
Smaug123 Apr 21, 2022
4a26662
A bit more golfing
Smaug123 Apr 22, 2022
53b1a9e
More lint
Smaug123 Apr 22, 2022
d4e5ec4
Merge master
Smaug123 Apr 25, 2022
a5d4a0c
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Apr 25, 2022
430fa33
fix broken lemmas
BoltonBailey Apr 25, 2022
c3986aa
comment out lemma already in library
BoltonBailey Apr 25, 2022
fe15965
edit prime list to have smaller prime
BoltonBailey Apr 25, 2022
987e42f
fix style complaints
BoltonBailey Apr 25, 2022
1ab6921
golf away lemma
BoltonBailey Apr 25, 2022
0fbc595
a few comments on where to move certain lemmas
BoltonBailey Apr 25, 2022
282b375
move lemmas generalize
BoltonBailey Apr 29, 2022
d6e7665
golf
BoltonBailey Apr 29, 2022
949caaf
rename
BoltonBailey Apr 29, 2022
7dbc0ea
changes
BoltonBailey Apr 29, 2022
9c5ef00
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey May 7, 2022
07ed177
adapt proof to new pr
BoltonBailey May 7, 2022
7cfab26
comments
BoltonBailey May 7, 2022
0c0757f
Rem unused function
Smaug123 May 7, 2022
f109ad5
golf and unfact
BoltonBailey May 7, 2022
cda51c8
more golf
BoltonBailey May 7, 2022
db8050b
unicodeize "nat"
BoltonBailey May 7, 2022
f2d1d8b
golf
BoltonBailey May 7, 2022
a62541c
comments
BoltonBailey May 7, 2022
c1c67ae
clean up comments
BoltonBailey May 7, 2022
592b9ab
golf
BoltonBailey May 7, 2022
0bee8fa
deinstance prime
BoltonBailey May 7, 2022
32faa9a
remove alpha
BoltonBailey May 7, 2022
0186e51
add lemmas from bertrand branch
BoltonBailey May 7, 2022
cc158c6
edits
BoltonBailey May 7, 2022
c47a8f1
add new refs
BoltonBailey May 7, 2022
fce6f6b
fix refs
BoltonBailey May 7, 2022
e26fe36
remove args
BoltonBailey May 7, 2022
1666e2e
Update src/data/nat/choose/central.lean
BoltonBailey May 7, 2022
2077ac5
Update src/data/nat/choose/central.lean
BoltonBailey May 8, 2022
1f372aa
golf
BoltonBailey May 8, 2022
ff33225
switch to factorization
BoltonBailey May 9, 2022
e7f53df
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey May 9, 2022
02d40ea
fix call
BoltonBailey May 9, 2022
2a04623
another lemma
BoltonBailey May 9, 2022
22ceef0
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey May 9, 2022
5d51b49
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey May 11, 2022
375fcc3
spell factorization the way it's spelled in the function
BoltonBailey May 12, 2022
b8d7b88
Merge branch 'master' into BoltonBailey/central_binom_padic
BoltonBailey May 24, 2022
b65afbf
Update src/data/nat/choose/central.lean
BoltonBailey May 24, 2022
2fcf5b3
Update src/data/nat/choose/central.lean
BoltonBailey May 24, 2022
6e7ad2d
remove unused arg
BoltonBailey May 29, 2022
d6fa7da
split into new file
BoltonBailey May 29, 2022
d1d31a4
remove unnecessary p.prime assumptions
BoltonBailey May 29, 2022
d575f1a
lix line too long
BoltonBailey May 29, 2022
3f615a4
Update src/data/nat/choose/central.lean
BoltonBailey May 30, 2022
aeaeaae
Update src/data/nat/choose/factorization.lean
BoltonBailey May 30, 2022
51eb143
Update src/data/nat/choose/factorization.lean
BoltonBailey May 30, 2022
01f06aa
readd central binom lemma
BoltonBailey May 30, 2022
32b619a
Update src/data/nat/choose/factorization.lean
BoltonBailey May 31, 2022
64940e0
Update src/data/nat/choose/factorization.lean
BoltonBailey May 31, 2022
148c6d6
Update src/data/nat/choose/factorization.lean
BoltonBailey May 31, 2022
8507815
update docs
BoltonBailey May 31, 2022
0887e9d
fix docs
BoltonBailey May 31, 2022
127c9c3
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 1, 2022
3e0f87f
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 1, 2022
de32950
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 1, 2022
cb99334
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 1, 2022
03b6219
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 1, 2022
d369b5b
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 1, 2022
4a48fe4
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 1, 2022
e5476db
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 1, 2022
fbc6599
delete lemma
BoltonBailey Jun 1, 2022
8d8b84a
Merge branch 'BoltonBailey/central_binom_padic' of github.com:leanpro…
BoltonBailey Jun 1, 2022
011401f
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 2, 2022
8aebe67
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 2, 2022
31fc974
Merge master
Smaug123 Jun 3, 2022
fc322f7
Fix typo in comment
Smaug123 Jun 3, 2022
87a325b
Merge upstream
Smaug123 Jun 3, 2022
431dc38
Update docs/references.bib
BoltonBailey Jun 3, 2022
82a7ee3
Update docs/references.bib
BoltonBailey Jun 3, 2022
aa487af
Mostly merge BoltonBailey/central_binom_padic
Smaug123 Jun 3, 2022
a15bb6c
Resolve log 4 markups
Smaug123 Jun 3, 2022
702ea02
remove prime
BoltonBailey Jun 4, 2022
28a9bc4
remove prime prefix
BoltonBailey Jun 4, 2022
0558371
Fix typo in bibtex
Smaug123 Jun 4, 2022
1f667fb
Merge branch 'BoltonBailey/central_binom_padic' into bertrand-2
Smaug123 Jun 4, 2022
158f1e1
Something seems to have gone wrong
Smaug123 Jun 4, 2022
9d7f539
Lemmas
Smaug123 Jun 5, 2022
55f8fee
Fix proof
Smaug123 Jun 5, 2022
5bfde65
Style lint
Smaug123 Jun 5, 2022
dc71a11
Remove unnecessary lemma
Smaug123 Jun 5, 2022
e2769b7
Merge master
Smaug123 Jun 5, 2022
46cc98b
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 7, 2022
015f48b
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 7, 2022
17412d3
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 7, 2022
28aeecd
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 7, 2022
a468acd
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 7, 2022
d49c2e8
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 7, 2022
7c7c6e6
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 7, 2022
2d3ba4c
move factorization_eq_zero_of_lt
BoltonBailey Jun 7, 2022
3b719ec
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 7, 2022
7a6f2f3
Merge branch 'master' into BoltonBailey/central_binom_padic
Smaug123 Jun 8, 2022
02f43d7
Merge branch 'BoltonBailey/central_binom_padic' into bertrand-2
Smaug123 Jun 8, 2022
24d4759
Merge master
Smaug123 Jun 9, 2022
cd2cbf2
Fix docstring
Smaug123 Jun 9, 2022
ed51702
golf out preexisting lemma
BoltonBailey Jun 9, 2022
441edd8
cleaner factorization lemmas
BoltonBailey Jun 10, 2022
57e092c
delete old lemmas
BoltonBailey Jun 10, 2022
bfe965f
simplify and move lemmas
BoltonBailey Jun 10, 2022
bb63977
comment elaboration
BoltonBailey Jun 10, 2022
e664a2e
fix curly braces
BoltonBailey Jun 10, 2022
13019b4
replace sq lemmas
BoltonBailey Jun 11, 2022
0913d3d
golf
BoltonBailey Jun 11, 2022
2a27073
add ref to pr
BoltonBailey Jun 11, 2022
526db67
Get rid of non-terminal simps
Smaug123 Jun 12, 2022
19a4584
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Jun 15, 2022
9640187
remove moved lemma
BoltonBailey Jun 15, 2022
a15d4a5
golf
BoltonBailey Jun 15, 2022
db1905a
fix colon
BoltonBailey Jun 16, 2022
fa912fc
switch to eric's proof
BoltonBailey Jun 16, 2022
03fed0c
Update src/number_theory/bertrand.lean
BoltonBailey Jun 16, 2022
0441451
Update src/number_theory/bertrand.lean
BoltonBailey Jun 16, 2022
e4f66de
golfing
BoltonBailey Jun 16, 2022
43ba6e3
Merge branch 'bertrand-2' of github.com:leanprover-community/mathlib …
BoltonBailey Jun 16, 2022
bdcf9b0
Update src/number_theory/bertrand.lean
BoltonBailey Jun 16, 2022
8a35864
linlined/deleted lemmas
BoltonBailey Jun 16, 2022
19b9d4e
Merge branch 'bertrand-2' of github.com:leanprover-community/mathlib …
BoltonBailey Jun 16, 2022
3ce4eea
golf
BoltonBailey Jun 16, 2022
b134aa6
fixed bug
BoltonBailey Jun 16, 2022
9a2ccef
golf
BoltonBailey Jun 16, 2022
a7e52f6
extract exp 1 lt 3 lemma
BoltonBailey Jun 16, 2022
52b72b4
Update src/data/complex/exponential_bounds.lean
BoltonBailey Jun 17, 2022
842a248
golf
BoltonBailey Jun 17, 2022
e37e7e2
Merge branch 'bertrand-2' of github.com:leanprover-community/mathlib …
BoltonBailey Jun 17, 2022
33e1202
fix line
BoltonBailey Jun 17, 2022
6c432b0
private lemmas and namespaces
BoltonBailey Jun 17, 2022
501a70e
remove unused lemma
BoltonBailey Jun 17, 2022
3d309cb
inline log_four_pos_nonzero
BoltonBailey Jun 17, 2022
2cd944c
get rid of unused log four lemma
BoltonBailey Jun 17, 2022
3ce90e2
inline four_eq_two_rpow_two
BoltonBailey Jun 17, 2022
63af6bc
exp_two_le_722 inline
BoltonBailey Jun 17, 2022
716bcb1
renaming and namespacing
BoltonBailey Jun 17, 2022
5ac46c5
namespacing
BoltonBailey Jun 18, 2022
822a81b
remove nat filter prime
BoltonBailey Jun 18, 2022
d871c53
golfing
BoltonBailey Jun 18, 2022
8b408b6
golfs
BoltonBailey Jun 18, 2022
b9e29ca
fix doc
BoltonBailey Jun 18, 2022
14328ac
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 18, 2022
d36c304
fix build
BoltonBailey Jun 19, 2022
e30144d
Update src/number_theory/bertrand.lean
BoltonBailey Jun 19, 2022
dc416b0
Update src/number_theory/bertrand.lean
BoltonBailey Jun 19, 2022
388cc23
Update src/number_theory/bertrand.lean
BoltonBailey Jun 19, 2022
8703762
Update src/data/nat/choose/factorization.lean
BoltonBailey Jun 19, 2022
b1d5b8a
Update src/number_theory/bertrand.lean
BoltonBailey Jun 27, 2022
08e6a12
Update src/number_theory/bertrand.lean
BoltonBailey Jun 27, 2022
b7a9794
Update src/number_theory/bertrand.lean
BoltonBailey Jun 27, 2022
40efc86
Update exponential_bounds.lean
BoltonBailey Jun 28, 2022
43e6b93
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Jun 28, 2022
465bb18
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Jul 4, 2022
282764c
721->648
BoltonBailey Jul 4, 2022
8fc982c
Update src/number_theory/bertrand.lean
BoltonBailey Jul 6, 2022
cc52d16
Update src/number_theory/bertrand.lean
BoltonBailey Jul 6, 2022
c77a00a
Update src/number_theory/bertrand.lean
BoltonBailey Jul 6, 2022
ca57c67
Update src/number_theory/bertrand.lean
BoltonBailey Jul 6, 2022
8ca865c
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Jul 6, 2022
88fe992
Update src/number_theory/bertrand.lean
BoltonBailey Jul 8, 2022
a678b98
Update src/number_theory/bertrand.lean
BoltonBailey Jul 8, 2022
b982206
Update src/number_theory/bertrand.lean
BoltonBailey Jul 8, 2022
4e07162
Update src/number_theory/bertrand.lean
BoltonBailey Jul 8, 2022
87cf418
Update src/number_theory/bertrand.lean
BoltonBailey Jul 8, 2022
a30881d
Update src/number_theory/bertrand.lean
BoltonBailey Jul 8, 2022
4bf9ed5
lower prime
BoltonBailey Jul 8, 2022
3c6f6fe
remove comments
BoltonBailey Jul 8, 2022
cbf69c9
Remove redundant explanation
Smaug123 Jul 8, 2022
9240d4b
edit tochori comment
BoltonBailey Jul 10, 2022
5c20fa2
absorb first step of central_binom_le_of_no_bertrand_prime into centr…
BoltonBailey Jul 10, 2022
e3b8c60
golf
BoltonBailey Jul 10, 2022
126c1a0
golf
BoltonBailey Jul 10, 2022
fbda8c6
golf
BoltonBailey Jul 10, 2022
9f1b82c
nat to \N
BoltonBailey Jul 10, 2022
f77621c
golf
BoltonBailey Jul 10, 2022
ce482a2
golf, todo
BoltonBailey Jul 10, 2022
a4dbc33
golf
BoltonBailey Jul 10, 2022
9f195d4
fix err_lin
BoltonBailey Jul 10, 2022
9dcbbc9
golf
BoltonBailey Jul 10, 2022
f1f2293
golf
BoltonBailey Jul 10, 2022
b42a2dc
Golfs from tb65536
Smaug123 Jul 11, 2022
9f9beda
golf!
tb65536 Jul 12, 2022
e25db2a
Update src/number_theory/bertrand.lean
BoltonBailey Jul 12, 2022
bcfc4a8
add namespace to comment
BoltonBailey Jul 19, 2022
6372b62
rename choose factorization lemmas
BoltonBailey Jul 19, 2022
71cd5eb
add some tags
BoltonBailey Jul 19, 2022
bdc554e
change n_pos
BoltonBailey Jul 19, 2022
7f8dff2
aliasing
BoltonBailey Jul 19, 2022
d5a44f7
Update src/number_theory/bertrand.lean
BoltonBailey Jul 19, 2022
027dae4
lix lines
BoltonBailey Jul 19, 2022
14874e5
Merge branch 'bertrand-2' of github.com:leanprover-community/mathlib …
BoltonBailey Jul 19, 2022
c32a486
Update 100.yaml
BoltonBailey Jul 19, 2022
4940deb
duplicated nat
BoltonBailey Jul 20, 2022
2eb3a3b
remove profiling
BoltonBailey Jul 20, 2022
1116e47
proof golf & optimization
digama0 Jul 31, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions docs/100.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -390,6 +390,8 @@
author : Anne Baanen
98:
title : Bertrand’s Postulate
decl : nat.bertrand
author : Bolton Bailey, Patrick Stevens
99:
title : Buffon Needle Problem
100:
Expand Down
2 changes: 1 addition & 1 deletion src/data/nat/choose/central.lean
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ end

/--
An exponential lower bound on the central binomial coefficient.
This bound is weaker than `four_pow_n_lt_n_mul_central_binom`, but it is of historical interest
This bound is weaker than `nat.four_pow_lt_mul_central_binom`, but it is of historical interest
because it appears in Erdős's proof of Bertrand's postulate.
-/
lemma four_pow_le_two_mul_self_mul_central_binom : ∀ (n : ℕ) (n_pos : 0 < n),
Expand Down
29 changes: 29 additions & 0 deletions src/data/nat/choose/factorization.lean
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ do not appear in the factorization of the `n`th central binomial coefficient.
These results appear in the [Erdős proof of Bertrand's postulate](aigner1999proofs).
-/

open_locale big_operators

namespace nat

variables {p n k : ℕ}
Expand Down Expand Up @@ -137,4 +139,31 @@ lemma le_two_mul_of_factorization_central_binom_pos
(h_pos : 0 < (central_binom n).factorization p) : p ≤ 2 * n :=
le_of_not_lt (pos_iff_ne_zero.mp h_pos ∘ factorization_central_binom_eq_zero_of_two_mul_lt)

/-- A binomial coefficient is the product of its prime factors, which are at most `n`. -/
lemma prod_pow_factorization_choose (n k : ℕ) (hkn : k ≤ n) :
∏ p in (finset.range (n + 1)),
p ^ ((nat.choose n k).factorization p)
= choose n k :=
begin
nth_rewrite_rhs 0 ←factorization_prod_pow_eq_self (choose_pos hkn).ne',
rw eq_comm,
apply finset.prod_subset,
{ intros p hp,
rw finset.mem_range,
contrapose! hp,
rw [finsupp.mem_support_iff, not_not, factorization_choose_eq_zero_of_lt hp] },
{ intros p _ h2, simp [not_not.1 (mt finsupp.mem_support_iff.2 h2)] },
end

/-- The `n`th central binomial coefficient is the product of its prime factors, which are
at most `2n`. -/
lemma prod_pow_factorization_central_binom (n : ℕ) :
∏ p in (finset.range (2 * n + 1)),
p ^ ((central_binom n).factorization p)
= central_binom n :=
begin
apply prod_pow_factorization_choose,
linarith,
end

end nat
234 changes: 234 additions & 0 deletions src/number_theory/bertrand.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,234 @@
/-
Copyright (c) 2020 Patrick Stevens. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Stevens, Bolton Bailey
-/
import data.nat.choose.factorization
import number_theory.primorial
import analysis.convex.specific_functions

/-!
# Bertrand's Postulate

This file contains a proof of Bertrand's postulate: That between any positive number and its
double there is a prime.

The proof follows the outline of the Erdős proof presented in "Proofs from THE BOOK": One considers
the prime factorization of `(2 * n).choose n`, and splits the constituent primes up into various
groups, then upper bounds the contribution of each group. This upper bounds the central binomial
coefficient, and if the postulate does not hold, this upper bound conflicts with a simple lower
bound for large enough `n`. This proves the result holds for large enough `n`, and for smaller `n`
an explicit list of primes is provided which covers the remaining cases.

As in the [Metamath implementation](carneiro2015arithmetic), we rely on some optimizations from
[Shigenori Tochiori](tochiori_bertrand). In particular we use the cleaner bound on the central
binomial coefficient given in `nat.four_pow_lt_mul_central_binom`.

## References

* [M. Aigner and G. M. Ziegler _Proofs from THE BOOK_][aigner1999proofs]
* [S. Tochiori, _Considering the Proof of “There is a Prime between n and 2n”_][tochiori_bertrand]
* [M. Carneiro, _Arithmetic in Metamath, Case Study: Bertrand's Postulate_][carneiro2015arithmetic]
BoltonBailey marked this conversation as resolved.
Show resolved Hide resolved

## Tags

Bertrand, prime, binomial coefficients
-/

open_locale big_operators

section real

open real

namespace bertrand

/--
A reified version of the `bertrand.main_inequality` below.
This is not best possible: it actually holds for 464 ≤ x.
-/
lemma real_main_inequality {x : ℝ} (n_large : (512 : ℝ) ≤ x) :
x * (2 * x) ^ (sqrt (2 * x)) * 4 ^ (2 * x / 3) ≤ 4 ^ x :=
begin
let f : ℝ → ℝ := λ x, log x + sqrt (2 * x) * log (2 * x) - log 4 / 3 * x,
have hf' : ∀ x, 0 < x → 0 < x * (2 * x) ^ sqrt (2 * x) / 4 ^ (x / 3) :=
λ x h, div_pos (mul_pos h (rpow_pos_of_pos (mul_pos two_pos h) _)) (rpow_pos_of_pos four_pos _),
have hf : ∀ x, 0 < x → f x = log (x * (2 * x) ^ sqrt (2 * x) / 4 ^ (x / 3)),
{ intros x h5,
have h6 := mul_pos two_pos h5,
have h7 := rpow_pos_of_pos h6 (sqrt (2 * x)),
rw [log_div (mul_pos h5 h7).ne' (rpow_pos_of_pos four_pos _).ne', log_mul h5.ne' h7.ne',
log_rpow h6, log_rpow zero_lt_four, ← mul_div_right_comm, ← mul_div, mul_comm x] },
have h5 : 0 < x := lt_of_lt_of_le (by norm_num1) n_large,
rw [← div_le_one (rpow_pos_of_pos four_pos x), ← div_div_eq_mul_div, ← rpow_sub four_pos,
← mul_div 2 x, mul_div_left_comm, ← mul_one_sub, (by norm_num1 : (1 : ℝ) - 2 / 3 = 1 / 3),
mul_one_div, ← log_nonpos_iff (hf' x h5), ← hf x h5],
have h : concave_on ℝ (set.Ioi 0.5) f,
{ refine ((strict_concave_on_log_Ioi.concave_on.subset (set.Ioi_subset_Ioi _)
(convex_Ioi 0.5)).add ((strict_concave_on_sqrt_mul_log_Ioi.concave_on.comp_linear_map
((2 : ℝ) • linear_map.id)).subset
(λ a ha, lt_of_eq_of_lt _ ((mul_lt_mul_left two_pos).mpr ha)) (convex_Ioi 0.5))).sub
((convex_on_id (convex_Ioi 0.5)).smul (div_nonneg (log_nonneg _) _)); norm_num1 },
suffices : ∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0,
{ obtain ⟨x1, x2, h1, h2, h0, h3, h4⟩ := this,
exact (h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4 },
refine ⟨18, 512, by norm_num1, by norm_num1, le_trans (by norm_num1) n_large, _, _⟩,
{ have : sqrt (2 * 18) = 6 :=
(sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1),
rw [hf, log_nonneg_iff (hf' 18 _), this]; norm_num1 },
{ have : sqrt (2 * 512) = 32,
{ exact (sqrt_eq_iff_mul_self_eq_of_pos (by norm_num1)).mpr (by norm_num1) },
rw [hf, log_nonpos_iff (hf' _ _), this, div_le_one (rpow_pos_of_pos four_pos _),
← rpow_le_rpow_iff _ (rpow_pos_of_pos four_pos _).le three_pos, ← rpow_mul]; norm_num1 },
end

end bertrand

end real

section nat

open nat

/--
The inequality which contradicts Bertrand's postulate, for large enough `n`.
-/
lemma bertrand_main_inequality {n : ℕ} (n_large : 512 ≤ n) :
n * (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n :=
begin
rw ← @cast_le ℝ,
simp only [cast_bit0, cast_add, cast_one, cast_mul, cast_pow, ← real.rpow_nat_cast],
have n_pos : 0 < n := (dec_trivial : 0 < 512).trans_le n_large,
have n2_pos : 1 ≤ 2 * n := mul_pos dec_trivial n_pos,
refine trans (mul_le_mul _ _ _ _) (bertrand.real_main_inequality (by exact_mod_cast n_large)),
{ refine mul_le_mul_of_nonneg_left _ (nat.cast_nonneg _),
refine real.rpow_le_rpow_of_exponent_le (by exact_mod_cast n2_pos) _,
exact_mod_cast real.nat_sqrt_le_real_sqrt },
{ exact real.rpow_le_rpow_of_exponent_le (by norm_num1) (cast_div_le.trans (by norm_cast)) },
{ exact real.rpow_nonneg_of_nonneg (by norm_num1) _ },
{ refine mul_nonneg (nat.cast_nonneg _) _,
exact real.rpow_nonneg_of_nonneg (mul_nonneg zero_le_two (nat.cast_nonneg _)) _, },
end

/--
A lemma that tells us that, in the case where Bertrand's postulate does not hold, the prime
factorization of the central binomial coefficent only has factors at most `2 * n / 3 + 1`.
-/
lemma central_binom_factorization_small (n : ℕ) (n_large : 2 < n)
(no_prime: ¬∃ (p : ℕ), p.prime ∧ n < p ∧ p ≤ 2 * n) :
central_binom n = ∏ p in finset.range (2 * n / 3 + 1), p ^ ((central_binom n).factorization p) :=
begin
refine (eq.trans _ n.prod_pow_factorization_central_binom).symm,
apply finset.prod_subset,
{ exact finset.range_subset.2 (add_le_add_right (nat.div_le_self _ _) _) },
intros x hx h2x,
rw [finset.mem_range, lt_succ_iff] at hx h2x,
rw [not_le, div_lt_iff_lt_mul' three_pos, mul_comm x] at h2x,
replace no_prime := not_exists.mp no_prime x,
rw [←and_assoc, not_and', not_and_distrib, not_lt] at no_prime,
cases no_prime hx with h h,
{ rw [factorization_eq_zero_of_non_prime n.central_binom h, pow_zero] },
{ rw [factorization_central_binom_of_two_mul_self_lt_three_mul n_large h h2x, pow_zero] },
end

/--
An upper bound on the central binomial coefficient used in the proof of Bertrand's postulate.
The bound splits the prime factors of `central_binom n` into those
1. At most `sqrt (2 * n)`, which contribute at most `2 * n` for each such prime.
2. Between `sqrt (2 * n)` and `2 * n / 3`, which contribute at most `4^(2 * n / 3)` in total.
3. Between `2 * n / 3` and `n`, which do not exist.
4. Between `n` and `2 * n`, which would not exist in the case where Bertrand's postulate is false.
5. Above `2 * n`, which do not exist.
-/
lemma central_binom_le_of_no_bertrand_prime (n : ℕ) (n_big : 2 < n)
(no_prime : ¬∃ (p : ℕ), nat.prime p ∧ n < p ∧ p ≤ 2 * n) :
central_binom n ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) :=
begin
have n_pos : 0 < n := (nat.zero_le _).trans_lt n_big,
have n2_pos : 1 ≤ 2 * n := mul_pos two_pos n_pos,
let S := (finset.range (2 * n / 3 + 1)).filter nat.prime,
let f := λ x, x ^ n.central_binom.factorization x,
have : ∏ (x : ℕ) in S, f x = ∏ (x : ℕ) in finset.range (2 * n / 3 + 1), f x,
{ refine finset.prod_filter_of_ne (λ p hp h, _),
contrapose! h, dsimp only [f],
rw [factorization_eq_zero_of_non_prime n.central_binom h, pow_zero] },
rw [central_binom_factorization_small n n_big no_prime, ← this,
← finset.prod_filter_mul_prod_filter_not S (≤ sqrt (2 * n))],
apply mul_le_mul',
{ refine (finset.prod_le_prod'' (λ p hp, (_ : f p ≤ 2 * n))).trans _,
{ exact pow_factorization_choose_le (mul_pos two_pos n_pos) },
have : (finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n),
{ rw [card_Icc, nat.add_sub_cancel] },
rw finset.prod_const,
refine pow_le_pow n2_pos ((finset.card_le_of_subset (λ x hx, _)).trans this.le),
obtain ⟨h1, h2⟩ := finset.mem_filter.1 hx,
exact finset.mem_Icc.mpr ⟨(finset.mem_filter.1 h1).2.one_lt.le, h2⟩ },
{ refine le_trans _ (primorial_le_4_pow (2 * n / 3)),
refine (finset.prod_le_prod' (λ p hp, (_ : f p ≤ p))).trans _,
{ obtain ⟨h1, h2⟩ := finset.mem_filter.1 hp,
refine (pow_le_pow (finset.mem_filter.1 h1).2.one_lt.le _).trans (pow_one p).le,
exact nat.factorization_choose_le_one (sqrt_lt'.mp $ not_le.1 h2) },
refine finset.prod_le_prod_of_subset_of_one_le' (finset.filter_subset _ _) _,
exact λ p hp _, (finset.mem_filter.1 hp).2.one_lt.le }
end

namespace nat

/--
Proves that Bertrand's postulate holds for all sufficiently large `n`.
-/
lemma exists_prime_lt_and_le_two_mul_eventually (n : ℕ) (n_big : 512 ≤ n) :
∃ (p : ℕ), p.prime ∧ n < p ∧ p ≤ 2 * n :=
begin
-- Assume there is no prime in the range.
by_contradiction no_prime,
-- Then we have the above sub-exponential bound on the size of this central binomial coefficient.
-- We now couple this bound with an exponential lower bound on the central binomial coefficient,
-- yielding an inequality which we have seen is false for large enough n.
have H1 : n * (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n := bertrand_main_inequality n_big,
have H2 : 4 ^ n < n * n.central_binom :=
nat.four_pow_lt_mul_central_binom n (le_trans (by norm_num1) n_big),
have H3 : n.central_binom ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) :=
central_binom_le_of_no_bertrand_prime n (lt_of_lt_of_le (by norm_num1) n_big) no_prime,
rw mul_assoc at H1, exact not_le.2 H2 ((mul_le_mul_left' H3 n).trans H1),
end

/--
Proves that Bertrand's postulate holds over all positive naturals less than n by identifying a
descending list of primes, each no more than twice the next, such that the list contains a witness
for each number ≤ n.
-/
lemma exists_prime_lt_and_le_two_mul_succ {n} (q)
{p : ℕ} (prime_p : nat.prime p) (covering : p ≤ 2 * q)
(H : n < q → ∃ (p : ℕ), p.prime ∧ n < p ∧ p ≤ 2 * n)
(hn : n < p) : ∃ (p : ℕ), p.prime ∧ n < p ∧ p ≤ 2 * n :=
begin
by_cases p ≤ 2 * n, { exact ⟨p, prime_p, hn, h⟩ },
exact H (lt_of_mul_lt_mul_left' (lt_of_lt_of_le (not_le.1 h) covering))
end

/--
**Bertrand's Postulate**: For any positive natural number, there is a prime which is greater than
it, but no more than twice as large.
-/
theorem exists_prime_lt_and_le_two_mul (n : ℕ) (hn0 : n ≠ 0) :
∃ p, nat.prime p ∧ n < p ∧ p ≤ 2 * n :=
begin
-- Split into cases whether `n` is large or small
cases lt_or_le 511 n,
-- If `n` is large, apply the lemma derived from the inequalities on the central binomial
-- coefficient.
{ exact exists_prime_lt_and_le_two_mul_eventually n h, },
replace h : n < 521 := h.trans_lt (by norm_num1),
revert h,
-- For small `n`, supply a list of primes to cover the initial cases.
([317, 163, 83, 43, 23, 13, 7, 5, 3, 2].mmap' $ λ n,
`[refine exists_prime_lt_and_le_two_mul_succ %%(reflect n) (by norm_num1) (by norm_num1) _]),
exact λ h2, ⟨2, prime_two, h2, nat.mul_le_mul_left 2 (nat.pos_of_ne_zero hn0)⟩,
end

alias nat.exists_prime_lt_and_le_two_mul ← bertrand

end nat

end nat