random PR: [WIP] feat(number_theory/geometry_of_numbers):...

Stream: triage

[Random Issue Bot]

Today I chose PR 2819 for discussion!

[WIP] feat(number_theory/geometry_of_numbers): Minkowski's theorem
Created by @Alex J Best (@alexjbest) on 2020-05-25
Labels: WIP, help wanted, incomplete, not-ready-to-merge

Is this PR still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose PR 2819 for discussion!

[WIP] feat(number_theory/geometry_of_numbers): Minkowski's theorem
Created by @Alex J Best (@alexjbest) on 2020-05-25
Labels: WIP, help wanted, incomplete, not-ready-to-merge

Is this PR still relevant? Any recent updates? Anyone making progress?

[Alex J. Best]

This is still relevant. There have been a lot of changes to measure theory recently, the addition of the haar measure for instance, that I hope now makes it close to possible to complete this pr. It is undoubtedly quite broken right now though.
There are a couple of measure theoretic facts that might be needed for this still that I'm not sure are in mathlib yet:

• n-fold product measures (perhaps this isn't needed in generality as we work with R^n, not sure)
• scaling of this measure under dilation of a set (not sure exactly what hypotheses are needed / what generality it holds in)
• every convex set is measurable

@Floris van Doorn @Yury G. Kudryashov may be able to say more about these

[Rob Lewis]

Random Issue Bot already repeating itself, heh

[Mario Carneiro]

can we give it some short term memory?

[Rob Lewis]

Yeah, it's probably easiest to check the most recent posts in #triage or something like that.

[Rob Lewis]

A little hard to test without some history, but it should now ignore any issue /PR that has a #triage thread with activity in the last two weeks.

[Rob Lewis]

I moved the issue number to the beginning of the topic title, but this needed to happen anyway since it'll usually get cut off like in this one