Outstanding Tasks, V2

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

For V1, see here

Wow contributions are coming in faster than I can produce new targets, amazing! We have nearly completed the execution of our first contour pull (passing no poles) to prove formulaLtOne. All that's left, as far as I can tell, is

1. isIntegrable Is the integrability of the Perron function; should be relatively easy. Done by @llllvvuu
2. tendsto_zero_Lower
   This and its cousin, tendsto_zero_Upper
   say that the integrals of the Perron function $s\mapsto x^s/(s(1+s))$ over a finite horizontal line at height $t$, decays to zero as $t\to\pm\infty$. Done by @llllvvuu

After these, let's make our next immediate target the first contour pull to the left, namely residuePull1, as described below. I have refactored things a bit, moving all the discussion about general meromorphic functions and poles of arbitrary order out of the blueprint (into GeneralMeromorphic.lean); we will only ever need simple poles, so let's not deal with the difficulties of the general case at this time.

The first batch of targets are for general complex analytic functions (or just pure geometry).

3. RectanglePullToNhdOfPole says that, if you have a holomorphic function on a rectangle except a point, you can zoom the rectangle in on a small square centered at the point. The proof is simply to chop the big rectangle with two horizontal and two vertical cuts into nine rectangles, the middle of which is the desired square. Then use HolomorphicOn.vanishesOnRectangle to show that the eight other rectangle integrals vanish. This theorem should be very accessible. Done by me and @llllvvuu
4. ResidueTheoremAtOrigin: This is the key calculation that will allow us to compute residues, saying that the integral of $s\mapsto 1/s$ around a unit square is 1. The proof is just two uses of $\arctan'x = 1/(1+x^2)$; should also be very accessible, given what's already formalized. Solved by @Paul Nelson
5. ResidueTheoremOnRectangleWithSimplePole With the previous two, we can prove that, if $f$ is holomorphic on a rectangle except $p\in\mathbb C$, and has "principal part" $A/(s-p)$ (that is, $f (s) = A/(s-p) + g(s)$ where $g$ is holomorphic on the whole rectangle), then the integral of $f$ over the rectangle is $A$. The proof is to replace $f$ by $A/(s-p)+g$; the integral of $g$ vanishes. Then localize the integral to a little square around $p$ using RectanglePullToNhdOfPole, and apply a change of variables to be able to quote ResidueTheoremAtOrigin. Should not be too difficult. Claimed by me and @Paul Nelson
6. RectangleIntegral_tendsTo_UpperU and RectangleIntegral_tendsTo_LowerU are two lemmas very similar to RectangleIntegral_tendsTo_VerticalIntegral; they say that if you pull the top of a RectangleIntegral up, it becomes an UpperUIntegral, and similarly if you pull down. They should be relatively easy to prove. Claimed by @Vláďa Sedláček

[Alex Kontorovich]

(deleted)

[Alex Kontorovich]

(deleted)

[Alex Kontorovich]

7. DiffVertRect_eq_UpperLowerUs This says that the difference between two vertical integrals and a rectangle between them is equal to an UpperU integral and a LowerU. Should be fairly easy to prove. Done by @Moritz Firsching

Then we have targets specific to the Perron function.

8. isHolomorphicOn
   [Edit: Changed name from isHolomorphicOn2.] This is just an extension of isHolomorphicOn (in fact the latter should be refactored into the former; we don't need both statements). The proof should be nearly identical. Done by @llllvvuu

[Alex Kontorovich]

9. vertIntBoundLeft is very similar to the completed vertIntBound, just for $\sigma<-3/2$. I also stated vertIntBound2 but now I realize it's not as useful, because the implied constant depends on $\sigma$, and we'll want to pull $\sigma$ around. I'll leave the statement there for now, but I think we'll eventually get rid of that one. (Is there a better way to unify these?) Done by @Arend Mellendijk

[Alex Kontorovich]

10. diffBddAtZero This says that the function $s\mapsto x^s/(s(1+s)) - 1/s$ remains bounded near $0$; this is because $x^s/s- x^0/s$ is the difference quotient of $s\mapsto x^s$ at $s=0$. Shouldn't be too hard to prove. Unclaimed by @Alex Kontorovich
11. sigmaNegOneHalfPull: This says that the vertical integral over $(\sigma)$, minus that over $(-1/2)$, is equal to the RectangleIntegral with opposite corners $-1/2-iT$ and $$\sigma+iT$, for any $T>0$. To prove this, use DiffVertRect_eq_UpperLowerUs to turn the difference into an UpperU minus a LowerU. Each of the U's is a limit of rectangle integrals, which are all zero (since $f$ is holomorphic there). Done by @Arend Mellendijk
    and finally:
12. residuePull1: This says that the vertical integral over the line $(\sigma)$ with $\sigma>0$ is equal to $1$ plus the vertical integral over the line $(-1/2)$, which passes through the pole at $s=0$. Use sigmaNegOneHalfPull to express the difference of vertical integrals as a rectangle; then RectanglePullToNhdOfPole to zoom in on a square about $0$, where the integral is evaluated by residueAtZero. That'll be our first "real" contour pull and residue! Done by @llllvvuu

[Alex Kontorovich]

Lastly, we can also continue attacking from the Fourier side; here are some of the easier targets there (from last week):
13. First Fourier Identity. This is basically a Fubini theorem type calculation, and the first step towards the Wiener-Ikehara theorem. Should be pretty simple. Done by @llllvvuu
14. Second Fourier identity Another Fubini calculation. Done by @llllvvuu
15. 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.

[Alex Kontorovich]

Also if anyone has general comments about how things are going so far, and suggestions for what could be done to improve the process, please feel free to add on here (or DM me).

Thanks for all the fantastic contributions!! Please keep them coming! :)

[Alex Kontorovich]

(Hopefully now everything is at least visible, even if I can't get it into a single message???)

[llllvvuu]

"1. isIntegrable" and "8. isHolomorphicOn2" are done as part of https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/28/

[llllvvuu]

I started working on "2. tendsto_zero_Lower": https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/34

[llllvvuu]

I bashed out the explicit uniform asymptotic since it wasn't too hard; but I wonder if I should invest into an API (unless it exists already?) for uniform asymptotics (similar to TendsToUniformly)?

In this case, TendsToUniformly would have been enough to state the sublemma (or perhaps I could have even used the pointwise asymptotic with Dini's Theorem; or maybe I'm missing something even easier). However, IsThetaUniformly could be interesting for carrying around info that can be composed with calc, add, scale, multiply, div etc

I guess I could try to use the existing IsTheta API with f(x, y) =O[\bot \times l] g(x, y) where g(x, y) = h(x)? What would make sense here?

[Terence Tao]

llllvvuu said:

I bashed out the explicit uniform asymptotic since it wasn't too hard; but I wonder if I should invest into an API (unless it exists already?) for uniform asymptotics (similar to TendsToUniformly)?

In this case, TendsToUniformly would have been enough to state the sublemma (or perhaps I could have even used the pointwise asymptotic with Dini's Theorem; or maybe I'm missing something even easier). However, IsThetaUniformly could be interesting for carrying around info that can be composed with calc, add, scale, multiply, div etc

I guess I could try to use the existing IsTheta API with f(x, y) =O[\bot \times l] g(x, y) where g(x, y) = h(x)? What would make sense here?

Certainly I think it makes sense to have some lemmas that allow one to manipulate the =O[\bot \times l] relation, e.g., the ability to integrate in the x variable and extract a =O[l] relation, and if you can spot any such lemmas that can be extracted from your code, that is worth isolating I think. At some later point one can try to respell that using some new notation like IsThetaUniformly but perhaps just =O[\bot \times l] will suffice for now.

[llllvvuu]

I'll have to take a break for a while, but I started a draft experimenting with some lemmas here (example at the end). In addition to extracting the integral big O, I've also added API to dispatch the O(1) terms more easily. The uncurrying to use the plain IsBigO API is aesthetically a bit odd but hasn't given me any issues so far.

[Alex Kontorovich]

Thanks for all your great work!

[llllvvuu]

llllvvuu said:

I started working on "2. tendsto_zero_Lower": https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/34

This is done

[Vincent Beffara]

I was hesitating to claim 3 but am arriving too late... but I am still tempted to try it as an experiment on my own using a different approach, namely defining the rectangle as a C^1 curve (with speed zero at the corners) and doing C^1 homotopy between rectangles. Still a bit artificial but not in the same direction ;-)

[Alex Kontorovich]

Dear Vincent, that would be great! I can work on something else if you'd like to try it via homotopy? (I had in mind something much simpler; one can build this up as a series of individual "cuts" in rectangles, just using intervalIntegral.integral_add_adjacent_intervals, alternating vertical and horizontal cuts where you add and subtract the same integral...)

[Vincent Beffara]

Yes, 4 cuts (which are the same up to pi/2 rotation) should suffice. I believe it would be useful to have both proofs available, the rectangle-slicing as a validation that the rectangular approach is sound and the homotopy one as kind of a connection with the rest of mathlib.

[Vincent Beffara]

None of the two being the one from the book (the one from the book is probably going through C^0 homotopy and local primitives of closed forms and lifts, but that is probably for much later ...)

[Vincent Beffara]

Some preliminary code here https://github.com/vbeffara/RMT4/blob/main/RMT4/square.lean but the eventual proof will likely be much longer than the rectangle-slicing one.

[Alex Kontorovich]

Thanks to @Paul Nelson for solving 4!

[Vincent Beffara]

Vincent Beffara said:

I was hesitating to claim 3 but am arriving too late... but I am still tempted to try it as an experiment on my own using a different approach, namely defining the rectangle as a C^1 curve (with speed zero at the corners) and doing C^1 homotopy between rectangles. Still a bit artificial but not in the same direction ;-)

So far the experiment brought more pan than anything else, piecewise C^1 is painful to manage and do homotopy with, and C^1 parameterzation of a polygon is a mess (unless I'm missing something). I'm more convinced than aver that the proof has to be either all the way towards the specific case in play with rectangle slicing, or the other way using only topology and C^0 homotopy.

Would it make sense to try to implement that within the PNT+ project?

[Terence Tao]

There is a sort of intermediate approach which I adopt for instance in https://terrytao.wordpress.com/2016/10/02/math-246a-notes-3-cauchys-theorem-and-its-consequences/ :

In all the discussion below we are integrating a fixed holomorphic function on some open set.

1. Because of the existence of local primitives, one can shift contours arbitrarily inside small balls. In particular this allows one to define contour integrals on C^0 curves by approximating them by a suitable polygonal path in a well defined manner, where the lengths of the edges in the path can be made as small as desired.
2. One can perform discrete contour shifting of polygonal paths, if all the line segments are of sufficiently small length, and each vertex of one path is sufficiently close to the corresponding vertex of the previous path, because the difference between the two polygonal contour integrals can be split up into the sum of a finite number of integrals over small quadrilaterals, whose integral vanishes due to local primitives.
3. Finally, any C^0 homotopy can be approximated by a discrete polygonal homotopy of the type required for 2 by a compactness argument.

After writing all this, though, it seems like it would be better to proceed from a more topological viewpoint, developing the theory of universal covers, monodromy, and connections of bundles, and get the homotopy version of Cauchy's theorem as a special case. I have no familiarity with the relevant portions of the Mathlib topology library though (and am certainly no topologist).

[Anatole Dedecker]

Two small comments on this:

1. I think this has been discussed a few times before, and I think it would be nice not to keep this design discussion only in this stream, because it's an interesting discussion for Mathlib too. Of course a project like this is precisely the right settings to try out multiple approaches and give us some feedback, so don't let mathlib slow you down too much, but I think some people not subscribed to this stream may want to share some thoughts.
2. I've had to think about related things recently, and I think (I have to check) that you can actually use our very general "extension by continuity" theorem, together with density of $C^1$-paths in $C^0$-paths, instead of doing concrete approximations. The key claim is that the function $\gamma \mapsto \int_\gamma f$, defined on the set of $C^1$-paths, is locally uniformly continuous for the $C^0$-distance on the domain and the discrete distance on the codomain. So it extends to all $C^0$-paths, and the obtained function is still locally constant, hence invariant by any homotopy by cutting it in small pieces. I'm not claiming this is the ideal setup, and I think it's not general enough in some sense, but at least it would save you the pain of piecewise affine things...

[Alex Kontorovich]

Indeed, @Ian Jauslin and I have a branch (which we've paused while working on PNT+) where we begin with primitives on disks (already a PR, #9598), and chain those together to show that holomorphic functions on simply connected domains have primitives...

[Alex Kontorovich]

But for PNT+ applications, usual rectangle integrals suffice; so we're not waiting for the "correct" viewpoint of connections on bundles to be in Mathlib...

[Alex Kontorovich]

I feel @Vincent Beffara's pain; we tried coding up keyhole contours and it was a horrible mess. That's when I switched to rectangles (again, just for now; hopefully eventually we'll be able to do it the "right" way...)

[Arend Mellendijk]

I'm working on 9. vertIntBoundLeft. The informal statement isn't quite right, so I'm having to slightly generalise the theorems about $\int_\R\frac{1}{|(1+t^2)(2+t^2)|^{1/2}}dt.$

[Arend Mellendijk]

Done: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/43

[Vincent Beffara]

I had some luck working with slightly more general quadrilaterals instead of rectangles (mostly to avoid going through real and imaginary parts). Namely, I can prove this (without the sorrys):

noncomputable def SegmentIntegral (f : ℂ → ℂ) (z w : ℂ) : ℂ :=
    (w - z) • ∫ t in (0:ℝ)..1, f (z + t • (w - z))

theorem cheat (hf : Differentiable ℂ f) : HasDerivAt (SegmentIntegral f z) (f w) w := by sorry

theorem cheat' (hf : Differentiable ℂ f) : HasDerivAt (λ z => SegmentIntegral f z w) (- f z) z := by

noncomputable def QuadIntegral (f : ℂ → ℂ) (w₁ w₂ w₃ w₄ : ℂ) : ℂ := SegmentIntegral f w₁ w₂ +
    SegmentIntegral f w₂ w₃ + SegmentIntegral f w₃ w₄ + SegmentIntegral f w₄ w₁

def zw (z w : ℂ) : ℂ := w.re + z.im * I

theorem rect_eq_quad : RectangleIntegral f z w = QuadIntegral f z (zw z w) w (zw w z) := by sorry

theorem loc_constant_4 {hf : Differentiable ℂ f} : HasDerivAt (QuadIntegral f z₁ z₂ z₃) 0 z := by sorry

The main cheat is the assumption that the function is analytic in the whole complex plane, which makes the statement in that case less interesting, but the proof of cheat only assumes holomorphicity on a star-like domain based at z (I had it lying around from a proof that holomorphic functions on a star-like domain have primitives) and by compactness one can always find a star-like neighborhood of a segment along which f is analytic so this should not be a huge obstacle.

[Vincent Beffara]

This avoids approximation of continuous paths by polygons (with variable numbers of edges, which I would fear would be tedious to work with in Lean).

[Vincent Beffara]

OK I managed to show this,

theorem nocheat (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hzw : segment ℝ z w ⊆ U) :
    HasDerivAt (SegmentIntegral f z) (f w) w := by

which I believe is enough to obtain 3 by quadrilateral deformation with little additional pain.

[Michael Stoll]

This looks fairly close to docs#intervalIntegral.integral_unitInterval_deriv_eq_sub .

[Vincent Beffara]

It's very close once you know that there is a primitive, yes

[Alex Kontorovich]

Arend Mellendijk said:

I'm working on 9. vertIntBoundLeft. The informal statement isn't quite right, so I'm having to slightly generalise the theorems about $\int_\R\frac{1}{|(1+t^2)(2+t^2)|^{1/2}}dt.$

Oh that was silly of me; we can pull back to $\Re s = -2$ (instead of -3/2) and then we're at distance 1 from the pole, so the same bound should work. Anyway, thanks for doing it!!

[Alex Kontorovich]

Vincent Beffara said:

OK I managed to show this,

theorem nocheat (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hzw : segment ℝ z w ⊆ U) :
    HasDerivAt (SegmentIntegral f z) (f w) w := by

which I believe is enough to obtain 3 by quadrilateral deformation with little additional pain.

Won't you run into issues more generally of figuring out what the "interior" of a polygonal path is? That's why I went with rectangles; there's it's obvious and cooked into the definition... Maybe there's better API for dealing with those real and imaginary parts...?

[Alex Kontorovich]

Vincent Beffara said:

It's very close once you know that there is a primitive, yes

Which we now do have, for discs, and work in progress for simply connected domains...

[Vincent Beffara]

Alex Kontorovich said:

Vincent Beffara said:

It's very close once you know that there is a primitive, yes

Which we now do have, for discs, and work in progress for simply connected domains...

Indeed. And the standard proof for star-convex domains is exactly showing that SegmentIntegral f z is holomorphic.

[Vincent Beffara]

Alex Kontorovich said:

Vincent Beffara said:

OK I managed to show this,

theorem nocheat (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hzw : segment ℝ z w ⊆ U) :
    HasDerivAt (SegmentIntegral f z) (f w) w := by

which I believe is enough to obtain 3 by quadrilateral deformation with little additional pain.

Won't you run into issues more generally of figuring out what the "interior" of a polygonal path is? That's why I went with rectangles; there's it's obvious and cooked into the definition... Maybe there's better API for dealing with those real and imaginary parts...?

This should not be an issue when deforming a rectangle into another rectangle, one should just need to show that the quadrilateral remains in the domain the whole time. It might well be harder than I thought...

[Alex Kontorovich]

Yes, for rectangles it's really not bad at all (though one does face issues with breaking into real/imaginary parts, and dealing with uIcc; it's a little messy, but totally doable)...

[Alex Kontorovich]

Ok, RectanglePullToNhdOfPole is done, modulo a slew of stupid lemmata called RectPull_aux1, RectPull_aux2, etc, and RectPull_rectSub1 etc. Copilot does a decent job of automating this, drastically speeding up what is already a horrible tedium. But I wonder if there's an even better way to do all of this? (@Vláďa Sedláček?) I might not wait around for the "right" way to do it; copilot just makes it bearable to repeat almost the same argument again and again...

[Vincent Beffara]

I'm not sure it would help, but did you consider slicing a rectangle into just 2 parts, one of which contains the pole, along a line at the target location, as a main lemma and then applying this lemma 4 times for the 4 sides? Directly cutting into 9 subset does sound kind of tedious to do. Ah sorry I was reading an old version of the file

[Alex Kontorovich]

Yep, that's exactly what happens now. But there are still so many tedious inclusions to verify about where exactly the pole wound up...

[Vincent Beffara]

The nine pieces are "obviously" (almost) disjoint and the pole is "obviously" in the small one so it is "obviously" not in the others ... the current file is indeed a bit painful to look at :-(

[Alex Kontorovich]

Any suggestions for how to make Lean see that it's "obvious"...?

[Vláďa Sedláček]

I have a 36-line proof of RectPull_rectSub1(which I'm sure can be optimized further). I'll try to generalize it to the other cases, or maybe see if it could be made into a uniform tactic.

[Alex Kontorovich]

Are you using RectSubRect or RectSubRect'?...

[Alex Kontorovich]

There're only four of those; there're sixteen of the RectPull_aux1s... After applying ContinuousOn.intervalIntegrable, it should be very similar to ContinuousOn.im_aux_1 from #9598...

[Alex Kontorovich]

Maybe they're the ones better to automate somehow...

[Vincent Beffara]

BTW, I realized that the hypothesis here is HolomorphicOn f (Rectangle z w \ {p}) rather than holomorphic on an open set containing Rectangle z w \ {p}. Would the version on an open set be sufficient for applications later?

[Alex Kontorovich]

Hmmm sure, you can make the domain of holomorphicity larger... but why would you want to? (I'm missing something)

[Vincent Beffara]

Because that would be the natural setup for homotopy arguments (you would like the rectangle boundary to be a continuous path inside the open set where the function is holomorphic)

[Alex Kontorovich]

That reminds me: @Vincent Beffara, did we ever show you how far we got with integrals of holomorphic functions over homotopic curves are equal? There's some decent progress here: https://github.com/ianjauslin-rutgers/lean-complex-has_primitives/blob/AK_branch/HasPrimitives/PrimitivesOfSimplyConnected.lean, see curvInt_eq_of_diffHomotopic (Progress paused until PNT+ is done...)

[Alex Kontorovich]

Based on your RMT work, of course

[Alex Kontorovich]

In particular, do we have something close to DifferentiablyHomotopic_of_OpenHomotopic there ...?

[Alex Kontorovich]

@Vláďa Sedláček, I just merged mem_Rect which might be useful?... (Should've thought to add it before; likely quite a lot can be refactored with it...)

[Alex Kontorovich]

FYI: I'll try my luck at diffBddAtZero next (10). I can't seem to edit the zulip post without getting that same annoying "Error editing message: Unable to render message" ...

[llllvvuu]

I'll try golfing the aux stuff. fun_prop works for one of the side conditions: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/52/files

The MapsTo part I'm not sure if there is a tactic but I'll see if I can combine some of the aux lemmas and/or extract something involving MapsTo uIcc Rectangle

[Alex Kontorovich]

I was thinking it might be useful to keep track of the fact that, e.g., z.re < p.re - c < p.re + c < w.re, and same for imaginary parts... But go ahead, @llllvvuu, I'm curious what you'll come up with...

[llllvvuu]

Well so far, I've pushed the hard work to RectPull_rectSub1 et al:

lemma mapsTo_left_edge (z w : ℂ) :
    MapsTo (fun (y : ℝ) => ↑z.re + ↑y * I) [[z.im, w.im]] (Rectangle z w) :=
  fun _ hx ↦ ⟨by simp, by simp [hx]⟩

attribute [fun_prop] Complex.continuous_ofReal
lemma RectPull_aux1 {f : ℂ → ℂ} {z w p : ℂ} (zRe_lt_wRe : z.re < w.re) (zIm_lt_wIm : z.im < w.im)
    {c : ℝ} (cpos : 0 < c) (hc : Rectangle (-c - I * c + p) (c + I * c + p) ⊆ Rectangle z w)
    (fCont : ContinuousOn f (Rectangle z w \ {p})) :
    IntervalIntegrable (fun (y : ℝ) ↦ f (z.re + y * I)) volume z.im (p.im - c) := by
  refine (fCont.comp (by fun_prop) ?_).intervalIntegrable
  refine MapsTo.mono_right ?_ (RectPull_rectSub1 zRe_lt_wRe zIm_lt_wIm cpos hc)
  convert mapsTo_left_edge _ _ <;> simp

Your comment could become very relevant if/when I also golf the rectSub lemmas. Maybe there is some general lemma that can be derived from p ∈ Rectangle (-c - I * c + p) (c + I * c + p), i.e. (h1 : Rectangle a b ⊆ Rectangle c d) (h2 : p ∈ Rectangle a b) : Rectangle ?? ?? ⊆ Rectangle c d \ {p}

[llllvvuu]

I got it sorry-free: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/54

I added some lemmas that help, but there is still repetition. I think this is about as much time as I have for now though.

[Vincent Beffara]

I would like to have a go at ResidueTheoremOnRectangleWithSimplePole (and try some refactoring of the file), but it is not listed as claimable. Is anyone working on it or planning to do so?

[Alex Kontorovich]

Oh that's (5), right? @Paul Nelson and I are hacking away at that one.

[Alex Kontorovich]

in fact, we're looking to develop API for things like RectangleBorderIntegrable so that we no longer need 16 auxiliary integrability statements... (Coming soon...)

[Vincent Beffara]

Alex Kontorovich said:

in fact, we're looking to develop API for things like RectangleBorderIntegrable so that we no longer need 16 auxiliary integrability statements... (Coming soon...)

That would be nice :-)

[Alex Kontorovich]

You're more than welcome to join us, if you'd like? We just finished a session - Paul, do you want to point Vincent to where your fork is?

[Paul Nelson]

sure, https://github.com/ultronozm/PrimeNumberTheoremAnd

[Alex Kontorovich]

Great thanks; so Vincent, you can see some progress here, around line 317, and more starting line 1067...

[llllvvuu]

Alex Kontorovich said:

in fact, we're looking to develop API for things like RectangleBorderIntegrable so that we no longer need 16 auxiliary integrability statements... (Coming soon...)

Brilliant! I can golf down my work from yesterday

[Vláďa Sedláček]

(6), i.e. RectangleIntegral_tendsTo_UpperU and RectangleIntegral_tendsTo_LowerU , are still up for the taking, right? I can try those.

[Alex Kontorovich]

Great, thanks Vlada! They're yours.

[llllvvuu]

llllvvuu said:

Alex Kontorovich said:

in fact, we're looking to develop API for things like RectangleBorderIntegrable so that we no longer need 16 auxiliary integrability statements... (Coming soon...)

Brilliant! I can golf down my work from yesterday

This is done (0 aux lemmas, also added/golfed a few other more general lemmas): https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/57

[llllvvuu]

draft started for first_fourier:
https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/58/files

[Alex Kontorovich]

llllvvuu said:

This is done (0 aux lemmas, also added/golfed a few other more general lemmas): https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/57

Beautiful!! You read my mind (and executed better than I could have)

[Alex Kontorovich]

It seems to me that the concept of Square is quite useful too. Shall we add some API for it? I just pushed a start...

[llllvvuu]

Alex Kontorovich said:

It seems to me that the concept of Square is quite useful too. Shall we add some API for it? I just pushed a start...

It sounds useful for @Vincent Beffara on ResidueTheoremOnRectangleWithSimplePole. I also suspect the bulk of RectanglePullToNhdsOfPole (i.e. the part after filter_upwards and intro) will want to be factored out into a lemma that equates arbitrary nested rectangles instead of just the Eventually. That way we can precisely pull in and out.

[Alex Kontorovich]

Oh, while Rectangle is symmetric in z and w, RectangleIntegral is not, because IntervalIntegral is oriented…. So rectangleIntegral_symm needs a minus sign…

[llllvvuu]

PR has been fixed

[Alex Kontorovich]

And FYI there's a bit of API for uIoo in #9598, in case it might be useful...

[llllvvuu]

llllvvuu said:

draft started for first_fourier:
https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/58/files

this ("13. First Fourier Identity") is finished

[Arend Mellendijk]

I'm trying out 11. sigmaNegOneHalfPull

[Arend Mellendijk]

Here it is: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/63
I originally missed DiffVertRect_eq_UpperLowerUs, but combining ideas did lead to a nice golf.

[llllvvuu]

started residuePull1: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/65

[llllvvuu]

llllvvuu said:

started residuePull1: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/65

done (build fixed by other PR)

[Vincent Beffara]

Based on the work by @Alex Kontorovich and @Paul Nelson I got ResidueTheoremOnRectangleWithSimplePole almost sorry-free (and also eventually-free, because in fact it does not use RectanglePullToNhdOfPole directly)
https://github.com/ultronozm/PrimeNumberTheoremAnd/pull/1

[Vincent Beffara]

It boils down to

theorem ResidueTheoremInRectangle {z w p c : ℂ} (h : Rectangle z w ∈ 𝓝 p) :
    RectangleIntegral' (λ s => c / (s - p)) z w = c

which is very close to ResidueTheoremAtOrigin, the blueprint indicates a proof of this by shrinking to a square neighborhood and using ResidueTheoremAtOrigin but it feels possible to instead adapt the proof of ResidueTheoremAtOrigin to the more general case instead.

[llllvvuu]

started a draft on "14. Second Fourier identity":
https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/66

[llllvvuu]

Vincent Beffara said:

Based on the work by Alex Kontorovich and Paul Nelson I got ResidueTheoremOnRectangleWithSimplePole almost sorry-free (and also eventually-free, because in fact it does not use RectanglePullToNhdOfPole directly)
https://github.com/ultronozm/PrimeNumberTheoremAnd/pull/1

might be worth re-opening the PR to AlexKontorovich:main as GitHub will show the (much smaller) real diff (i.e. git diff origin/main vbeffara/pn_main)

[llllvvuu]

@Vincent Beffara the following suffices for HolomorphicOn.rectangleBorderIntegrable':

theorem Set.left_not_mem_uIoo {a b : ℝ} : a ∉ Set.uIoo a b :=
  fun ⟨h1, h2⟩ ↦ (left_lt_sup.mp h2) (le_of_not_le (inf_lt_left.mp h1))

theorem Set.right_not_mem_uIoo {a b : ℝ} : b ∉ Set.uIoo a b :=
  fun ⟨h1, h2⟩ ↦ (right_lt_sup.mp h2) (le_of_not_le (inf_lt_right.mp h1))

theorem Set.ne_left_of_mem_uIoo {a b c : ℝ} (hc : c ∈ Set.uIoo a b) : c ≠ a :=
  fun h ↦ Set.left_not_mem_uIoo (h ▸ hc)

theorem Set.ne_right_of_mem_uIoo {a b c : ℝ} (hc : c ∈ Set.uIoo a b) : c ≠ b :=
  fun h ↦ Set.right_not_mem_uIoo (h ▸ hc)

theorem not_mem_rectangleBorder_of_rectangle_mem_nhds {z w p : ℂ} (hp : Rectangle z w ∈ 𝓝 p) :
    p ∉ RectangleBorder z w := by
  refine Set.disjoint_right.mp (rectangleBorder_disjoint_singleton ?_) rfl
  have h1 := rectangle_mem_nhds_iff.mp hp
  exact ⟨Set.ne_left_of_mem_uIoo h1.1, Set.ne_right_of_mem_uIoo h1.1,
    Set.ne_left_of_mem_uIoo h1.2, Set.ne_right_of_mem_uIoo h1.2⟩

theorem HolomorphicOn.rectangleBorderIntegrable' {f : ℂ → ℂ} {z w p : ℂ}
    (hf : HolomorphicOn f (Rectangle z w \ {p}))
    (hp : Rectangle z w ∈ nhds p) : RectangleBorderIntegrable f z w :=
  hf.continuousOn.rectangleBorderNoPIntegrable (not_mem_rectangleBorder_of_rectangle_mem_nhds hp)

[llllvvuu]

I proved your new theorem @Vincent Beffara : https://github.com/vbeffara/PNT/pull/1

[Vincent Beffara]

Thanks @llllvvuu ! PR here https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/67 and the proof of ResidueTheoremOnRectangleWithSimplePole is completely sorry-free.

[llllvvuu]

llllvvuu said:

started a draft on "14. Second Fourier identity":
https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/66

this is done as well

[Alex Kontorovich]

Argh! I'm still getting that annoying "Error editing message: Unable to render message", so can't update the outstanding tasks list. Anyway, it's time for a new one. I think at the speed with which you guys are solving goals (I've had to download github and zulip to my phone, and approve pull requests while chauffeuring my kids over the weekend!...), I should release my claim on 10. diffBddAtZero, and start making more precise targets in the blueprint. I made a bit of progress on diffBddAtZero, but there's some interesting API that needs to be developed (I think) between bddAbove and IsBigO.

[Alex Kontorovich]

Here's an interesting bit of API:

import Mathlib

open Topology

lemma DifferentiableAt.bddAboveOnSquare {f : ℂ → ℂ} {z₀ : ℂ} (fDiffble : DifferentiableAt ℂ f z₀) :
    ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove ((norm ∘ (fun (z : ℂ) ↦ (f z - f z₀) / (z - z₀))) '' Square z₀ c) := by
  have := fDiffble.hasDerivAt
  rw [hasDerivAt_iff_tendsto] at this
  have := @Tendsto.isBigO_one (h := this) ℂ _ _ _ _
  sorry

[Alex Kontorovich]

Basically one needs (which should be useful elsewhere as well) that Squares interlace with metric balls, so that a Tendsto argument with s in 𝓝 0 can be converted into an eventually for s in a square with side length c in 𝓝[>]0.... Does that make sense?

[Alex Kontorovich]

Then one applies this to $s\mapsto x^s$, to see that $x^s/s - 1/s$ is bounded near 0. (Then add that to $x^s/(1+s)$ being bounded near zero.)

[Alex Kontorovich]

The same argument will work for diffBddAtNegOne...

[Vincent Beffara]

Probably an interesting spelling for interlacement would be to say

theorem nhds_basis_square (p : ℂ) : HasBasis (𝓝 p) (λ c => 0 < c) (λ c => Square p c) := sorry

rather than explicit comparison with metric balls

[Vincent Beffara]

theorem nhds_basis_square (p : ℂ) : HasBasis (𝓝 p) (0 < ·) (Square p ·) := by
  apply Filter.HasBasis.to_hasBasis' Metric.nhds_basis_closedBall <;> intro c hc
  · refine ⟨c / Real.sqrt 2, div_pos hc (Real.sqrt_pos.mpr zero_lt_two), ?_⟩
    convert square_subset_closedBall p (c / Real.sqrt 2)
    field_simp [abs_div, abs_eq_self.mpr hc.le, abs_eq_self.mpr (sqrt_nonneg 2)]
  · apply rectangle_mem_nhds_iff.mpr
    simp [mem_reProdIm, uIoo, hc.ne, hc.ne.symm]

[Anatole Dedecker]

Would it be easier to use the homeomorphism between $\mathbb{C}$ and $\mathbb{R}\times\mathbb{R}$ and pull back the filter basis?

[llllvvuu]

I implemented @Anatole Dedecker 's suggestion here: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/70/files

[Anatole Dedecker]

We should have some filter magic to make that even shorter, but it’s probably not the most fun task of the project. Do you want me to have a go at golfing it tomorrow ?

[llllvvuu]

Go for it!

[Patrick Massot]

How can you write “filter magic” and “not fun” in the same sentence? What happened to you while I was away??

[Anatole Dedecker]

I meant "not fun if you don’t know the tricks" of course! Although one could maybe argue that I’m trying to keep the fun for myself…

[Patrick Massot]

I understand better now.

[llllvvuu]

I managed to golf it from 12 to 9 lines. That's probably the limit of my filter skills :woozy_face:

[llllvvuu]

I've got something cooking for diffBddAtZero https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/71/files should be finished up soon

[llllvvuu]

llllvvuu said:

I've got something cooking for diffBddAtZero https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/71/files should be finished up soon

done

[Vincent Beffara]

As an experiment I wrote a direct proof of this:

theorem ResidueTheoremInRectangle' {z w p c : ℂ} (zRe_le_wRe : z.re ≤ w.re) (zIm_le_wIm : z.im ≤ w.im)
    (pInRectInterior : Rectangle z w ∈ 𝓝 p) : RectangleIntegral' (λ s => c / (s - p)) z w = c := by

(which is exactly ResidueTheoremInRectangle without the fHolo assumption, which derives from the others anyway). Direct in the sense, compute the 4 side integrals in terms of logs and arctangents and show explicit cancellation using mostly ring_nf interlaced with simp. The proof is not going to win any beauty contest but it is rather short (about 90 lines total, which is similar to that of ResidueTheoremAtOrigin) and not as painful as I would have imagined at first, and it does not rely on RectanglePullToNhdOfPole or rectangle-slicing at all.

https://github.com/vbeffara/PNT/blob/af0f9203291ff98be39b57ef190eda9c48f4589a/PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean#L978

[Alex Kontorovich]

Curiously, that was my first version (on paper, when designing the blueprint)! But I didn't want to deal with complex logs, and eventually discovered that everything just perfectly cancels out for squares!... (So then one only needs arctan and real integrals... Hence the cutting of rectangles down to squares...)

[Alex Kontorovich]

I'm in the process of making a new list of Tasks and filling out more of the blueprint. (But hosting a visitor all day today, and traveling to give a colloquium all day tomorrow; will try to get it up and running as soon as I can...)

[Vláďa Sedláček]

Vláďa Sedláček said:

(6), i.e. RectangleIntegral_tendsTo_UpperU and RectangleIntegral_tendsTo_LowerU , are still up for the taking, right? I can try those.

This is done: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/72

[Vincent Beffara]

Alex Kontorovich said:

Curiously, that was my first version (on paper, when designing the blueprint)! But I didn't want to deal with complex logs, and eventually discovered that everything just perfectly cancels out for squares!... (So then one only needs arctan and real integrals... Hence the cutting of rectangles down to squares...)

Only real logs :-) I will see if it makes sense to refactor all the ResidueTheoremAtOrigin_aux** lemmas.

On a semi-related theme: is there an established or natural place in blueprints to put "strategy comments" like this? Typically we chose this avenue to formalize the result, another one would have been to do this, that and the other thing instead but that would lead to such and such technical issue which our approach is bypassing.

[Alex Kontorovich]

Very good question! I suppose it never hurts to add some auxiliary comments/"notes to self" in the blueprint...? As is, we're already duplicating (or rather, triplicating) work by having three different approaches to PNT itself...

[llllvvuu]

Technically PerronFormula.lean only uses the result on squares since it is already pulling the rectangle to get the bddAbove, and it could even bypass that pull by adjusting sigmaNegOneHalfPull to cut down to arbitrary squares. The more lemmas the merrier though, I think.

[Vláďa Sedláček]

I'll go for residuePull2 next if nobody's working on it yet.

[Vláďa Sedláček]

Vláďa Sedláček said:

I'll go for residuePull2 next if nobody's working on it yet.

Done: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/76 (thanks to @Ian Jauslin for a helpful discussion). PerronFormula is now sorry-free.

[llllvvuu]

I have a golf that removes the dependency on U integral work, although I keep the general U integral lemmas: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/77