Equivalence of measures

Stream: Carleson

[Jeremy Tan]

In fpvandoorn/carleson#409 I fix several sorrys in RealInterpolation. I've reduced one remaining sorry to the following equivalence of measures:

lemma map_restrict_Ioi_eq_restrict_Ioi :
    (volume.restrict (Ioi 0)).map ENNReal.ofReal = volume.restrict (Ioi 0) := by
  sorry

There don't seem to be any tools to easily prove equivalence of measures in mathlib. How do I go about this?

[Floris van Doorn]

Something like this works: (at the bottom of Measure.NNReal)

lemma ENNReal.volume_eq_volume_preimage {s : Set ℝ≥0∞} (hs : MeasurableSet s) :
    volume s = volume (ENNReal.ofReal ⁻¹' s ∩ Ici 0) := by
  rw [ENNReal.volume_val hs]
  rw [measure_congr ENNReal.map_toReal_ae_eq_map_toReal_comap_ofReal]
  congr
  ext x
  sorry -- easy

lemma map_restrict_Ioi_eq_restrict_Ioi :
    (volume.restrict (Ioi 0)).map ENNReal.ofReal = volume.restrict (Ioi 0) := by
  ext s hs
  rw [Measure.map_apply measurable_ofReal hs]
  simp only [measurableSet_Ioi, Measure.restrict_apply']
  rw [ENNReal.volume_eq_volume_preimage (by measurability)]
  congr 1
  ext x
  simp +contextual [LT.lt.le]