noncomputable def schwartzMap_multidimensional_of_schwartzMap_real (F : Type u_1) [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : SchwartzMap ℝ ℂ) : SchwartzMap F ℂ

Equations

• schwartzMap_multidimensional_of_schwartzMap_real F f = (SchwartzMap.compCLM ℝ ⋯ ⋯) f

@[simp]

theorem schwartzMap_multidimensional_of_schwartzMap_real_toFun (F : Type u_1) [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : SchwartzMap ℝ ℂ) (a✝ : F) : (schwartzMap_multidimensional_of_schwartzMap_real F f) a✝ = f (‖a✝‖ ^ 2)