measure on R^n

Stream: maths

[Johan Commelin]

@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]

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

[Alex J. Best]

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

[Johan Commelin]

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

[Floris van Doorn]

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