close_smooth_approx_periodic

lemma close_smooth_approx_periodic {T : ℝ} {f : ℝ → ℂ}  (unicontf : UniformContinuous f)  (periodicf : f.Periodic T) {ε : ℝ} (εpos : ε > 0) :    ∃ (f₀ : ℝ → ℂ), ContDiff ℝ ∞ f₀ ∧ f₀.Periodic T ∧      ∀ x, ‖f x - f₀ x‖ ≤ ε := by  obtain ⟨δ, δpos, hδ⟩ := (Metric.uniformContinuous_iff.mp unicontf) ε εpos  let φ : ContDiffBump (0 : ℝ) := ⟨δ/2, δ, by linarith, by linarith⟩  set f₀ := MeasureTheory.convolution (φ.normed MeasureTheory.volume) f    (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume with f₀def  refine ⟨f₀, ?_, fun x ↦ ?_, fun x ↦ ?_⟩  · exact HasCompactSupport.contDiff_convolution_left _ φ.hasCompactSupport_normed      φ.contDiff_normed unicontf.continuous.locallyIntegrable  · rw [f₀def, MeasureTheory.convolution, MeasureTheory.convolution]    congr with t    congr 1    convert periodicf (x - t) using 2    ring  · rw [← Complex.dist_eq, dist_comm]    exact ContDiffBump.dist_normed_convolution_le unicontf.continuous.aestronglyMeasurable      fun y hy ↦ (hδ hy).le