!3#18863 Unfolding Trick

Stream: PR reviews

[Scott Morrison]

@Alex Kontorovich, your mathlib3 PR !3#18863 currently has a merge conflict. Assuming you would still like this merged to mathlib3 so you can forward port it, would you mind merging master?

(And if you'd prefer to move it direct to mathlib4, that's of course fine too. :-)

[Alex Kontorovich]

Ok thanks; it was just a matter of merging (I think; building now).

[Alex Kontorovich]

Actually I'm going to try to move it directly to mathlib4. Shouldn't be that hard... (Famous last words)

[Jireh Loreaux]

@Alex Kontorovich one benefit of having it merged in mathlib3 is that you can just get mathport output directly instead of needing to run it yourself. This is especially relevant for your PR because you modify several mathlib files, so it's probably something you want.

[Scott Morrison]

I agree that mathport will be helpful here. I left a trivial comment, and had a superficial look. It's not really my corner of the library, so it would be great if another reviewer could have a look at this and hopefully merge soon.

[Scott Morrison]

@Alex Kontorovich, I've just delegated this PR. There's a trivial request about formatting of comments. :-)

[Alex Kontorovich]

Do you know when mathport will run again? It doesn't seem to have yet. Thanks!

[Jireh Loreaux]

It only runs once a day on mathlib3. So you should have it tomorrow.

[Alex Kontorovich]

FYI @Heather Macbeth and I just did it by hand; it's now #6223

[Kevin Buzzard]

Is this unfolding trick something which could be used to that a convex symmetric set in R^n with volume bigger than 2^n contains a nontrivial lattice point? (hence a route to Hasse-Minkowski via geometry of numbers)

[Mario Carneiro]

silly question: is every convex set in R^n measurable? I think it might not be Borel-measurable because IIUC a unit disk including an arbitrary subset of the boundary is convex, but that's measure zero away from the open disk so it is still lebesgue measurable

[Alex Kontorovich]

Kevin Buzzard said:

Is this unfolding trick something which could be used to that a convex symmetric set in R^n with volume bigger than 2^n contains a nontrivial lattice point? (hence a route to Hasse-Minkowski via geometry of numbers)

I actually had in mind things like developing non-holomorphic Eisenstein series, aiming (eventually) for Rankin-Selberg L-functions, trace formulae, etc. A shorter-term goal would be a general Poisson summation (perhaps eventually adelic, Tate's thesis...). But certainly Minkowski would be a nice application too...

[Alex Kontorovich]

Mario Carneiro said:

silly question: is every convex set in R^n measurable? I think it might not be Borel-measurable because IIUC a unit disk including an arbitrary subset of the boundary is convex, but that's measure zero away from the open disk so it is still lebesgue measurable

Yes, indeed: https://math.stackexchange.com/questions/207609/the-measurability-of-convex-sets

[Oliver Nash]

Also docs#Convex.nullMeasurableSet

[Yaël Dillies]

Kevin Buzzard said:

Is this unfolding trick something which could be used to that a convex symmetric set in R^n with volume bigger than 2^n contains a nontrivial lattice point? (hence a route to Hasse-Minkowski via geometry of numbers)

We already have that. It was !3#2770