How to make formalizing limits less tedious?

Stream: PrimeNumberTheorem+

[Terence Tao]

I recently completed the proof of pn_asymptotic, which deduces the $p_n = (1+o(1)) n \log n$ version of the prime number theorem from the $\pi(x) = (1+o(1)) x/\log x$ version. It was surprisingly tedious, coming in at 200 lines and 30000 heartbeats. One of the main reasons was having to establish "easy" limits such as the following:

import Mathlib

open Filter Real

example (ε:ℝ) (hε:ε>0) : atTop.Tendsto (fun n ↦ ((1 + ε) * log n - 1/n) / log ((1 + ε) * n * log n - 1)) (nhds (1+ε))  := by sorry

This alone took me about 80 lines, with the lower order terms causing all sorts of annoying headaches (also the fact that some of the logarithms become negative or junk for very small $n$, though one could usually filter_upwards one's way out of that).

I'm pretty sure I'm doing this the wrong way. Are there any smarter tactics or other tricks to do these sorts of computations efficiently (and, ideally, mindlessly)?

[Bhavik Mehta]

This one seems to be disprovable:

import Mathlib

open Filter Real

lemma thing1 {ε : ℝ} (hε : ε > 0) : atTop.Tendsto (fun n ↦ (1 + ε) * n * log n - 1) atTop := by
  suffices atTop.Tendsto (fun n ↦ (1 + ε) * (n * log n)) atTop by
    simpa [mul_assoc] using Filter.tendsto_atTop_add_const_right _ (-1) this
  apply Filter.Tendsto.const_mul_atTop' (by positivity)
  exact tendsto_id.atTop_mul_atTop₀ Real.tendsto_log_atTop

open Topology

lemma thing2 (ε:ℝ) (hε:ε>0) :
    atTop.Tendsto (fun n ↦ ((1 + ε) * n * log n - 1) / log ((1 + ε) * n * log n - 1)) atTop := by
  suffices atTop.Tendsto (fun n ↦ n / log n) atTop from this.comp (thing1 hε)
  suffices atTop.Tendsto (fun n ↦ log n / n) (𝓝[>] 0) from (tendsto_inv_nhdsGT_zero.comp this).congr (by simp)
  rw [nhdsWithin, tendsto_inf]
  constructor
  · simpa using Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 (by simp)
  · rw [tendsto_principal]
    filter_upwards [eventually_gt_atTop 1] with x hx
    exact div_pos (log_pos hx) (by positivity)

example (ε:ℝ) (hε:ε>0) :
    ¬ atTop.Tendsto (fun n ↦ ((1 + ε) * n * log n - 1) / log ((1 + ε) * n * log n - 1)) (nhds (1+ε)) := by
  intro h
  simpa [inf_nhds_atTop, NeBot.ne, Tendsto] using h.inf (thing2 ε hε)

[Bhavik Mehta]

For the original question: I agree this is tedious, and my personal approach is to break the limit down in steps (actually as I did above), using lots of suffices or have blocks, and use simp/ring to handle lots of the algebra and lower order terms. (I had a lot of this kind of explicit limit and explicit asymptotic calculation in both the unit-fractions and exponential-ramsey projects). I'm hoping this: #announce > New tactic: `compute_asymptotics` will help a lot with this kind of goal too.

[Terence Tao]

Oops, my extraction of the limit from the proof had an extraneous $n$ in the numerator, which I have now deleted.

[Alex Kontorovich]

This is a great test case for compute_asymptotics - has it hit Mathlib yet? I did a slew of this kind of very painful line by line analysis when finishing MediumPNT (working with $\exp((\log x)^{1/10}))$, yuck!..); we indeed need a lot more automation to see through stuff like this.

[Michael Rothgang]

My understanding is that compute_asymptotics is still quite far away from mathlib, simplify because there is a lot of code to review.

[Michael Rothgang]

To give you an idea: getting 2000 lines of code merged in two weeks is impressive. (If you have a dedicated reviewer who promptly reviews everything you make can give you this.) That tactic is about 16000 lines of remaining code. So, getting it merged faster than within a few months would certainly be surprising and require a very very dedicated effort.

[Alex Kontorovich]

How hard would it be to folk the repo where compute_asymptotics already lives, and try it out there?

[Alastair Irving]

I agree this is currently very painful. In this case though I wonder if you could have given a much shorter proof without introducing $\epsilon$:

1. From the PNT we have $n=\pi(p_n)\sim p_n/\log p_n$
2. Taking logs $\log n \sim \log p_n-\log\log p_n\sim \log p_n$
3. Multiplying these gives $p_n\sim n\log n$
   Unless I'm missing something these steps all use fairly standard results about asymptotics which should already exist or could be added if not.

[Terence Tao]

Ha, that would have been a lot simpler! I unfortunately won't have the time to refactor the argument along these lines, but if anyone else wants to volunteer, be my guest...