theorem hasFDerivAt_norm_sq {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} : HasFDerivAt (fun (x : F) => ‖x‖ ^ 2) (2 • (innerSL ℝ) x) x

theorem differentiableAt_norm_sq {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} : DifferentiableAt ℝ (fun (x : F) => ‖x‖ ^ 2) x

theorem differentiable_norm_sq {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] : Differentiable ℝ fun (x : F) => ‖x‖ ^ 2

noncomputable def schwartzMap_multidimensional_of_schwartzMap_real (F : Type u_2) [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_2) [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : SchwartzMap ℝ ℂ) (a✝ : F) : (schwartzMap_multidimensional_of_schwartzMap_real F f) a✝ = f (‖a✝‖ ^ 2)