fejer_integrand_integrable

lemma fejer_integrand_integrable {f : ℝ → ℝ} {n : ℕ} {x : ℝ}    (hf_int : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)    (hf_per : Function.Periodic f (2 * Real.pi)) :    MeasureTheory.IntegrableOn (fun t => (f (x - t) - f x) * fejer_kernel n t) (Set.Icc (-Real.pi) Real.pi) := by      -- The function $f$ is integrable on $[-\pi, \pi]$ and periodic, so $t \mapsto f(x-t)$ is integrable on $[-\pi, \pi]$. The Fejér kernel $K_n$ is a trigonometric polynomial, hence continuous and bounded on $[-\pi, \pi]$. Therefore, $(f(x-t) - f(x)) K_n(t)$ is integrable.      have h_integrable : MeasureTheory.IntegrableOn (fun t => f (x - t)) (Set.Icc (-Real.pi) Real.pi) := by        have h_integrable : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (x - Real.pi) (x + Real.pi)) := by          have h_integrable : ∀ m : ℤ, MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (m * 2 * Real.pi - Real.pi) (m * 2 * Real.pi + Real.pi)) := by            intro m            have h_integrable : MeasureTheory.IntegrableOn (fun t => f (t + m * 2 * Real.pi)) (Set.Icc (-Real.pi) Real.pi) := by              have h_integrable : MeasureTheory.IntegrableOn (fun t => f t) (Set.Icc (-Real.pi) Real.pi) := by                rw [ intervalIntegrable_iff_integrableOn_Icc_of_le ( by linarith [ Real.pi_pos ] ) ] at hf_int ; aesop;              convert h_integrable using 1;              exact funext fun t => by simpa [ mul_assoc ] using Function.Periodic.int_mul hf_per m t;            rw [ ← MeasureTheory.integrable_indicator_iff ( measurableSet_Icc ) ] at *;            convert h_integrable.comp_sub_right ( m * 2 * Real.pi ) using 1;            ext; simp [Set.indicator];            split_ifs <;> ring_nf at * <;> aesop;          -- Choose $m$ such that $m * 2 * \pi - \pi \leq x - \pi < m * 2 * \pi + \pi$.          obtain ⟨m, hm⟩ : ∃ m : ℤ, m * 2 * Real.pi - Real.pi ≤ x - Real.pi ∧ x - Real.pi < m * 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 (m * 2 * Real.pi - Real.pi) (m * 2 * Real.pi + Real.pi + 2 * Real.pi)) := by            convert MeasureTheory.IntegrableOn.union ( h_integrable m ) ( h_integrable ( m + 1 ) ) using 1 ; ring;            grind;          exact h_integrable.mono_set ( Set.Icc_subset_Icc ( by linarith ) ( by linarith ) );        rw [ ← MeasureTheory.integrable_indicator_iff ( measurableSet_Icc ) ] at *;        convert h_integrable.comp_sub_left x using 1;        ext; simp [Set.indicator];        grind;      have h_integrable : MeasureTheory.IntegrableOn (fun t => (f (x - t) - f x) * fejer_kernel n t) (Set.Icc (-Real.pi) Real.pi) := by        have h_bounded : ∃ C, ∀ t ∈ Set.Icc (-Real.pi) Real.pi, |fejer_kernel n t| ≤ C := by          use (n + 1) / 2;          field_simp;          exact fun t ht => by rw [ abs_of_nonneg ( fejer_kernel_nonneg n t ) ] ; exact le_trans ( mul_le_mul_of_nonneg_right ( fejer_kernel_le_linear n t ) zero_le_two ) ( by linarith ) ;        refine' MeasureTheory.Integrable.mono' _ _ _;        refine' fun t => |f ( x - t ) - f x| * h_bounded.choose;        · exact MeasureTheory.Integrable.mul_const ( MeasureTheory.Integrable.abs ( h_integrable.sub ( MeasureTheory.integrable_const _ ) ) ) _;        · refine' MeasureTheory.AEStronglyMeasurable.mul _ _;          · exact MeasureTheory.AEStronglyMeasurable.sub h_integrable.aestronglyMeasurable ( MeasureTheory.aestronglyMeasurable_const );          · refine' Measurable.aestronglyMeasurable _;            refine' Measurable.mul _ _;            · exact measurable_const;            · refine' Finset.measurable_sum _ fun i _ => _;              exact Measurable.add measurable_const ( Finset.measurable_sum _ fun j hj => Real.continuous_cos.measurable.comp ( measurable_const.mul measurable_id' ) );        · filter_upwards [ MeasureTheory.ae_restrict_mem measurableSet_Icc ] with t ht using by simpa only [ norm_mul, Real.norm_eq_abs, abs_abs ] using mul_le_mul_of_nonneg_left ( h_bounded.choose_spec t ht ) ( abs_nonneg _ ) ;      convert h_integrable using 1