fejer_kernel_nonneg

theorem fejer_kernel_nonneg (n : ℕ) (t : ℝ) : 0 ≤ fejer_kernel n t := by  by_cases h : Real.sin ( t / 2 ) = 0;  · -- Since $\sin(t/2) = 0$, we have $t = 2k\pi$ for some integer $k$.    obtain ⟨k, rfl⟩ : ∃ k : ℤ, t = 2 * k * Real.pi := by      exact Real.sin_eq_zero_iff.mp h |> fun ⟨ k, hk ⟩ => ⟨ k, by linarith ⟩;    exact mul_nonneg ( by positivity ) ( Finset.sum_nonneg fun _ _ => add_nonneg ( by positivity ) ( Finset.sum_nonneg fun _ _ => by rw [ show Real.cos ( _ * ( 2 * k * Real.pi ) ) = 1 by rw [ Real.cos_eq_one_iff ] ; use k * ‹ℕ›; push_cast; ring ] ; positivity ) );  · exact ( by rw [ fejer_kernel_closed_form n t h ] ; positivity )