fejer_sum_diff_bound_split

lemma fejer_sum_diff_bound_split {f : ℝ → ℝ} {n : ℕ} {x δ : ℝ}    (hδ_pos : 0 < δ) (hδ_le : δ ≤ Real.pi)    (hf_int : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)    (hf_per : Function.Periodic f (2 * Real.pi)) :    |fejer_sum f n x - f x| ≤    |(1 / Real.pi) * ∫ t in Set.Icc (-δ) δ, (f (x - t) - f x) * fejer_kernel n t| +    |(1 / Real.pi) * ∫ t in (Set.Icc (-Real.pi) (-δ) ∪ Set.Icc δ Real.pi), (f (x - t) - f x) * fejer_kernel n t| := by      rw [ fejer_sum_diff_eq_set_integral hf_int hf_per ];      rw [ ← MeasureTheory.integral_indicator, ← MeasureTheory.integral_indicator ];      · -- Apply the triangle inequality to the integral over the union of the central and tail regions.        have h_triangle : ∫ t, (Set.Icc (-Real.pi) Real.pi).indicator (fun t => (f (x - t) - f x) * fejer_kernel n t) t = (∫ t in Set.Icc (-δ) δ, (Set.Icc (-Real.pi) Real.pi).indicator (fun t => (f (x - t) - f x) * fejer_kernel n t) t) + (∫ t in (Set.Icc (-Real.pi) (-δ) ∪ Set.Icc δ Real.pi), (Set.Icc (-Real.pi) Real.pi).indicator (fun t => (f (x - t) - f x) * fejer_kernel n t) t) := by          rw [ ← MeasureTheory.integral_union_ae ];          · rw [ ← MeasureTheory.integral_indicator ] <;> norm_num [ Set.indicator ];            grind;          · exact?;          · exact MeasurableSet.nullMeasurableSet ( measurableSet_Icc.union measurableSet_Icc );          · refine' MeasureTheory.Integrable.integrableOn _;            rw [ MeasureTheory.integrable_indicator_iff ];            · exact?;            · norm_num;          · refine' MeasureTheory.Integrable.integrableOn _;            rw [ MeasureTheory.integrable_indicator_iff ];            · exact?;            · norm_num;        rw [ h_triangle, MeasureTheory.integral_indicator, MeasureTheory.integral_indicator ] <;> norm_num [ Set.indicator ];        rw [ ← mul_add ];        rw [ show ( Set.Icc ( -Real.pi ) Real.pi ∩ Set.Icc ( -δ ) δ : Set ℝ ) = Set.Icc ( -δ ) δ from Set.inter_eq_right.mpr <| Set.Icc_subset_Icc ( by linarith ) ( by linarith ), show ( Set.Icc ( -Real.pi ) Real.pi ∩ ( Set.Icc ( -Real.pi ) ( -δ ) ∪ Set.Icc δ Real.pi ) : Set ℝ ) = Set.Icc ( -Real.pi ) ( -δ ) ∪ Set.Icc δ Real.pi from Set.inter_eq_right.mpr <| Set.union_subset ( Set.Icc_subset_Icc ( by linarith ) ( by linarith ) ) ( Set.Icc_subset_Icc ( by linarith ) ( by linarith ) ) ];        rw [ ← MeasureTheory.integral_indicator, ← MeasureTheory.integral_indicator ] <;> norm_num [ Set.indicator ];        exact?;      · norm_num;      · norm_num