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

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

theorem hasTemperateGrowth_norm_sq {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] : Function.HasTemperateGrowth fun (x : F) => ‖x‖ ^ 2

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 ℝ ℂ) (x : F) : (schwartzMap_multidimensional_of_schwartzMap_real F f) x = f (‖x‖ ^ 2)