A question about measure theory

Stream: new members

[Ching-Tsun Chou]

Is there a theorem in Mathlib saying that the Lebesgue measure of a measurable subset of ℝ is invariant under translation? Somehow I can find similar results about scaling, but not translation.

[Bjørn Kjos-Hanssen]

The keyword should be "Haar measure"

[Ben Eltschig]

docs#IsHaarMeasure is defined in the second half of MeasureTheory.Group.Measure; further up in the same file are results on general left- and right-invariant measures, which are probably what you are looking for. I haven't looked too closely, but for example docs#MeasureTheory.map_add_left_eq_self seems relevant.

[Ching-Tsun Chou]

Thanks! I wouldn't have found it myself.

[Ching-Tsun Chou]

I was able to prove the result I want:

example (s : Set ℝ) (c : ℝ) : volume (image (fun x ↦ x + c) s) = volume s := by
  rw [← map_add_left_eq_self volume c]
  simp

But I have to say I do not understand the proof at all. Even weirder, map_add_right_eq_self also works:

example (s : Set ℝ) (c : ℝ) : volume (image (fun x ↦ x + c) s) = volume s := by
  rw [← map_add_right_eq_self volume c]
  simp

Well, using simp?, I found that neither theorems are actually needed:

example (s : Set ℝ) (c : ℝ) : volume (image (fun x ↦ x + c) s) = volume s := by
  simp only [image_add_right, measure_preimage_add_right]

[Ching-Tsun Chou]

Now I have another question: which result in Mathlib will allow me to prove the following?

example {s : Set ℝ} (h : MeasurableSet s) (c : ℝ) : MeasurableSet (image (fun x ↦ x + c) s) := by
  sorry

[Eric Wieser]

That last one is

example {s : Set ℝ} (h : MeasurableSet s) (c : ℝ) : MeasurableSet ((fun x ↦ x + c) '' s) := by
  exact (MeasurableEquiv.addRight c).measurableSet_image.mpr h

[Ching-Tsun Chou]

Thanks! I found that I can also search for the solution using "apply?":

example {s : Set ℝ} (h : MeasurableSet s) (c : ℝ) : MeasurableSet (image (fun x ↦ x + c) s) := by
  apply (MeasurableEmbedding.measurableSet_image ?_).mpr h
  exact measurableEmbedding_addRight c