Product of nonmeasurable sets

Stream: maths

[Yury G. Kudryashov]

Is it true that with some reasonable typeclass assumptions we have ν t ≠ 0 → NullMeasurableSet (s ×ˢ t) (μ.prod ν) → NullMeasurableSet s μ? What are these assumptions? How do I prove this? I tried to google but found incorrect proofs only.

[Antoine Chambert-Loir]

I would guess that it follows from Fubini, with a “locally null measurable” variant if the measures do not satisfy Fubini.

[Yury G. Kudryashov]

How?

[Felix Weilacher]

Does this work?

Let A and B be measurable such that the product measure of B \ A is 0 and A \subset s x t \subset B. If Tonelli holds, then since t has positive measure, there is some y \in t such that B^y \ A^y has mu-measure 0. But A^y \subset s \subset B^y.

[Felix Weilacher]

By C^y for C a subset of the plane, I mean {x | (x,y) \in C}

[Felix Weilacher]

Also, if t is simply non measurable rather than having positive measure, this still works. If a measurable function is positive on some non-null set, it is positive on some measurable set of positive measure

[Yury G. Kudryashov]

I'll try to formalize this now.

[Yury G. Kudryashov]

Thanks! #7578