Zulip Chat Archive

Stream: maths

Topic: measure on R^n

view this post on Zulip Johan Commelin (Nov 07 2020 at 08:53):

@Floris van Doorn whats the status on product measures? Do you have time for this? I think it's the main thing that's blocking #2819 (Minkowski's geometry of numbers).

view this post on Zulip Yury G. Kudryashov (Nov 07 2020 at 17:06):

We can introduce a measure on Rn\mathbb R^n as the Haar measure but then we'll have to prove manually theorems like "volume of a rectangular box is the product of its dimensions".

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

Did you see what I wrote at https://leanprover.zulipchat.com/#narrow/stream/263328-triage/topic/random.20PR.3A.20.5BWIP.5D.20feat%28number_theory.2Fgeometry_of_numbers%29.3A.2E.2E.2E/near/215254314

view this post on Zulip Johan Commelin (Nov 07 2020 at 17:54):

Aaah, thanks for the pointer. That was from before I subscribed to #triage

view this post on Zulip Floris van Doorn (Nov 07 2020 at 23:40):

I'm not sure how much time I'll have for this over the next ~month while doing job applications and other stuff.
If someone wants to do this, be my guest. Otherwise, I'll do it at some point.
The only thing I have so far on finitary products are the bottom ~200 lines of https://github.com/leanprover-community/mathlib/blob/measure-prod/src/measure_theory/prod.lean

Last updated: May 18 2021 at 06:15 UTC