fejer_kernel_closed_form

theorem fejer_kernel_closed_form (n : ℕ) (t : ℝ) (h : Real.sin (t / 2) ≠ 0) :    fejer_kernel n t = (1 / (2 * (n + 1) : ℝ)) * (Real.sin ((n + 1) * t / 2) / Real.sin (t / 2)) ^ 2 := by      unfold fejer_kernel at *;      -- Using the identity $2\sin((j+1/2)t)\sin(t/2) = \cos(jt) - \cos((j+1)t)$, the sum telescopes.      have h_telescope : ∑ j ∈ Finset.range (n + 1), Real.sin ((j + 1 / 2) * t) = (1 / (2 * Real.sin (t / 2))) * (1 - Real.cos ((n + 1) * t)) := by        field_simp;        induction n <;> simp_all +decide [ Finset.sum_range_succ, add_mul, mul_add, Real.sin_add, Real.cos_add ] ; ring_nf;        · rw [ Real.sin_sq, Real.cos_sq ] ; ring_nf;        · rw [ ← Complex.ofReal_inj ] ; norm_num [ Complex.sin, Complex.cos ] ; ring_nf;          norm_num [ sq, ← Complex.exp_add ] ; ring;      -- Substitute the closed form of the Dirichlet kernel into the sum.      have h_substitute : ∑ j ∈ Finset.range (n + 1), dirichlet_kernel j t = (1 / (2 * Real.sin (t / 2))) * (∑ j ∈ Finset.range (n + 1), Real.sin ((j + 1 / 2) * t)) := by        rw [ Finset.mul_sum _ _ _ ] ; refine' Finset.sum_congr rfl fun j hj => _ ; rw [ dirichlet_kernel_closed_form ] ; ring ; aesop;      simp_all +decide [ mul_pow, Real.sin_sq, Real.cos_sq ] ; ring;      rw [ Real.sin_sq, Real.cos_sq ] ; ring