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

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

Changes from 112 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
Loading