How do I show that Affine maps preserve measureable sets?

Stream: new members

[Toby Cathcart Burn]

How should I prove that affine maps send measurable sets to measurable sets? Is this in mathlib, and should it be? I'm specifically interested in functions ℝ × ℝ → ℝ × ℝ .
measurableEmbedding_addRight reduces this problem to showing that linear maps preserve measurable sets, but I can't find that in mathlib either.

[Aaron Liu]

Maybe docs#Continuous.measurable

[Aaron Liu]

We have docs#AffineMap.continuous_iff

[Toby Cathcart Burn]

Thanks, that looks great.

[Aaron Liu]

Maybe docs#AffineMap.continuous_linear_iff would be better

[Toby Cathcart Burn]

docs#Measurable talks about inverse images. Does this mean I need to get hold the inverse map (the cases I care about are invertible)?

[Aaron Liu]

Why would you need the inverse map?

[Aaron Liu]

Can you post the statement you want, written out in Lean?

[Toby Cathcart Burn]

theorem affine_Measurable (f : (ℝ × ℝ) →ᵃ[ℝ] (ℝ × ℝ)) {s : Set (ℝ×ℝ)} (h : MeasurableSet s ) : MeasurableSet (f '' s) := by
    sorry

[Aaron Liu]

hmmm

[Sébastien Gouëzel]

This one is not true. There are measurable subsets of R^2 whose projection on R is not measurable. So taking f (x, y) = (x, 0), you get a counterexample to your statement. Preimages are much better behaved than direct images in many respects.

[Toby Cathcart Burn]

I hadn't realized the theorem wasn't true in general, thanks for pointing it out.
In this particular case, wouldn't the image of f always have measure 0 (as a subset of R^2)?

[Sébastien Gouëzel]

Sure. Here by measurable I mean Borel-measurable, which is the standard meaning in mathlib. It's true that the image is always Lebesgue measurable, but that's a deep theorem.

[Toby Cathcart Burn]

Thanks for explaining that. I guess I'll show that my affine maps have inverses. How would I find which kind of measure is the default? docs#Real.measureSpace doesn't have the most informative definition.

[Toby Cathcart Burn]

I've found docs#Real.measurableSpace. So MeasurableSet (on R) means Borel measurable, but since volume is defined on all subsets of R, it makes sense to extend it usefully by using the Lebesgue measure.

[Etienne Marion]

In Mathlib measures are always defined for any set as the biggest outer measure which coincides with the measure on measurable sets.