PRs

Stream: Sphere packing in 8 dimensions

[Sidharth Hariharan]

Hi all,

Recently, there have a number of people making PRs co-authored by Aristotle and Gauss. While these contributions really have been fantastic (thank you!), I'd like to request that the people running these models on our repository first take a look at the PR queue and only run them on files that aren't being worked on in other PRs. We've already had two instances of duplicate/redundant PRs. If you'd like to help with PRs still in progress, then please contact the PR authors and see if you can help them.

On another note, there are a number of PRs that I would like to review, but I am quite busy for the next few days. I will try and get some of them merged at ItaLean next week, especially the ones whose authors will be there in-person.

Thank you!

[Seewoo Lee]

Could anyone review this #PR193? (and can we use this thread for a purpose of asking review?)

[Tito Sacchi]

@Sidharth Hariharan @Cameron Freer Regarding the integrability conditions for the double zeroes PR, I think that the required results are the following:

1. Integrability on infinite intervals of the integrals in Proposition 4.4.6 of Sid's master thesis. These are basically the integrals that appear in d. Since the techniques used to prove integrability are always the same, I think that the best option would be to have a general lemma that can be invoked in each of the relevant cases. Do you think that's possible?
   The relevant goals should be the following, and some of them are equivalent (you can get one from the other by changing variables, but Lean still requires to prove integrability separately):

• IntegrableOn (fun t ↦ I * φ₀'' (-1 / (I * ↑t)) * (I * ↑t) ^ 2 * cexp (I * ↑π * ↑r * (I * ↑t))) (Ici 0) volume
• IntegrableOn (fun t ↦ φ₀'' (-1 / (↑t * I)) * (↑t * I) ^ 2 * cexp (↑π * I * ↑r * (-1 + ↑t * I))) (Ioi 1) volume
• IntegrableOn (fun t ↦ φ₀'' (-1 / (↑t * I + 1)) * (↑t * I + 1) ^ 2 * cexp (↑π * I * ↑r * (↑t * I))) (Ioi 1) volume
• IntegrableOn (fun t ↦ φ₀'' (-1 / (↑t * I)) * (↑t * I) ^ 2 * cexp (↑π * I * ↑r * (1 + ↑t * I))) (Ioi 1) volume
• IntegrableOn (fun t ↦ φ₀'' (-1 / (↑t * I - 1)) * (↑t * I - 1) ^ 2 * cexp (↑π * I * ↑r * (↑t * I))) (Ioi 1) volume
• Integrable (fun t ↦ I * (φ₀'' (-1 / (↑t * I)) * (↑t * I) ^ 2 * cexp (↑π * I * ↑r * (-1 + ↑t * I)))) (volume.restrict (Ici 0))
  We should try to prove a general lemma for integrability on Ioi 0 of integrands similar to φ₀'' (-1 / (a + I * t)) * (a + I * t) ^ 2 * cexp (π * I * r * (I * t + b)).

2. Additionally, to apply Cauchy-Goursat some continuity and differentiability hypotheses are required but they should already be somewhere in the codebase, I will look for them in the next few days.

3. Vanishing of the integrands that are involved in Cauchy-Goursat as Im(z) approaches infinity. This should require the bounds on page 41 of Sid's thesis. These will probably show up while proving integrability, but please state them as separate lemmas so that I can fill in the hypotheses for Cauchy-Goursat.
   The relevant goals are the following:

• ∀ ε > 0, ∃ M, ∀ (z : ℂ), M ≤ z.im → ‖φ₀'' (-1 / (z - 1)) * (z - 1) ^ 2 * cexp (↑π * I * ↑r * z)‖ < ε
• ∀ ε > 0, ∃ M, ∀ (z : ℂ), M ≤ z.im → ‖φ₀'' (-1 / (z + 1)) * (z + 1) ^ 2 * cexp (↑π * I * ↑r * z)‖ < ε
  (These could probably be expressed more concisely using Filters and atTop, if you prefer more idiomatic and mathlib-like code)

Let me know if this summary is complete enough, and thanks for your work!

[Cameron Freer]

@Tito Sacchi Thanks for the detailed description -- that all makes sense for now. I'll keep you posted on what I separate from and add to 260/261, and will let you know if I have any questions.

[Sidharth Hariharan]

Thank you very much for this @Tito Sacchi! Makes sense! I'll have a closer look at these

[Cameron Freer]

@Sidharth Hariharan @Tito Sacchi I've completed an initial pass at this; please let me know whether something like the following PRs work for what you need in spherepacking#229.

• spherepacking#288: Continuity and decay helpers in CuspPath.lean, RealDecay.lean
  • spherepacking#296: PhiBounds, S-transform bounds, integrand infrastructure in ContourEndpoints.lean (merge 288 first)
    • spherepacking#297: bounds, integrableOn_goal1-6 in VerticalIntegrability.lean (merge 296 first; independent of 298)
    • spherepacking#298: Vanishing lemmas (incl. thesis Lemma 4.4.5) in VerticalVanishing.lean (merge 296 first; independent of 297)

If we do divide it up this way, then I think all four of these would be needed before the spherepacking#229 double zeros proof, but I will refactor what remains of spherepacking#260 and spherepacking#261 to separately build on 298 independently of 297 and 229.

[Tito Sacchi]

@Cameron Freer the PR looks great, thanks! I am filling in the sorries for integrability. Just one thing, there is a goal I forgot to include in my last message, which is the following:
IntegrableOn (fun t ↦ I * (φ₀'' (-1 / (↑t * I)) * (↑t * I) ^ 2 * cexp (↑π * I * ↑r * (1 + ↑t * I)))) (Ici 0) volume
It is very similar to a goal you have already proved, but with 1 instead of -1.

[Cameron Freer]

@Tito Sacchi Thanks, I've added a 7th goal in spherepacking#297 along with a def ContourEndpoints.phiBounds (itself with a sorry) that I think should unblock you in using these in spherepacking#229.

[Tito Sacchi]

Thanks, great!

[Cameron Freer]

@Tito Sacchi @Sidharth Hariharan I eliminated the hypotheses from spherepacking#296 and spherepacking#297 that we discussed today, using the new PhiBounds architecture that Tito suggested, now introduced in spherepacking#296 (with some sorries).

Separately, these sorries are filled in spherepacking#304 (using stubbed sorry results from spherepacking#268) -- I think this should be reviewable independently from both of the chains 288->296->(297+298)->229 and 266->267->268.

[Tito Sacchi]

I'm filling in all the sorries and the most painful are definitely the ones related to differentiability and continuity of integrands on the upper half plane, because fun_prop doesn't work well with H. Do you know if we already have any auxiliary lemmas in our codebase?

My goals look pretty much like this:
DifferentiableOn ℂ (fun z ↦ φ₀'' (-1 / (z + r))) (Set.univ ×ℂ Ioi 0)

[Tito Sacchi]

I have successfully filled in all sorries for integrability and now I'm working on vanishing endpoints, but I think that Cameron's lemmas prove something slightly different from the goal I mentioned above, which is:

∀ ε > 0, ∃ M, ∀ (z : ℂ), M ≤ z.im → ‖φ₀'' (-1 / (z - 1)) * (z - 1) ^ 2 * cexp (↑π * I * ↑r * z)‖ < ε

If I have understood this right, this means that for z = x + I y:
||φ₀'' (-1 / (z - 1)) * (z - 1) ^ 2 * cexp (↑π * I * ↑r * z)|| tends to 0 when y goes to +Inf uniformly on x ∈ R. i.e.:
|| integrand z || is arbitrarily small for all z with z.im above M.

But lemmas tendsto_φ₀_integrand_plus_one and tendsto_φ₀_integrand_minus_one prove that for two specific values of x (namely +1 and -1), || integrand z || tends to 0 when y goes to +Inf.

@Sidharth Hariharan Can you confirm that Cauchy-Goursat requires this kind of "uniform convergence" when seeing the integrand as a function of two real variables (real part and complex part)? It makes sense to me, since we are moving an horizontal contour upwards.

@Cameron Freer Do you think you could extend your lemmas to include this stronger condition? One possible way of doing this (if you like filters) would be creating a custom atTop-like filter for the complex plane which has sets { z ∈ C | z.im > M} as a basis.

[Cameron Freer]

@Tito Sacchi I was able to add this to spherepacking#296, extending

  tendsto_verticalIntegrandX_atTop (x r : ℝ) (hr : 2 < r) :
      Tendsto (fun t => verticalIntegrandX x r t) atTop (𝓝 0)

to the following:

  uniform_vanishing_verticalIntegrandX (r : ℝ) (hr : 2 < r) :
      ∀ ε > 0, ∃ M : ℝ, ∀ x t : ℝ, M ≤ t → ‖verticalIntegrandX x r t‖ < ε

The bound verticalBound r t already didn't depend on x at all -- since ‖integrand(x,t)‖ ≤ bound(t) for all x, and bound(t) → 0 as t → ∞, we got uniform vanishing for free.

See 4ab1b29 (subsequently golfed in the following two commits).

Does this work for what you need?

[Tito Sacchi]

It should, thanks! I will try to fill in the last sorries tonight or tomorrow.

[Cameron Freer]

Thanks! (I also added the filter version, along the lines you suggested.)

[Cameron Freer]

See also spherepacking#305, an independent PR that proves φ₀''_holo, which also fills your lemmas φ₀''_differentiable and φ₀''_continuous as one-liners.

[Tito Sacchi]

I just filled in those using φ ₀''_holo from ComplexIntegrands.lean, thanks! I guess the sorry there will be filled in when spherepacking#305 will be merged (probably after spherepacking#229).

[Sidharth Hariharan]

Tito Sacchi said:

Sidharth Hariharan Can you confirm that Cauchy-Goursat requires this kind of "uniform convergence" when seeing the integrand as a function of two real variables (real part and complex part)? It makes sense to me, since we are moving an horizontal contour upwards.

Sorry for the late reply! I'm fairly certain that we need this uniform condition on the region between the contours that are being defined.

[Sidharth Hariharan]

I'll have a look soon!

[Tito Sacchi]

@Sidharth Hariharan I think that our proof of Cauchy-Goursat in OpenRectangular.lean requires a much stronger condition than needed: it requires that the integrand vanishes for every Re[z] in R as Im[z] -> +Inf. Since we are deforming contours that have a bounded real part, vanishing for Re[z] in Icc -1 1 should suffice.

The real part of zactually matters, since Cameron's lemmas rely on a uniform bound that holds for Re[z] in Icc -1 1 (see uniform_vanishing_topEdgeIntegrand in ContourEndpoints.lean in spherepacking#296).

I think we have two options:

• We could modify our proof of Cauchy-Goursat to require a looser condition, or
• As a workaround, I could define an auxiliary function g that is zero when Re[z] not in Icc -1 1 and matches our integrand when Re[z] in Icc -1 1, and apply Cauchy-Goursat to the function g, that obviously vanishes uniformly on R.

The second option is probably the quicker one. Generalizing Cauchy-Goursat is probably the more idiomatic, but it will take some more time especially for someone who is not familiar with our current formalisation of the proof.
Let me know what you prefer.

[Sidharth Hariharan]

I agree, the conditions in our version of Cauchy-Goursat is stronger than it needs to be. We only need that for $z$ with $\Re(z)$ lying between the vertical contours. In the case at hand, that's $[-1, 1]$.

[Sidharth Hariharan]

As an aside, though, it is actually true that the integrands vanish on all vertical contours as $\Im(z) \to \infty$

[Sidharth Hariharan]

Not even vertical contours. There's no direction involved. The point of the condition right now is that as long as your imaginary part is tending to infinity, no matter what's going on with your real part, the integrand will vanish

[Sidharth Hariharan]

But this can easily be modified to include a condition on the real part: instead of $\forall z \in \mathbb{C}$, we can just say $\forall z$ with real part lying between your contours

[Tito Sacchi]

Should we open another PR to work on Cauchy-Goursat and adjust the required condition? It could make sense to handle Cauchy-Goursat and the double zeroes lemmas separately.

[Sidharth Hariharan]

I agree. I'll try and do it later today or over the weekend.

[Sidharth Hariharan]

We actually might not need to do it ourselves because I think the exact result we need was proved in the PNT+ project...

[Tito Sacchi]

Thanks, great! No hurry:+1: