# Zulip Chat Archive

## 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)`

#### Yury G. Kudryashov (Jan 08 2021 at 22:19):

(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