fejer_kernel_le_linear

theorem fejer_kernel_le_linear (n : ℕ) (t : ℝ) : fejer_kernel n t ≤ (n + 1 : ℝ) / 2 := by  unfold fejer_kernel;  -- By definition of $D_j(t)$, we know that $|D_j(t)| \leq j + 1/2$.  have h_dirichlet_bound : ∀ j : ℕ, ∀ t : ℝ, |dirichlet_kernel j t| ≤ j + 1 / 2 := by    unfold dirichlet_kernel;    intro j t; refine' abs_le.mpr ⟨ _, _ ⟩ <;> linarith [ show ( ∑ k ∈ Finset.Icc 1 j, Real.cos ( k * t ) ) ≥ -↑j by exact le_trans ( by norm_num ) ( Finset.sum_le_sum fun i hi => Real.neg_one_le_cos _ ), show ( ∑ k ∈ Finset.Icc 1 j, Real.cos ( k * t ) ) ≤ ↑j by exact le_trans ( Finset.sum_le_sum fun i hi => Real.cos_le_one _ ) ( by norm_num ) ] ;  rw [ div_mul_eq_mul_div, div_le_iff₀ ] <;> try linarith;  exact le_trans ( mul_le_mul_of_nonneg_left ( Finset.sum_le_sum fun _ _ => le_of_abs_le ( h_dirichlet_bound _ _ ) ) zero_le_one ) ( by induction' n with n ih <;> norm_num [ Finset.sum_range_succ ] at * ; nlinarith )