fejer_kernel_le_quadratic

theorem fejer_kernel_le_quadratic (n : ℕ) (t : ℝ) (ht_pos : 0 < t) (ht_le : t ≤ Real.pi) :    fejer_kernel n t ≤ Real.pi ^ 2 / (2 * (n + 1) * t ^ 2) := by      -- Using the inequality $\sin u \ge \frac{2}{\pi}u$ for $0 \le u \le \pi/2$, with $u = t/2$, we have $\sin(t/2) \ge \frac{2}{\pi}(t/2) = \frac{t}{\pi}$.      have h_sin_ineq : Real.sin (t / 2) ≥ t / Real.pi := by        have := Real.mul_le_sin ( by positivity ) ( by linarith : t / 2 ≤ Real.pi / 2 );        ring_nf at this ⊢; linarith;      -- Squaring both sides of the inequality $\sin(t/2) \ge t/\pi$, we get $\sin^2(t/2) \ge t^2/\pi^2$.      have h_sin_sq_ineq : Real.sin (t / 2) ^ 2 ≥ t^2 / Real.pi^2 := by        simpa only [ div_pow ] using pow_le_pow_left₀ ( by positivity ) h_sin_ineq 2;      rw [ fejer_kernel_closed_form ];      · field_simp at h_sin_sq_ineq ⊢;        exact div_le_of_le_mul₀ ( sq_nonneg _ ) ( by positivity ) ( by nlinarith [ Real.sin_sq_le_one ( t * ( n + 1 ) / 2 ) ] );      · exact ne_of_gt ( Real.sin_pos_of_pos_of_lt_pi ( by positivity ) ( by linarith [ Real.pi_pos ] ) )