integral_periodic_shift

theorem integral_periodic_shift (g : ℝ → ℝ) (hg_per : Function.Periodic g (2 * Real.pi)) (x : ℝ)    (hg_int : IntervalIntegrable g MeasureTheory.volume (-Real.pi) Real.pi) :    ∫ u in (x - Real.pi)..(x + Real.pi), g u = ∫ u in (-Real.pi)..Real.pi, g u := by      -- Since $g$ is periodic with period $2\pi$, the integral over any interval of length $2\pi$ is the same.      have h_periodic : ∀ a : ℝ, ∫ u in a..a + 2 * Real.pi, g u = ∫ u in (-Real.pi)..Real.pi, g u := by        intro a;        have h_periodic : ∀ a b : ℝ, ∫ u in a..b, g u = ∫ u in (a - 2 * Real.pi).. (b - 2 * Real.pi), g u := by          simp +decide [ ← intervalIntegral.integral_comp_sub_right, hg_per ];          exact fun a b => by congr; ext u; rw [ hg_per.sub_eq ] ;        have h_split : ∫ u in a..a + 2 * Real.pi, g u = (∫ u in a..(-Real.pi + 2 * Real.pi * ⌊(a + Real.pi) / (2 * Real.pi)⌋), g u) + (∫ u in (-Real.pi + 2 * Real.pi * ⌊(a + Real.pi) / (2 * Real.pi)⌋)..(-Real.pi + 2 * Real.pi * (⌊(a + Real.pi) / (2 * Real.pi)⌋ + 1)), g u) + (∫ u in (-Real.pi + 2 * Real.pi * (⌊(a + Real.pi) / (2 * Real.pi)⌋ + 1))..a + 2 * Real.pi, g u) := by          rw [ intervalIntegral.integral_add_adjacent_intervals, intervalIntegral.integral_add_adjacent_intervals ] <;> apply_rules [ MeasureTheory.IntegrableOn.intervalIntegrable ];          · have h_integrable : ∀ n : ℤ, MeasureTheory.IntegrableOn g (Set.Icc (-Real.pi + 2 * Real.pi * n) (Real.pi + 2 * Real.pi * n)) := by              intro n; rw [ intervalIntegrable_iff_integrableOn_Icc_of_le ( by nlinarith [ Real.pi_pos ] ) ] at hg_int; exact (by              have h_integrable : ∀ n : ℤ, MeasureTheory.IntegrableOn g (Set.Icc (-Real.pi + 2 * Real.pi * n) (Real.pi + 2 * Real.pi * n)) := by                intro n                have h_shift : ∀ x, g x = g (x - 2 * Real.pi * n) := by                  exact fun x => by simpa [ mul_comm ] using Function.Periodic.int_mul hg_per n ( x - 2 * Real.pi * n ) ;                rw [ ← MeasureTheory.integrable_indicator_iff ( measurableSet_Icc ) ] at *;                convert hg_int.comp_sub_right ( 2 * Real.pi * n ) using 1;                ext; simp [Set.indicator];                grind;              convert h_integrable n using 2 <;> ring);            have h_integrable : MeasureTheory.IntegrableOn g (Set.Icc (-Real.pi + 2 * Real.pi * ⌊(a + Real.pi) / (2 * Real.pi)⌋) (Real.pi + 2 * Real.pi * ⌊(a + Real.pi) / (2 * Real.pi)⌋)) := by              exact h_integrable _;            refine' h_integrable.mono_set _;            intro x hx; constructor <;> cases Set.mem_uIcc.mp hx <;> nlinarith [ Int.floor_le ( ( a + Real.pi ) / ( 2 * Real.pi ) ), Int.lt_floor_add_one ( ( a + Real.pi ) / ( 2 * Real.pi ) ), Real.pi_pos, mul_div_cancel₀ ( a + Real.pi ) ( by positivity : ( 2 * Real.pi ) ≠ 0 ) ] ;          · have h_integrable : ∀ n : ℤ, MeasureTheory.IntegrableOn g (Set.Icc (-Real.pi + 2 * Real.pi * n) (Real.pi + 2 * Real.pi * n)) := by              intro n; rw [ intervalIntegrable_iff_integrableOn_Icc_of_le ( by nlinarith [ Real.pi_pos ] ) ] at hg_int; exact (by              have h_integrable : ∀ n : ℤ, MeasureTheory.IntegrableOn g (Set.Icc (-Real.pi + 2 * Real.pi * n) (Real.pi + 2 * Real.pi * n)) := by                intro n                have h_shift : ∀ x, g x = g (x - 2 * Real.pi * n) := by                  exact fun x => by simpa [ mul_comm ] using Function.Periodic.int_mul hg_per n ( x - 2 * Real.pi * n ) ;                rw [ ← MeasureTheory.integrable_indicator_iff ( measurableSet_Icc ) ] at *;                convert hg_int.comp_sub_right ( 2 * Real.pi * n ) using 1;                ext; simp [Set.indicator];                grind;              convert h_integrable n using 2 <;> ring);            refine' MeasureTheory.IntegrableOn.mono_set _ _;            exact Set.Icc ( -Real.pi + 2 * Real.pi * ( ⌊ ( a + Real.pi ) / ( 2 * Real.pi ) ⌋ + 1 ) ) ( Real.pi + 2 * Real.pi * ( ⌊ ( a + Real.pi ) / ( 2 * Real.pi ) ⌋ + 1 ) );            · convert h_integrable ( ⌊ ( a + Real.pi ) / ( 2 * Real.pi ) ⌋ + 1 ) using 1 ; push_cast ; ring;            · rw [ Set.uIcc_of_le ( by nlinarith [ Int.floor_le ( ( a + Real.pi ) / ( 2 * Real.pi ) ), Int.lt_floor_add_one ( ( a + Real.pi ) / ( 2 * Real.pi ) ), Real.pi_pos, mul_div_cancel₀ ( a + Real.pi ) ( by positivity : ( 2 * Real.pi ) ≠ 0 ) ] ) ] ; exact Set.Icc_subset_Icc_right ( by nlinarith [ Int.floor_le ( ( a + Real.pi ) / ( 2 * Real.pi ) ), Int.lt_floor_add_one ( ( a + Real.pi ) / ( 2 * Real.pi ) ), Real.pi_pos, mul_div_cancel₀ ( a + Real.pi ) ( by positivity : ( 2 * Real.pi ) ≠ 0 ) ] ) ;          · have h_integrable : ∀ n : ℤ, MeasureTheory.IntegrableOn g (Set.Icc (-Real.pi + 2 * Real.pi * n) (Real.pi + 2 * Real.pi * n)) := by              intro n; rw [ intervalIntegrable_iff_integrableOn_Icc_of_le ( by nlinarith [ Real.pi_pos ] ) ] at hg_int; exact (by              have h_integrable : ∀ n : ℤ, MeasureTheory.IntegrableOn g (Set.Icc (-Real.pi + 2 * Real.pi * n) (Real.pi + 2 * Real.pi * n)) := by                intro n                have h_shift : ∀ x, g x = g (x - 2 * Real.pi * n) := by                  exact fun x => by simpa [ mul_comm ] using Function.Periodic.int_mul hg_per n ( x - 2 * Real.pi * n ) ;                rw [ ← MeasureTheory.integrable_indicator_iff ( measurableSet_Icc ) ] at *;                convert hg_int.comp_sub_right ( 2 * Real.pi * n ) using 1;                ext; simp [Set.indicator];                grind;              convert h_integrable n using 2 <;> ring);            have h_integrable : MeasureTheory.IntegrableOn g (Set.Icc (-Real.pi + 2 * Real.pi * ⌊(a + Real.pi) / (2 * Real.pi)⌋) (Real.pi + 2 * Real.pi * ⌊(a + Real.pi) / (2 * Real.pi)⌋)) := by              exact h_integrable _;            exact h_integrable.mono_set ( fun x hx => by constructor <;> cases Set.mem_uIcc.mp hx <;> nlinarith [ Int.floor_le ( ( a + Real.pi ) / ( 2 * Real.pi ) ), Int.lt_floor_add_one ( ( a + Real.pi ) / ( 2 * Real.pi ) ), Real.pi_pos, mul_div_cancel₀ ( a + Real.pi ) ( by positivity : ( 2 * Real.pi ) ≠ 0 ) ] );          · have h_integrable : ∀ n : ℤ, MeasureTheory.IntegrableOn g (Set.Icc (-Real.pi + 2 * Real.pi * n) (Real.pi + 2 * Real.pi * n)) := by              intro n; rw [ intervalIntegrable_iff_integrableOn_Icc_of_le ( by nlinarith [ Real.pi_pos ] ) ] at hg_int; exact (by              have h_integrable : ∀ n : ℤ, MeasureTheory.IntegrableOn g (Set.Icc (-Real.pi + 2 * Real.pi * n) (Real.pi + 2 * Real.pi * n)) := by                intro n                have h_shift : ∀ x, g x = g (x - 2 * Real.pi * n) := by                  exact fun x => by simpa [ mul_comm ] using Function.Periodic.int_mul hg_per n ( x - 2 * Real.pi * n ) ;                rw [ ← MeasureTheory.integrable_indicator_iff ( measurableSet_Icc ) ] at *;                convert hg_int.comp_sub_right ( 2 * Real.pi * n ) using 1;                ext; simp [Set.indicator];                grind;              convert h_integrable n using 2 <;> ring);            convert h_integrable ⌊ ( a + Real.pi ) / ( 2 * Real.pi ) ⌋ using 1 ; ring;            rw [ Set.uIcc_of_le ( by nlinarith [ Real.pi_pos ] ) ];        -- By periodicity, the integral over any interval of length $2\pi$ is the same.        have h_periodic_integral : ∀ k : ℤ, ∫ u in (-Real.pi + 2 * Real.pi * k)..(-Real.pi + 2 * Real.pi * (k + 1)), g u = ∫ u in (-Real.pi)..Real.pi, g u := by          intro k; symm; induction' k using Int.induction_on with n ihn n ihn <;> norm_num at *;          · grind;          · grind;          · rw [ ihn, h_periodic ] ; ring;        have h_periodic_integral : ∫ u in a..(-Real.pi + 2 * Real.pi * ⌊(a + Real.pi) / (2 * Real.pi)⌋), g u = ∫ u in (a + 2 * Real.pi)..(-Real.pi + 2 * Real.pi * (⌊(a + Real.pi) / (2 * Real.pi)⌋ + 1)), g u := by          grind;        have h_periodic_integral : ∫ u in (a + 2 * Real.pi)..(-Real.pi + 2 * Real.pi * (⌊(a + Real.pi) / (2 * Real.pi)⌋ + 1)), g u = -∫ u in (-Real.pi + 2 * Real.pi * (⌊(a + Real.pi) / (2 * Real.pi)⌋ + 1))..a + 2 * Real.pi, g u := by          rw [ intervalIntegral.integral_symm ];        linarith [ ‹∀ k : ℤ, ∫ u in -Real.pi + 2 * Real.pi * ( k : ℝ )..-Real.pi + 2 * Real.pi * ( k + 1 ), g u = ∫ u in -Real.pi..Real.pi, g u› ⌊ ( a + Real.pi ) / ( 2 * Real.pi ) ⌋ ];      convert h_periodic ( x - Real.pi ) using 2 ; ring