fejer_kernel_uniform_limit_zero

theorem fejer_kernel_uniform_limit_zero (δ : ℝ) (hδ_pos : 0 < δ) (hδ_le : δ ≤ Real.pi) :    Filter.Tendsto (fun n => ⨆ t ∈ Set.Icc δ Real.pi, fejer_kernel n t) Filter.atTop (nhds 0) := by      -- By Lemma~\ref{lem:A.37}, we have the bound $K_n(t) \le \frac{\pi^2}{2(n+1)t^2}$ for $0 < t \le \pi$.      have h_bound : ∀ n t, 0 < t → t ≤ Real.pi → (fejer_kernel n t) ≤ (Real.pi^2) / (2 * (n + 1) * t^2) := by        exact?;      -- For $t \in [\delta, \pi]$, we have $t \ge \delta$, so $t^2 \ge \delta^2$, and thus $\frac{1}{t^2} \le \frac{1}{\delta^2}$.      have h_bound_delta : ∀ n, ⨆ t ∈ Set.Icc δ Real.pi, fejer_kernel n t ≤ (Real.pi^2) / (2 * (n + 1) * δ^2) := by        intro n        have h_sup_le : ∀ t ∈ Set.Icc δ Real.pi, fejer_kernel n t ≤ (Real.pi^2) / (2 * (n + 1) * δ^2) := by          exact fun t ht => le_trans ( h_bound n t ( by linarith [ ht.1 ] ) ( by linarith [ ht.2 ] ) ) ( by gcongr ; linarith [ ht.1, ht.2 ] );        field_simp;        refine' le_trans ( mul_le_mul_of_nonneg_right ( mul_le_mul_of_nonneg_right ( mul_le_mul_of_nonneg_right ( ciSup_le fun t => _ ) zero_le_two ) ( by positivity ) ) ( by positivity ) ) _;        exact Real.pi ^ 2 / ( 2 * ( n + 1 ) * δ ^ 2 );        · field_simp;          by_cases h : t ∈ Set.Icc δ Real.pi <;> simp_all +decide [ mul_assoc ];          · exact le_trans ( mul_le_mul_of_nonneg_right ( h_sup_le t h.1 h.2 ) ( by positivity ) ) ( by rw [ div_mul_cancel₀ _ ( by positivity ) ] );          · positivity;        · field_simp;          norm_num;      exact squeeze_zero ( fun n => by exact Real.iSup_nonneg fun _ => Real.iSup_nonneg fun _ => fejer_kernel_nonneg _ _ ) h_bound_delta <| tendsto_const_nhds.div_atTop <| Filter.Tendsto.atTop_mul_const ( by positivity ) <| Filter.Tendsto.const_mul_atTop ( by positivity ) <| Filter.tendsto_atTop_add_const_right _ _ tendsto_natCast_atTop_atTop;