fejer_kernel_integral_one

theorem fejer_kernel_integral_one (n : ℕ) : (1 / Real.pi) * ∫ t in (-Real.pi)..Real.pi, fejer_kernel n t = 1 := by  unfold fejer_kernel;  -- By Fubini's theorem, we can interchange the order of summation and integration.  have h_fubini : ∫ t in (-Real.pi)..Real.pi, (∑ j ∈ Finset.range (n + 1), dirichlet_kernel j t) = ∑ j ∈ Finset.range (n + 1), ∫ t in (-Real.pi)..Real.pi, dirichlet_kernel j t := by    rw [ intervalIntegral.integral_finset_sum ];    intro i hi; apply_rules [ Continuous.intervalIntegrable ] ; unfold dirichlet_kernel; continuity;  -- By definition of $D_n(t)$, we know that $\int_{-\pi}^{\pi} D_n(t) \, dt = \pi$.  have h_dirichlet_integral : ∀ j : ℕ, ∫ t in (-Real.pi)..Real.pi, dirichlet_kernel j t = Real.pi := by    intro j; unfold dirichlet_kernel; rw [ intervalIntegral.integral_add ] <;> norm_num ; ring;    · erw [ intervalIntegral.integral_finset_sum ] <;> norm_num;      · erw [ Finset.sum_eq_zero ] ; intros ; rw [ intervalIntegral.integral_comp_mul_left ] <;> norm_num ; aesop;      · exact fun _ _ _ => Continuous.intervalIntegrable ( Real.continuous_cos.comp <| by continuity ) _ _;    · exact Continuous.intervalIntegrable ( continuous_finset_sum _ fun _ _ => Real.continuous_cos.comp ( by continuity ) ) _ _;  simp_all +decide [ div_eq_inv_mul, mul_assoc, mul_comm, mul_left_comm, ne_of_gt Real.pi_pos ];  exact mul_inv_cancel₀ ( by positivity )