fejer_kernel_tail_mass_vanishes

theorem fejer_kernel_tail_mass_vanishes (δ : ℝ) (hδ_pos : 0 < δ) (hδ_le : δ ≤ Real.pi) :    Filter.Tendsto (fun n => ∫ t in (Set.Icc (-Real.pi) (-δ) ∪ Set.Icc δ Real.pi), fejer_kernel n t) Filter.atTop (nhds 0) := by      have h_fejer_kernel_tail : Filter.Tendsto (fun n => ∫ t in Set.Icc δ Real.pi, fejer_kernel n t) Filter.atTop (nhds 0) := by        -- By the properties of the Fejér kernel, we know that its integral over $[\delta, \pi]$ is bounded by $\frac{1}{n+1} \int_{\delta}^{\pi} \frac{\pi^2}{2t^2} dt$.        have h_integral_bound : ∀ n : ℕ, ∫ t in Set.Icc δ Real.pi, fejer_kernel n t ≤ (1 / (n + 1 : ℝ)) * ∫ t in Set.Icc δ Real.pi, (Real.pi ^ 2 / (2 * t ^ 2)) := by          intro n;          rw [ ← MeasureTheory.integral_const_mul ];          field_simp;          refine' MeasureTheory.setIntegral_mono_on _ _ measurableSet_Icc fun t ht => _;          · exact Continuous.integrableOn_Icc ( show Continuous ( fejer_kernel n ) from by unfold fejer_kernel; exact Continuous.mul ( continuous_const ) <| continuous_finset_sum _ fun _ _ => continuous_const.add <| continuous_finset_sum _ fun _ _ => Real.continuous_cos.comp <| by continuity );          · exact ContinuousOn.integrableOn_Icc ( continuousOn_of_forall_continuousAt fun x hx => ContinuousAt.div continuousAt_const ( ContinuousAt.mul continuousAt_const ( continuousAt_id.pow 2 ) ) ( by nlinarith [ hx.1, hx.2, Real.pi_pos ] ) );          · convert fejer_kernel_le_quadratic n t ( by linarith [ ht.1 ] ) ( by linarith [ ht.2 ] ) using 1 ; ring;        exact squeeze_zero ( fun n => MeasureTheory.setIntegral_nonneg measurableSet_Icc fun t ht => fejer_kernel_nonneg _ _ ) h_integral_bound <| by simpa using tendsto_one_div_add_atTop_nhds_zero_nat.mul_const _;      convert h_fejer_kernel_tail.const_mul 2 using 2 <;> ring;      rw [ MeasureTheory.setIntegral_union ] <;> norm_num;      · norm_num [ mul_two, MeasureTheory.integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le, hδ_pos.le, hδ_le ];        convert intervalIntegral.integral_comp_neg _ using 2 <;> norm_num [ fejer_kernel_even ];      · exact Set.disjoint_left.mpr fun x hx₁ hx₂ => by linarith [ Set.mem_Icc.mp hx₁, Set.mem_Icc.mp hx₂ ] ;      · exact Continuous.integrableOn_Icc ( by exact Continuous.mul ( continuous_const ) ( by exact continuous_finset_sum _ fun _ _ => by exact Continuous.add continuous_const <| by exact continuous_finset_sum _ fun _ _ => Real.continuous_cos.comp <| by continuity ) );      · exact Continuous.integrableOn_Icc ( by unfold fejer_kernel; exact Continuous.mul ( continuous_const ) ( by exact continuous_finset_sum _ fun _ _ => by exact Continuous.add ( continuous_const ) ( by exact continuous_finset_sum _ fun _ _ => Real.continuous_cos.comp ( by continuity ) ) ) )