integrable_shifted_periodic

lemma integrable_shifted_periodic {f : ℝ → ℝ} (hf_int : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)    (hf_per : Function.Periodic f (2 * Real.pi)) (x : ℝ) :    IntervalIntegrable (fun t => f (x + t)) MeasureTheory.volume 0 Real.pi := by      have h_integrable_left : IntervalIntegrable (fun t => f (x + t)) MeasureTheory.volume (-Real.pi) Real.pi := by        have h_integrable : IntervalIntegrable (fun t => f t) MeasureTheory.volume (x - Real.pi) (x + Real.pi) := by          rw [ intervalIntegrable_iff ] at *;          have h_integrable : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (x - Real.pi) (x + Real.pi)) := by            have h_integrable : ∀ n : ℤ, MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (n * (2 * Real.pi) - Real.pi) (n * (2 * Real.pi) + Real.pi)) := by              intro n              have h_integrable : MeasureTheory.IntegrableOn (fun t => f (t - n * (2 * Real.pi))) (Set.Icc (n * (2 * Real.pi) - Real.pi) (n * (2 * Real.pi) + Real.pi)) := by                have h_integrable : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (-Real.pi) Real.pi) := by                  simpa only [ Set.uIoc_of_le ( neg_le_self Real.pi_pos.le ), MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_congr_set MeasureTheory.Ioc_ae_eq_Icc ] using hf_int;                rw [ ← MeasureTheory.integrable_indicator_iff ( measurableSet_Icc ) ] at *;                convert h_integrable.comp_sub_right ( n * ( 2 * Real.pi ) ) using 1;                ext; simp [Set.indicator];                split_ifs <;> ring_nf at * <;> aesop;              convert h_integrable using 1;              exact funext fun x => by simpa using Function.Periodic.int_mul hf_per n ( x - n * ( 2 * Real.pi ) ) ;            -- Choose $n$ such that $n * (2 * π) - π ≤ x - π < (n + 1) * (2 * π) - π$.            obtain ⟨n, hn⟩ : ∃ n : ℤ, n * (2 * Real.pi) - Real.pi ≤ x - Real.pi ∧ x - Real.pi < (n + 1) * (2 * Real.pi) - Real.pi := by              exact ⟨ ⌊ ( x - Real.pi + Real.pi ) / ( 2 * Real.pi ) ⌋, by nlinarith [ Int.floor_le ( ( x - Real.pi + Real.pi ) / ( 2 * Real.pi ) ), Real.pi_pos, mul_div_cancel₀ ( x - Real.pi + Real.pi ) ( by positivity : ( 2 * Real.pi ) ≠ 0 ) ], by nlinarith [ Int.lt_floor_add_one ( ( x - Real.pi + Real.pi ) / ( 2 * Real.pi ) ), Real.pi_pos, mul_div_cancel₀ ( x - Real.pi + Real.pi ) ( by positivity : ( 2 * Real.pi ) ≠ 0 ) ] ⟩;            have h_integrable : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (n * (2 * Real.pi) - Real.pi) ((n + 1) * (2 * Real.pi) + Real.pi)) := by              have h_integrable : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (n * (2 * Real.pi) - Real.pi) (n * (2 * Real.pi) + Real.pi)) ∧ MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc ((n + 1) * (2 * Real.pi) - Real.pi) ((n + 1) * (2 * Real.pi) + Real.pi)) := by                exact ⟨ h_integrable n, by simpa using h_integrable ( n + 1 ) ⟩;              convert h_integrable.1.union h_integrable.2 using 1;              grind;            exact h_integrable.mono_set <| Set.Icc_subset_Icc ( by linarith ) ( by linarith );          exact h_integrable.mono_set ( by rw [ Set.uIoc_of_le ( by linarith [ Real.pi_pos ] ) ] ; exact Set.Ioc_subset_Icc_self );        convert h_integrable.comp_add_left x using 1 ; ring;        ring;      apply_rules [ h_integrable_left.mono_set, Set.Icc_subset_Icc ] <;> norm_num [ Real.pi_pos.le ]