## Stream: maths

### Topic: sigma_finite measures

#### Yury G. Kudryashov (Jan 08 2021 at 20:57):

@Floris van Doorn, your definition of docs#measure_theory.sigma_finite requires sets to be measurable. Actually, this assumption is not needed: for any s : set α there exists a measurable t ⊇ s of the same measure, see proof here. Taking this into account, do we need finite_spanning_sets_in?

#### Yury G. Kudryashov (Jan 08 2021 at 20:58):

And here is a proof of sigma_finite without is_measurable assumption.

#### Sebastien Gouezel (Jan 08 2021 at 21:24):

In practice, isn't it useful to have a sequence of measurable sets with finite measure covering the whole space? I mean, the definition you suggest (without measurability) is equivalent to the one with measurability, but the one with measurability seems more convenient to use.

#### Yury G. Kudryashov (Jan 08 2021 at 21:27):

I suggest that we use a definition without is_measurable but add measurability in docs#measure_theory.spanning_sets

#### Yury G. Kudryashov (Jan 08 2021 at 21:29):

I.e., the new definition should be accumulate (λ i, to_measurable μ ((classical.choice h).set i))

#### Yury G. Kudryashov (Jan 08 2021 at 21:30):

This way we have is_measurable (spanning_sets μ i) but we don't have to prove is_measurable (s n)

(deleted)

#### Floris van Doorn (Jan 08 2021 at 23:37):

Yeah, we should probably get rid of the is_measurable assumption. That is an artifact from the time that sigma_finite was not a proposition.
I agree we can remove it from sigma_finite, and keep it in spanning_sets.

#### Floris van Doorn (Jan 08 2021 at 23:41):

The structure finite_spanning_sets_in is still useful. I used it to get rid of some code duplication in measure_theory.prod.
The lemma docs#measure_theory.measure.finite_spanning_sets_in.prod shows both an extensionality result for measures on a product type (using docs#measure_theory.measure.finite_spanning_sets_in.ext) and the sigma-finiteness of product measures.

Last updated: May 11 2021 at 17:39 UTC