Outstanding Tasks, V1

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

Thanks for all the contributions so far, especially @Bolton Bailey who gave us our first dark green backgrounds with proofs of the Smooth Urysohn lemma and its relative, SmoothExistence. We now also have a first light green background in PerronFormulaLtOne. (Recall that this means that its proof is formalized, but depends on things that are not yet.) The dependencies are (by design) very simple, so please feel free to claim any of the following:

1. RectangleIntegral_eq_zero says that the integral of a holomorphic function on a rectangle vanishes, and should be a simple matter of applying integral_boundary_rect_eq_zero_of_differentiableOn. Done thanks to @llllvvuu
2. RectangleIntegral_tendsTo_VerticalIntegral is also rather simple, saying that if you integrate over a rectangle, and send the top and bottom to infinity (assuming those decay), what's left is the difference of the (positively-oriented) integrals over the sides. Right now there are no conditions on $f$, so we will need to stipulate that the top and bottom integrals go to zero. (And then this condition will need to be implemented where RectangleIntegral_tendsTo_VerticalIntegral is used in the proof of PerronFormulaLtOne. Again, I would be surprised if this caused great difficulty... Claimed by @llllvvuu
3. limitOfConstant should be very simple, saying that a constant function whose limit is zero, is also zero. (Maybe it's already in Mathlib somewhere?) Done thanks to @llllvvuu
4. HolomorphicOn_of_Perron_function says that, for $x>0$, the function $s\mapsto x^s/(s(s+1))$ is holomorphic (i.e., Complex differentiable) for $\Re(s)>0$. Just a matter of chaining some differentiability statements together; shouldn't be too hard. Done by @llllvvuu
5. PerronIntegralPosAux says essentially that $x\mapsto 1/(1+x^2)$ is integrable over $\R$; shouldn't be hard for someone familiar with that part of the library... Done by @llllvvuu
6. tendsto_Realpow_atTop_nhds_0_of_norm_lt_1 says that if $0<x<1$, then $x^\sigma\to0$ as $\sigma\to\infty$ in $\R$. Such a thing nearly exists, called tendsto_pow_atTop_nhds_0_of_norm_lt_1, but not quite (uses natural exponents, whereas we want real)... Done by @Yury G. Kudryashov
7. VertIntPerronBound is a bound on an integral, applying the triangle inequality, and bounding $|x^s|\le x^{\Re(s)}$; again, shouldn't be too hard. Solved by @Ruben Van de Velde

Those would close out PerronFormulaLtOne. I'm working on a similar treatment for PerronFormulaGtOne which will be more complicated, as we actually need to pull some contours past poles and evaluate residues. Those two together should give us the PerronFormula and we'll be well on the way towards proving MellinInversion.

In the grand scheme of things, Mellin inversion can be used to prove Fourier inversion, which would get us closer to the Fourier transform being a bijection on Schwartz functions. The latter is en route to the first proof of Weak PNT. Though at this point, if @Arend Mellendijk's Selberg sieve argument works out to prove SmoothedChebyshevClose, it seems to me that we'll get to (a weak) PNT even faster by following the second, complex analytic proof. The latter is also a better warmup for the stronger, exp-root-log-savings proof than weak proof 1...

Please let me know if you'd like to claim any of the above, and of any other comments/suggestions. This is really fun; thanks all for participating!! :)

[Terence Tao]

Chiming in with some selected tasks from the non-complex-analysis parts of the project that should be relatively straightforward.

8. First Fourier Identity. This is basically a Fubini theorem type calculation, and the first step towards the Wiener-Ikehara theorem. Should be pretty simple.
9. Second Fourier identity Another Fubini calculation.
10. Asymptotics for first summatory function Assuming the Weak PNT $\sum_{n \leq x} \Lambda(n) \sim x$ as a black box, it should be relatively simple to conclude that $\sum_{p \leq x} \log p \sim x$ as well. This could be a good test case to see whether we have phrased our asymptotic estimates in a convenient fashion.

[Terence Tao]

I should add that this list is not meant to be exhaustive; if anyone spots a node in the blueprint that they think they can easily polish off, please feel free to claim it even if we don't list it in our recommended task list!

[llllvvuu]

here's "1. RectangleIntegral_eq_zero": https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/18

[llllvvuu]

here's "3. limitOfConstant": https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/19

[Ruben Van de Velde]

I came across something close to 7 recently, let me see if I can find it

[Ruben Van de Velde]

Oh, not all of 7, just docs#Complex.abs_exp

[Alex Kontorovich]

Yes that needs to be added to the triangle inequality, together with a simple estimate for the denominator...

[Ruben Van de Velde]

I've done 7 modulo some integrability goals I'll look at tomorrow

WIP

lemma VertIntPerronBound {x : ℝ} (xpos : 0 < x) (x_le_one : x < 1) {σ : ℝ} (σ_gt_one : 1 < σ) :
    Complex.abs (VerticalIntegral (fun s ↦ x^s / (s * (s + 1))) σ)
      ≤ x ^ σ * ∫ (t : ℝ), 1 / |Real.sqrt (1 + t^2) * Real.sqrt (2 + t^2)| := by
  simp only [VerticalIntegral]
  rw [smul_eq_mul, map_mul, abs_I, one_mul]
  rw [← Complex.norm_eq_abs]
  apply le_trans <| MeasureTheory.norm_integral_le_integral_norm _
  simp_rw [norm_div]
  have : (x : ℂ) ≠ 0 := mod_cast xpos.ne'
  simp [cpow_add _ _ this]
  simp [cpow_mul_ofReal_nonneg xpos.le]
  conv =>
    lhs
    enter [2]
    ext a
    rw [Complex.abs_cpow_eq_rpow_re_of_pos (rpow_pos_of_pos xpos _)]
  simp [div_eq_mul_inv]
  rw [MeasureTheory.integral_mul_left]
  rw [abs_eq_self.mpr xpos.le]
  gcongr
  apply MeasureTheory.integral_mono
  sorry
  sorry
  rw [@Pi.le_def]
  intro a
  rw [← mul_inv]
  gcongr
  rw [abs_eq_self.mpr ?_]
  simp [Complex.abs]
  rw [mul_comm]
  gcongr
  apply sqrt_le_sqrt
  swap
  apply sqrt_le_sqrt
  simp [normSq_add_mul_I]
  rw [abs_eq_self.mpr ?_]
  exact σ_gt_one.le
  apply (one_pos.trans σ_gt_one).le
  calc 2 + a ^ 2 ≤ normSq ((↑(σ + 1) : ℂ) + (a : ℂ) * I) := ?_
    _ = normSq ((σ : ℂ) + (a : ℂ) * I + 1) := ?_
  simp_rw [normSq_add_mul_I]
  gcongr
  nlinarith
  simp [add_right_comm]
  positivity

[Alex Kontorovich]

Great thanks! It's probably closely related to 5; maybe your work on 7 will handle 5 also?

[Yury G. Kudryashov]

Isn't No. 6 docs#tendsto_rpow_atTop_of_base_lt_one ?

[Ruben Van de Velde]

7: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/21

No time to look further at 5; maybe docs#integral_inv_one_add_sq or docs#Real.deriv_arctan is relevant

[llllvvuu]

Here's "4. HolomorphicOn_of_Perron_function": https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/22

[llllvvuu]

I've made some progress on "5. PerronIntegralPosAux": https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/24

I should be able to finish it soon.

[llllvvuu]

llllvvuu said:

I've made some progress on "5. PerronIntegralPosAux": https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/24

I should be able to finish it soon.

Finished

[Alex Kontorovich]

Great thanks!

[Alex Kontorovich]

What's the "right" way to handle things like this more generally? Something like: $\int_\R f(x) dx$ is integrable if, say, $f$ is continuous (so no problems near $0$), and then $\exists \epsilon>0 : |f(x)| = O(x^{-1-\epsilon})$. Does that already exist somewhere? If so, could PerronIntegralPosAux be done more easily by showing the big-O statement, instead of the precise work with $\arctan$?

[Alex Kontorovich]

By the way, even if the above works, the $\arctan$ work will not have been for naught! We'll need it later when we evaluate residues of simple poles. (Do we have, e.g., that $\arctan 1 = \pi/4$?)

[Arend Mellendijk]

(docs#Real.arctan_one)

[llllvvuu]

I probably could have used the following instead: https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean#L89-L123

Oops. Well, it wasn't too bad either way. Once the arctan stuff is upstreamed, we are left with just the proof of the asymptotic, which is necessary regardless of the asymptotic used (1/x^2 or 1/(1+x^2)). Actually, 1/x^2 might've been a bit more tedious for lower bounding the integral.

[llllvvuu]

More generally, I think f = O(g) might be more tedious to work with than f < g, since you have to deal with the part before the "eventually" oops continuity handles this part. Generalization of docs#integrable_of_isBigO_exp_neg to something like integrable_of_isBigO_integrable could work as an API. You have to do apply it to both tails though which is kind of tedious.

Actually, "show integrable by showing f < g for some integrable g" and "show integral pos by showing h < f < g for some h, g with positive integral" are already pretty expedient techniques at a high level. The part that is not as expedient as it could be currently is, inequalities. One could imagine PerronIntegralPosAux being very short had I been able to skip the manual calc and trans work (and in this case, there is also some extra boilerplate because measurability timed out).

[llllvvuu]

--

[llllvvuu]

I've started work on 2. RectangleIntegral_tendsTo_VerticalIntegral: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/28. The lemma is done, I just need to satisfy the new hypotheses.

[Terence Tao]

I just wanted to say that one of the intended outcomes of this project is that we pick up experience with asymptotic notation and how to use estimates to prove statements such as integrability, convergence, etc. in a civilized manner. In particular if in the course of formalizing one of the lemmas in this project, you spot a general lemma (such as a criterion for integrability) that could be re-used for some future application, it may well be worth spinning that off as a standalone lemma, even if it means a little bit more work for the immediate task at hand.

[Yury G. Kudryashov]

... and opening a PR to Mathlib

[Sébastien Gouëzel]

docs#integrable_one_add_norm may prove useful for this kind of things, by the way.

[llllvvuu]

It turns out that I do need to use the asymptotic method, so I've started working on a draft mathlib PR: https://github.com/leanprover-community/mathlib4/pull/10248

The even/odd variant is the one I need (hopefully the statement is actually true). Maybe others will find it helpful too.

[Terence Tao]

llllvvuu said:

It turns out that I do need to use the asymptotic method, so I've started working on a draft mathlib PR: https://github.com/leanprover-community/mathlib4/pull/10248

The even/odd variant is the one I need (hopefully the statement is actually true). Maybe others will find it helpful too.

For integrable_of_isBigO_integrable, perhaps one can replace the hypotheses (hsymm : ∀ x, ‖f x‖ = ‖f (-x)‖) (ho : f =O[atTop] g) with (ho : f =O[atTop] g) (ho' : (fun x ↦ f (-x)) =O[atTop] g)? Or perhaps (ho : f =O[atTop] g) (ho' : f =O[atBot] g') where g' obeys similar hypotheses to g? This could be more flexible for applications, and the original version could be recovered as a corollary.

There is a more abstract statement that if f is locally integrable on some topological measure space X, and is O() of an integrable function with respect to the cocompact filter, then f is integrable, which combines well with the general statement (docs#Continuous.locallyIntegrable) that continuous functions on a locally compact space will be locally integrable wrt any locally finite measure. It may possibly be worth proving this general statement first and deriving your special case from them, since these results are likely to be useful elsewhere (e.g., in higher dimensions).

[Terence Tao]

One could also split this up using docs#MeasureTheory.IntegrableAtFilter into two sublemmas:

1. If f =O[l] g and IntegrableAtFilter g l, then IntegrableAtFilter f l. [EDIT: some measurability hypothesis on f is needed here also.]
2. If IntegrableAtFilter f Filter.cocompact and LocallyIntegrable f, then Integrable f. [EDIT: this is in fact an if and only if.]

EDIT: On the reals (and possibly some other ordered topological spaces), there would also be

3. If IntegrableAtFilter f Filter.cocompact iff IntegrableAtFilter f atTop and IntegrableAtFilter f atBot.
4. On non-negative reals or Ici intervals, one can omit the atBot proposition in #3.

[Arend Mellendijk]

RE: 3, you could split that up further into docs#Real.cocompact_eq and a more general theorem stating IntegrableAtFilter f (l1 ⊔ l2) ↔ (IntegrableAtFilter f l1 ∧ IntegrableAtFilter f l2) (which doesn't seem to exist yet).

[llllvvuu]

Thanks for the suggestions! I've split up the work and proved 1. and 2. in the PR, and will follow up with a dependent PR establishing 3. and 4.

[Terence Tao]

llllvvuu said:

Thanks for the suggestions! I've split up the work and proved 1. and 2. in the PR, and will follow up with a dependent PR establishing 3. and 4.

For part #1, it might be nice to also add the corollary specializing to the top filter ⊤ (so that IntegrableAtFilter simplifies to Integrable - this, by the way, should also be a lemma in Mathlib, possibly even a simp lemma). There will be occasions in the future where we obtain non-asymptotic bounds f =O[⊤] g (as opposed to merely f =O[atTop] g or f =O[Filter.cocompact] g) and it would be nice to support this also.

[llllvvuu]

I've added the requested IntegrableAtFilter f ⊤ μto the first PR and the Real corollaries as a second PR. Both are ready for review for mathlib; in the meantime, I'll try using this content in PrimeNumberTheorem+