fejer_theorem_uniform_on_R

theorem fejer_theorem_uniform_on_R (f : ℝ → ℝ) (hf_int : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)    (hf_per : Function.Periodic f (2 * Real.pi)) (hf_cont : Continuous f) :    TendstoUniformly (fejer_sum f) f Filter.atTop := by      -- By `fejer_theorem_uniform_on_I`, `fejer_sum f` converges uniformly to `f` on $[-\pi, \pi]$.      have h_unif : TendstoUniformlyOn (fejer_sum f) f Filter.atTop (Set.Icc (-Real.pi) Real.pi) := by        apply fejer_theorem_uniform_on_I f hf_int hf_per (-Real.pi) Real.pi (by linarith [Real.pi_pos]);        exact fun x hx => hf_cont.continuousAt;      rw [ Metric.tendstoUniformlyOn_iff ] at h_unif;      rw [ Metric.tendstoUniformly_iff ];      -- Given ε > 0, we can find N such that for all n ≥ N, the distance between f(x) and fejer_sum f n x is less than ε for all x in [-π, π].      intro ε hε_pos      obtain ⟨N, hN⟩ : ∃ N, ∀ n ≥ N, ∀ x ∈ Set.Icc (-Real.pi) Real.pi, dist (f x) (fejer_sum f n x) < ε := by        exact Filter.eventually_atTop.mp ( h_unif ε hε_pos ) |> fun ⟨ N, hN ⟩ => ⟨ N, fun n hn x hx => hN n hn x hx ⟩;      -- Since both `fejer_sum f n` and `f` are $2\pi$-periodic, we can extend the uniform convergence to all of $\mathbb{R}$.      have h_periodic : ∀ n x, fejer_sum f n (x + 2 * Real.pi) = fejer_sum f n x ∧ f (x + 2 * Real.pi) = f x := by        exact fun n x => ⟨ by exact Function.Periodic.int_mul ( fejer_sum_periodic f n ) 1 x ▸ by norm_num, by exact hf_per x ⟩;      refine' Filter.eventually_atTop.mpr ⟨ N, fun n hn x => _ ⟩;      -- By periodicity, we can reduce any $x$ to the interval $[-\pi, \pi]$.      obtain ⟨k, hk⟩ : ∃ k : ℤ, x - 2 * k * Real.pi ∈ Set.Icc (-Real.pi) Real.pi := by        exact ⟨ ⌊ ( x + Real.pi ) / ( 2 * Real.pi ) ⌋, by nlinarith [ Int.floor_le ( ( x + Real.pi ) / ( 2 * Real.pi ) ), Real.pi_pos, mul_div_cancel₀ ( x + Real.pi ) ( by positivity : ( 2 * Real.pi ) ≠ 0 ) ], by nlinarith [ Int.lt_floor_add_one ( ( x + Real.pi ) / ( 2 * Real.pi ) ), Real.pi_pos, mul_div_cancel₀ ( x + Real.pi ) ( by positivity : ( 2 * Real.pi ) ≠ 0 ) ] ⟩;      convert hN n hn ( x - 2 * k * Real.pi ) hk using 1 ; ring;      exact congr_arg₂ _ ( by simpa [ mul_assoc, mul_comm Real.pi ] using Function.Periodic.int_mul hf_per k ( x - k * Real.pi * 2 ) ) ( by simpa [ mul_assoc, mul_comm Real.pi ] using Function.Periodic.int_mul ( show Function.Periodic ( fun x => fejer_sum f n x ) ( 2 * Real.pi ) from fun x => h_periodic n x |>.1 ) k ( x - k * Real.pi * 2 ) )