Source indexedlemma · leanprover/lean4:v4.32.0

AddCircle.map_subtypeVal_map_equivIoc_volume

Carleson.ToMathlib.MeasureTheory.Integral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/Periodic.lean:65 to 72

Mathematical statement

Exact Lean statement

lemma map_subtypeVal_map_equivIoc_volume :
    (volume.map (equivIoc T a)).map Subtype.val = volume.restrict (Ioc a (a + T))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma map_subtypeVal_map_equivIoc_volume :    (volume.map (equivIoc T a)).map Subtype.val = volume.restrict (Ioc a (a + T)) := by  have h := measurable_equivIoc T a  rw [← (AddCircle.measurePreserving_mk T a).map_eq]  rw [Measure.map_map measurable_subtype_coe h, Measure.map_map (measurable_subtype_coe.comp h)]  · exact (Measure.map_congr <| Filter.Eventually.mono (self_mem_ae_restrict measurableSet_Ioc) <|      fun x hx ↦ AddCircle.liftIoc_coe_apply hx).trans Measure.map_id  · exact fun _ ↦ id