Whitney/Borel Lemma Usage

Stream: Sphere packing in 8 dimensions

[Matthew Cushman]

Hi, @Sidharth Hariharan (or anyone else), could you point me to where in the blueprint or in the thesis use of the lemma on even smooth functions would be used? I am interested in looking into whether extending this to Schwarz as discussed would be helpful or not as we discussed on Tuesday. It seems related (a partial converse) to theorem 3.1.6 from the thesis, but I don't see exactly where the converse would be useful yet.

[Sidharth Hariharan]

The problem is that the thesis takes a slightly different approach to the lemma than what we want to do. In the thesis my idea was to compose with norm squared, but now we're just composing with the norm. I have a sorry-free proof that if $f : \mathbb{R} \to \mathbb{R}$ is Schwartz, then $f(\Vert x \Vert^2) : \mathbb{R}^n \to \mathbb{R}$ is Schwartz as well.

[Sidharth Hariharan]

I don't think it would be particularly valuable at this stage to generalise to Schwartz functions. The reason I say this is I think you thought of a significantly simpler fix: define our $I_j$ to be those integrals (where we have just an $e^{i \pi r z}$ and not an $e^{i \pi r^2 z}$) times a smooth function that's identically $0$ on $(-\infty, -1]$ (or something like this) and identically $1$ on $[0, \infty)$. This would render them Schwartz and allow us to compose with the norm squared to get Schwartz functions from $\mathbb{R}^8$ to $\mathbb{R}$.

[Matthew Cushman]

OK, thanks -- I have a construction of such a function formalized, I can make a PR out of it in advance of tomorrow if you'd like

[Sidharth Hariharan]

That would be great, thank you!

[Matthew Cushman]

I'll work on this (sorry didn't get to it yet, and won't be able to make it to the packathon today)