fejer_kernel_integral_half_range

lemma fejer_kernel_integral_half_range (n : ℕ) :    (1 / Real.pi) * ∫ t in (0:ℝ)..Real.pi, fejer_kernel n t = 1 / 2 := by      -- Since the Fejér kernel is even, we have $\int_{-\pi}^{\pi} K_n(t) dt = 2 \int_{0}^{\pi} K_n(t) dt$.      have h_even : ∫ t in (-Real.pi)..Real.pi, fejer_kernel n t = 2 * ∫ t in (0)..Real.pi, fejer_kernel n t := by        -- By definition of even function, we can split the integral into two parts: from -π to 0 and from 0 to π.        have h_split : ∫ t in (-Real.pi)..Real.pi, fejer_kernel n t = (∫ t in (-Real.pi)..0, fejer_kernel n t) + (∫ t in (0)..Real.pi, fejer_kernel n t) := by          rw [ intervalIntegral.integral_add_adjacent_intervals ] <;> apply_rules [ Continuous.intervalIntegrable ];          · unfold fejer_kernel;            unfold dirichlet_kernel;            fun_prop (disch := norm_num);          · unfold fejer_kernel;            unfold dirichlet_kernel;            fun_prop (disch := norm_num);        norm_num [ two_mul, h_split ];        convert intervalIntegral.integral_comp_neg _ using 2 <;> norm_num [ fejer_kernel_even ];      have := fejer_kernel_integral_one n; rw [ h_even ] at this; nlinarith [ Real.pi_pos, mul_inv_cancel₀ Real.pi_ne_zero ] ;