How to spell asymptotics?

Stream: PrimeNumberTheorem+

[Terence Tao]

I'm starting to write out some possible spellings for various versions of the prime number theorem and I'm not obviously seeing what the "best" way to do so is. For instance, here is the current proposal to spell the weak prime number theorem:

open Nat Real BigOperators ArithmeticFunction Filter

theorem WeakPNT :
    Tendsto (fun N : ℕ ↦ ((Finset.range N).sum Λ) / N) atTop (nhds 1) := by
  sorry

But I am also experimenting with this spelling for a slight variant of the PNT:

open BigOperators Filter Real Classical Asymptotics

theorem chebyshev_asymptotic : ∃ E : ℝ → ℝ, E =o[atTop] (fun x ↦ (x:ℝ)) ∧ ∀ x : ℝ, ∑ p in (Finset.filter Nat.Prime (Finset.range ⌊x⌋₊)), log p = x + E x := by
  sorry

thus making the parameter real instead of natural number, and trying to utilize the o() notation. The various results in Section 5 of the blueprint seem to slightly favor this type of spelling, but perhaps there is a better way. Any thoughts would be appreciated.

[Yaël Dillies]

@Yury G. Kudryashov or @Anatole Dedecker, didn't you have plans to make asymptotic notation work for the natural numbers?

[Yury G. Kudryashov]

What's Λ in WeakPNT?

[Yury G. Kudryashov]

Note that we have docs#Asymptotics.IsEquivalent

[Yury G. Kudryashov]

So you can write f ~[atTop] Nat.cast

[David Michael Roberts]

https://en.wikipedia.org/wiki/Von_Mangoldt_function, no?

[Terence Tao]

Yury G. Kudryashov said:

Note that we have docs#Asymptotics.IsEquivalent

Nice! Here is one form then:

theorem chebyshev_asymptotic : (fun x ↦ ∑ p in (Finset.filter Nat.Prime (Finset.range ⌈x⌉₊)), log p) ~[atTop] (fun x ↦ x) := by sorry

It is true that one could also just work with the natural numbers

theorem chebyshev_asymptotic' : (fun n ↦ ∑ p in (Finset.filter Nat.Prime (Finset.range n)), log p) ~[atTop] Nat.cast := by sorry

but I am thinking it will be more convenient in elementary number theory applications to generalize these sorts of summatory estimates to the reals. This is because we often use identities such as $\sum_{n \leq x} f*g(n) = \sum_{d \leq x} \sum_{m \leq x/d} f(d) g(m)$ (where $f*g$ is the Dirichlet convolution of $f,g$) and for this sort of manipulation it is likely better to permit $x, d, x/d$ to all be reals rather than natural numbers. (But perhaps we could have several versions of each of these theorems. For instance it could make sense to have one version for ⌊x⌋₊ and one for ⌈x⌉₊, corresponding to the ranges n ≤ x and n < x respectively. In principle one could try to set a uniform convention to just use one version throughout, but I think there is no consensus in the literature on which version is preferred.

[Terence Tao]

Perhaps what we will end up doing is create some general lemmas showing that various slightly different versions of a given asymptotic estimate are equivalent.