Zulip Chat Archive

Stream: triage

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


view this post on Zulip Random Issue Bot (Oct 31 2020 at 14:13):

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?

view this post on Zulip Random Issue Bot (Nov 01 2020 at 14:14):

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?

view this post on Zulip Alex J. Best (Nov 01 2020 at 17:48):

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

view this post on Zulip Rob Lewis (Nov 01 2020 at 18:37):

Random Issue Bot already repeating itself, heh

view this post on Zulip Mario Carneiro (Nov 01 2020 at 18:58):

can we give it some short term memory?

view this post on Zulip Rob Lewis (Nov 01 2020 at 19:19):

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

view this post on Zulip Rob Lewis (Nov 01 2020 at 22:27):

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.

view this post on Zulip Rob Lewis (Nov 01 2020 at 22:28):

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


Last updated: May 09 2021 at 15:11 UTC