# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: measure_space.pi

#### Yury G. Kudryashov (Jan 03 2021 at 21:37):

@Floris van Doorn I want to have a `measure_space`

instance on `fin n → \R`

. Do you prefer to add an instance `measure_space.pi`

yourself, or should I PR it?

#### Floris van Doorn (Jan 03 2021 at 22:27):

You can PR it, I currently have nothing else lined up for finitary product measures.

The file is currently very bare-bones, but it should be easy to show more properties about it.

#### Yury G. Kudryashov (Jan 03 2021 at 23:07):

I have it + `sigma_finite volume`

. I'll PR it later today.

#### Yury G. Kudryashov (Jan 03 2021 at 23:07):

(actually, I have `locally_finite_measure`

+ `second_countable_topology`

+ `opens_measurable_space`

→ `sigma_finite`

)

#### Floris van Doorn (Jan 03 2021 at 23:22):

we should at some point also get `measure.pi.sigma_finite`

.

Your result is also useful. I did something similar yesterday (not PR'd yet):

```
theorem measure_theory.measure.regular.sigma_finite : [topological_group G] [opens_measurable_space G] [t2_space G] [separable_space G] [locally_compact_space G], μ.regular → sigma_finite μ
```

That result should follow easily from yours (at least, if one of us replaces `second_countable_topology`

/ `separable_space`

with the other.

Last updated: May 17 2021 at 16:26 UTC