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

[Smaug123]

---

• depends on: [Merged by Bors] - feat(data/complex/exponential): bound on exp for arbitrary arguments #8667
• depends on: [Merged by Bors] - feat(number_theory/prime_counting): The prime counting function #9080
• depends on: [Merged by Bors] - feat(data/nat/choose): add facts about the multiplicity of primes in the factorisation of central binomial coefficients #9925 [then we can take a lot of the stuff about \alpha from data.nat.choose.central instead]
• depends on: [Merged by Bors] - feat(analysis/special_functions/log): add log_div_self_antitone_on #10985
• depends on: [Merged by Bors] - feat(analysis/special_functions/{log, pow}): add log_base #11246
• depends on: [Merged by Bors] - feat(analysis/special_functions/log/monotone): add lemmas #13848
• depends on: [Merged by Bors] - feat(data/nat/choose/central): arity of primes in central binomial coefficients #14017
• depends on: [Merged by Bors] - feat(data/nat/factorization): Lemma on zero-ness of factorization #14560
• depends on: [Merged by Bors] - feat(data/nat/prime): prime.even_iff #14688
• depends on: [Merged by Bors] - feat(analysis/convex/special_functions): sqrt * log is strictly convex on x>1 #14822
• depends in: [Merged by Bors] - feat(analysis/convex/function): Variants of convex_on.le_right_of_left_le #14821

Related to #2784, going via analysis.
@BoltonBailey You might be interested in this - the remaining sorries are all quite tractable.

[adomani]

I started looking at this PR and I am very happy that you are working on Bertrand's postulate! At the moment, I only have some golfing suggestions.

[Smaug123]

Good luck proving log 584 + 2 ≤ 8 - it's not true! The LHS is 8.3699.

[BoltonBailey]

• depends on: [Merged by Bors] - feat(data/complex/exponential): bound on exp for arbitrary arguments #8667

[BoltonBailey]

Update: Since being advised to tighten up the proof a little, I have been working on some things related to the prime counting function, so we can have a better bound on that if desired. Right now, I have gone through to comment out many of the calculus based proofs, some of which seem to have broken, and which shouldn't be necessary anyway if we go the "log x / x is decreasing" route. To that end I have redone the reification of the main inequality (see real_false_inequality_is_false). Notice that even without the tightening of the binomial coefficient bound and prime counting function from the Tochiori proof, we can still do Tochiori's last step of dividing through by x and using the same log x / x logic. It remains to be seen what n_big ends up as this way, but perhaps it's worth working through anyway.

[Smaug123]

Notice that even without the tightening of the binomial coefficient bound and prime counting function from the Tochiori proof, we can still do Tochiori's last step of dividing through by x and using the same log x / x logic.

We do actually have Tochiori's bounds already, in data.nat.choose.central. I've also got #9925 which I haven't looked at for a while, but that pulls out a couple more of the lemmas from this file into data.nat.choose.central.

[BoltonBailey]

Ok, after 6 or so months, this PR is once again compiling and sorry-free, now without derivatives. There are still things left to do in terms of making the tighter Tochiori bounds on the prime counting function and binomial coefficient so that we don't have to brute force a prime over 1024. Also, generally cleaning the proof up. Ideally, each of the statements in the main inequality chain should be isolated and extracted as their own lemmas, which are then chained together in a calc proof.

[Smaug123]

@BoltonBailey Thanks for plugging away at it! The PR will get shorter once #9925 is merged and we've integrated src/data/nat/choose/central.lean into this proof; it's basically a parallel cherry-picked development of the central binomial coefficient stuff, but it's already committed to mathlib.

[urkud]

Thanks a lot! LGTM modulo a few minor comments but I would prefer to have one more review before merging it.
UPD: @digama0 says that there is a better proof. I'm assigning this PR to him.

[BoltonBailey]

@digama0 To explain what's happened with this PR since we discussed it last, and why we haven't implemented all the tricks from the Tochiori paper: We did start on these, but I think we concluded that the main thing that was causing the cutoff n to be so high was loose reasoning in the main part of the proof. After fixing these and using your proof that ln x / x is decreasing, the cutoff dropped to about n >= 700, at which point the prime-checking wasn't really the main bottleneck. So at that point I stopped working on the Tochiori lemmas and just went about cleaning up the PR.

If you still feel that the cutoff should be around 64, I can follow through on the proof that prime_counting n <= n/3 + 2, which I think is the biggest part of the Tochiori reasoning for reducing the cutoff. But when I attempted a proof of this earlier, I found it involved a lot of casework, and I wasn't sure adding a few more 10s of lines to prove a specific bound like this would ultimately decrease the compilation time.

[digama0]

The prime checking is not the bottleneck, the issue is the proof of the asymptotic part. Tochiori's proof both lowers the bound and also works out numerically much better, without the need for huge high precision estimates of log.

[tb65536]

The prime checking is not the bottleneck, the issue is the proof of the asymptotic part. Tochiori's proof both lowers the bound and also works out numerically much better, without the need for huge high precision estimates of log.

Tochiori's proof sounds nice. But where does the current proof use high precision estimates of log?

[BoltonBailey]

Tochiori's proof sounds nice. But where does the current proof use high precision estimates of log?

I think @digama0 may be thinking of a version of the proof from before you came and switched out the proof we had with the one using the concavity of sqrt * log. Indeed at many points in the past the proof has used estimates from the file data/complex/exponential_bounds. The concavity of sqrt * log doesn't use these though, so I think the proof now no longer depends on them. Indeed, it seems like switching away from the Tochiori style where we apply antitonicity of log x / x saved about 20 seconds of compilation time, comparing commit 8703762 to the current one and running set_option profiler true on the real inequality and its dependencies, the time for the Tochiori version was about ~30 sec, whereas now it's about ~8 sec.

In fact, even if I ignore the runtime from the lemmas in the Tochiori version which use the exponential bounds, I still get that the current version is about 10 seconds faster. I'm not sure it makes sense to switch back, given that it would apparently increase the running time.

[jcommelin]

@digama0 🏓

[digama0]

@BoltonBailey The proof does indeed look a lot better now. I gave it a once-over, a mix of golfing, optimization, and unpacking some long lines, and now the whole file compiles in about 4 seconds, comparable to much more basic files, which is a testament to all the work that went into improving those bounds. Congratulations!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests