sigma_finite measures

Stream: maths

[Yury G. Kudryashov]

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

And here is a proof of sigma_finite without is_measurable assumption.

[Sebastien Gouezel]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

(deleted)

[Floris van Doorn]

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]

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.