theorem HadamardDecomposition.continuous_fderiv_comp_smul_path {n : ℕ} (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (x v : EuclideanSpace ℝ (Fin n)) : Continuous fun (t : ℝ) => (fderiv ℝ (⇑φ) (t • x)) v

Helper for the Hadamard / fundamental-theorem-of-calculus identity: the map t ↦ (Dφ)(t · x) v is continuous, since it is the composition of the continuous Schwartz Fréchet derivative Dφ, the continuous ray t ↦ t · x, and continuous evaluation at the fixed vector v.