Derivatives of continuous loops in terms of Fourier coefficients

Let $\varphi,h:S^1\to\mathbb{R}^{2n}$ be continuous, $S^1=\mathbb{R}/\mathbb{Z}$, and regard them as $1$-periodic functions on $\mathbb{R}$. With Fourier coefficients $\hat g_k=\int_{S^1}e^{-2\pi i k t}g(t)\,dt\in\mathbb{C}^{2n}$ (Haar probability measure), the following are equivalent:

1. $t\mapsto\varphi(t)$ is differentiable at every $t\in\mathbb{R}$ with derivative $h(t)$;
2. $\hat h_k=2\pi i k\,\hat\varphi_k$ for every $k\in\mathbb{Z}$.

This identifies classical derivatives of continuous loops with the Fourier-side derivative $\hat f_k\mapsto 2\pi i k\,\hat f_k$ that defines the asymptotic operator $A_S=-J_0\partial_t-S$ on $W^{1,2}(S^1,\mathbb{R}^{2n})$, in both directions: continuous solutions of the Fourier-side equation are classical solutions, and classical periodic solutions satisfy it.

Formalization Note. φ h : C(UnitAddCircle, Vec n) with Vec n = EuclideanSpace ℝ (Fin n ⊕ Fin n); condition 1 is ∀ x : ℝ, HasDerivAt (fun y : ℝ => φ ↑y) (h ↑x) x; condition 2 is ∀ k : ℤ, coeff h k = ((2 * π * k : ℝ) * I) • coeff φ k, with coeff the componentwise fourierCoeff of the complexification (setting module).