Stream: maths

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 $\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".

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