theorem Function.Periodic.setIntegral_Ioc_add_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {T : ℝ} (hf : Periodic f T) (t s : ℝ) : ∫ (x : ℝ) in Set.Ioc t (t + T), f x = ∫ (x : ℝ) in Set.Ioc s (s + T), f x

If f is a periodic function with period T, then its integral over [t, t + T] does not depend on t.

theorem Function.Periodic.setLIntegral_Ioc_add_eq {T : ℝ} {f : ℝ → ENNReal} (hf : Periodic f T) (t s : ℝ) : ∫⁻ (x : ℝ) in Set.Ioc t (t + T), f x = ∫⁻ (x : ℝ) in Set.Ioc s (s + T), f x

theorem Function.Periodic.eLpNorm {T s t : ℝ} {f : ℝ → ℂ} (periodic_f : Periodic f T) {p : ENNReal} : MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (Set.Ioc t (t + T))) = MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (Set.Ioc s (s + T)))

theorem Function.Periodic.aestronglyMeasurable {t T : ℝ} [hT : Fact (0 < T)] {f : ℝ → ℂ} (periodic_f : Periodic f T) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioc t (t + T)))) : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume

theorem Function.Periodic.aestronglyMeasurable_iff {t T : ℝ} [hT : Fact (0 < T)] {f : ℝ → ℂ} (periodic_f : Periodic f T) : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume ↔ MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioc t (t + T)))

theorem AddCircle.volume_preimage_equivIoc {T : ℝ} [hT : Fact (0 < T)] {s : Set ℝ} (hs : MeasurableSet s) : MeasureTheory.volume ((fun (x : AddCircle T) => ↑((equivIoc T 0) x)) ⁻¹' s) = MeasureTheory.volume (s ∩ Set.Ioc 0 T)

theorem MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc {T : ℝ} [hT : Fact (0 < T)] {t : ℝ} {f : ℝ → ℂ} (hf : AEStronglyMeasurable f (volume.restrict (Set.Ioc t (t + T)))) {p : ENNReal} : eLpNorm f p (volume.restrict (Set.Ioc t (t + T))) = eLpNorm (AddCircle.liftIoc T t f) p volume

theorem MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc' {T : ℝ} [hT : Fact (0 < T)] {t : ℝ} {f : AddCircle T → ℂ} (hf : AEStronglyMeasurable f volume) {p : ENNReal} : eLpNorm (fun (x : ℝ) => f ↑x) p (volume.restrict (Set.Ioc t (t + T))) = eLpNorm f p volume