fejer_theorem_uniform_on_I

theorem fejer_theorem_uniform_on_I (f : ℝ → ℝ) (hf_int : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)    (hf_per : Function.Periodic f (2 * Real.pi)) (a b : ℝ) (hab : a ≤ b)    (hf_cont : ∀ x ∈ Set.Icc a b, ContinuousAt f x) :    TendstoUniformlyOn (fejer_sum f) f Filter.atTop (Set.Icc a b) := by      have h_fejer_uniform : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, ∀ x ∈ Set.Icc a b, |fejer_sum f n x - f x| < ε := by        intro ε hε_pos        obtain ⟨δ₀, hδ₀_pos, hδ₀⟩ : ∃ δ₀ > 0, ∀ x ∈ Set.Icc a b, ∀ t, |t| < δ₀ → |f (x - t) - f x| < ε / 2 := by          have := @uniform_continuity_shift;          exact this a b hab hf_cont ( ε / 2 ) ( half_pos hε_pos );        -- Let `δ = min(δ₀/2, π/2)`. Then `0 < δ < π` and `[-δ, δ] ⊆ (-δ₀, δ₀)`.        set δ := min (δ₀ / 2) (Real.pi / 2) with hδ_def        have hδ_pos : 0 < δ := by          exact lt_min ( half_pos hδ₀_pos ) ( half_pos Real.pi_pos )        have hδ_le_pi : δ ≤ Real.pi := by          exact le_trans ( min_le_right _ _ ) ( by linarith [ Real.pi_pos ] )        have hδ_subset : Set.Icc (-δ) δ ⊆ Set.Ioo (-δ₀) δ₀ := by          exact fun x hx => ⟨ by linarith [ hx.1, hx.2, min_le_left ( δ₀ / 2 ) ( Real.pi / 2 ), min_le_right ( δ₀ / 2 ) ( Real.pi / 2 ) ], by linarith [ hx.1, hx.2, min_le_left ( δ₀ / 2 ) ( Real.pi / 2 ), min_le_right ( δ₀ / 2 ) ( Real.pi / 2 ) ] ⟩;        -- By `fejer_tail_convergence`, the `Tail` integral converges uniformly to 0 on `[a, b]`.        have h_tail_uniform : TendstoUniformlyOn (fun n x => (1 / Real.pi) * ∫ t in (Set.Icc (-Real.pi) (-δ) ∪ Set.Icc δ Real.pi), (f (x - t) - f x) * fejer_kernel n t) 0 Filter.atTop (Set.Icc a b) := by          apply_rules [ fejer_tail_convergence ];          exact lt_of_le_of_ne hδ_le_pi ( by rintro h; linarith [ Real.pi_pos, min_le_left ( δ₀ / 2 ) ( Real.pi / 2 ), min_le_right ( δ₀ / 2 ) ( Real.pi / 2 ) ] );        -- By `fejer_sum_diff_bound_split`, we have `|fejer_sum f n x - f x| ≤ |Central| + |Tail|`.        have h_bound : ∀ n x, x ∈ Set.Icc a b → |fejer_sum f n x - f x| ≤ |(1 / Real.pi) * ∫ t in Set.Icc (-δ) δ, (f (x - t) - f x) * fejer_kernel n t| + |(1 / Real.pi) * ∫ t in (Set.Icc (-Real.pi) (-δ) ∪ Set.Icc δ Real.pi), (f (x - t) - f x) * fejer_kernel n t| := by          intros n x hx          apply fejer_sum_diff_bound_split hδ_pos hδ_le_pi hf_int hf_per;        -- By `fejer_central_bound`, `|Central| ≤ ε/2`.        have h_central_bound : ∀ n x, x ∈ Set.Icc a b → |(1 / Real.pi) * ∫ t in Set.Icc (-δ) δ, (f (x - t) - f x) * fejer_kernel n t| ≤ ε / 2 := by          intros n x hx          apply fejer_central_bound hδ_pos hδ_le_pi (fun t ht => by            exact le_of_lt ( hδ₀ x hx t ( by linarith [ abs_lt.mpr ( hδ_subset ( show t ∈ Set.Icc ( -δ ) δ from ⟨ by linarith [ abs_le.mp ht ], by linarith [ abs_le.mp ht ] ⟩ ) ) ] ) )) hf_int hf_per;        rw [ Metric.tendstoUniformlyOn_iff ] at h_tail_uniform;        simp +zetaDelta at *;        exact Exists.elim ( h_tail_uniform ( ε / 2 ) ( half_pos hε_pos ) ) fun N hN => ⟨ N, fun n hn x hx₁ hx₂ => lt_of_le_of_lt ( h_bound n x hx₁ hx₂ ) ( by linarith [ hN n hn x hx₁ hx₂, h_central_bound n x hx₁ hx₂ ] ) ⟩ ;      rw [ Metric.tendstoUniformlyOn_iff ];      exact fun ε hε => by rcases h_fejer_uniform ε hε with ⟨ N, hN ⟩ ; filter_upwards [ Filter.Ici_mem_atTop N ] with n hn using fun x hx => by rw [ dist_comm ] ; exact hN n hn x hx;