fejer_central_bound

lemma fejer_central_bound {f : ℝ → ℝ} {n : ℕ} {x δ ε : ℝ}    (hδ_pos : 0 < δ) (hδ_le : δ ≤ Real.pi)    (h_cont : ∀ t, |t| ≤ δ → |f (x - t) - f x| ≤ ε)    (hf_int : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)    (hf_per : Function.Periodic f (2 * Real.pi)) :    |(1 / Real.pi) * ∫ t in Set.Icc (-δ) δ, (f (x - t) - f x) * fejer_kernel n t| ≤ ε := by      -- Applying the bound |f(x-t) - f(x)| ≤ ε to the integral over [-δ, δ], we get:      have h_integral_bound : |∫ t in Set.Icc (-δ) δ, (f (x - t) - f x) * fejer_kernel n t| ≤ ε * ∫ t in Set.Icc (-δ) δ, fejer_kernel n t := by        rw [ ←MeasureTheory.integral_const_mul ];        refine' le_trans ( MeasureTheory.norm_integral_le_integral_norm ( _ : ℝ → ℝ ) ) ( MeasureTheory.integral_mono_of_nonneg _ _ _ );        · exact Filter.Eventually.of_forall fun t => norm_nonneg _;        · refine' Continuous.integrableOn_Icc _;          refine' Continuous.mul continuous_const _;          exact continuous_const.mul <| continuous_finset_sum _ fun i _ => continuous_const.add <| continuous_finset_sum _ fun j _ => Real.continuous_cos.comp <| by continuity;        · filter_upwards [ MeasureTheory.ae_restrict_mem measurableSet_Icc ] with t ht using by simpa only [ Real.norm_eq_abs, abs_mul, abs_of_nonneg ( show 0 ≤ fejer_kernel n t from fejer_kernel_nonneg _ _ ) ] using mul_le_mul_of_nonneg_right ( h_cont t <| abs_le.mpr ⟨ by linarith [ ht.1 ], by linarith [ ht.2 ] ⟩ ) ( fejer_kernel_nonneg _ _ ) ;      -- Since $\int_{-\delta}^\delta K_n(t) dt \leq \int_{-\pi}^\pi K_n(t) dt = \pi$, we have:      have h_integral_le_pi : ∫ t in Set.Icc (-δ) δ, fejer_kernel n t ≤ ∫ t in Set.Icc (-Real.pi) Real.pi, fejer_kernel n t := by        refine' MeasureTheory.setIntegral_mono_set _ _ _;        · refine' Continuous.integrableOn_Icc _;          refine' continuous_const.mul _;          refine' continuous_finset_sum _ fun i hi => _;          exact continuous_const.add ( continuous_finset_sum _ fun _ _ => Real.continuous_cos.comp ( by continuity ) );        · filter_upwards [ MeasureTheory.ae_restrict_mem measurableSet_Icc ] with t ht using fejer_kernel_nonneg n t;        · exact MeasureTheory.ae_of_all _ fun t ht => ⟨ by linarith [ ht.1 ], by linarith [ ht.2 ] ⟩;      -- Since $\int_{-\pi}^\pi K_n(t) dt = \pi$, we have:      have h_integral_pi : ∫ t in Set.Icc (-Real.pi) Real.pi, fejer_kernel n t = Real.pi := by        convert congr_arg ( fun x : ℝ => x * Real.pi ) ( fejer_kernel_integral_one n ) using 1 <;> ring;        rw [ MeasureTheory.integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le ( by linarith [ Real.pi_pos ] ), mul_inv_cancel₀ Real.pi_ne_zero, one_mul ];      rw [ abs_mul, abs_of_nonneg ( by positivity ) ];      rw [ div_mul_eq_mul_div, div_le_iff₀ ] <;> nlinarith [ Real.pi_pos, show 0 ≤ ε by exact le_trans ( abs_nonneg _ ) ( h_cont 0 ( by norm_num; linarith ) ) ]