measure_space.pi

Stream: Is there code for X?

[Yury G. Kudryashov]

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

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]

I have it + sigma_finite volume. I'll PR it later today.

[Yury G. Kudryashov]

(actually, I have locally_finite_measure + second_countable_topology + opens_measurable_space → sigma_finite)

[Floris van Doorn]

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.