# Zulip Chat Archive

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

#### 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

#### 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