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