Topic: measure on R^n
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).
Yury G. Kudryashov (Nov 07 2020 at 17:06):
We can introduce a measure on 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".
Alex J. Best (Nov 07 2020 at 17:46):
Johan Commelin (Nov 07 2020 at 17:54):
Aaah, thanks for the pointer. That was from before I subscribed to #triage
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