Function.Periodic.aestronglyMeasurable

theorem aestronglyMeasurable {t T : ℝ} [hT : Fact (0 < T)] {f : ℝ → ℂ}  (periodic_f : f.Periodic T) (hf : AEStronglyMeasurable f (volume.restrict (Ioc t (t + T)))) :    AEStronglyMeasurable f := by  rw [← Measure.restrict_univ (μ := volume), ← iUnion_Ioc_add_zsmul hT.out t]  apply AEStronglyMeasurable.iUnion  intro n  have : AEStronglyMeasurable (f ∘ (fun x ↦ x - n • T))      (volume.restrict (Ioc (t + n • T) (t + (n + 1) • T))) := by    apply hf.comp_measurePreserving    have : (Ioc (t + n • T) (t + (n + 1) • T)) = (fun x ↦ x - n • T) ⁻¹' (Ioc t (t + T)) := by      rw [preimage_sub_const_Ioc, add_smul]      ring_nf    rw [this]    apply MeasurePreserving.restrict_preimage (measurePreserving_sub_right _ _) measurableSet_Ioc  convert! this  ext x  simp only [comp_apply]  rw [periodic_f.sub_zsmul_eq]