Zulip Chat Archive

Stream: maths

Topic: sigma_finite measures


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jan 08 2021 at 20:58):

And here is a proof of sigma_finite without is_measurable assumption.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip 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)

view this post on Zulip Yury G. Kudryashov (Jan 08 2021 at 22:19):

(deleted)

view this post on Zulip 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.

view this post on Zulip 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