Multidimensional Radial Schwartz Functions

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)

theorem isRadial_schwartzMap_multidimensional_of_schwartzMap_real (F : Type u_1) [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : SchwartzMap ℝ ℂ) : Function.IsRadial ⇑(schwartzMap_multidimensional_of_schwartzMap_real F f)

The multidimensional lift x ↦ f (‖x‖ ^ 2) of a real Schwartz function is radial.

theorem contDiff_ofReal {n : WithTop ℕ∞} : ContDiff ℝ n Complex.ofReal

theorem eq_schwartzMap {f : ℝ → ℂ} {a : ℝ} (smooth : ContDiff ℝ (↑⊤) f) (decay : ∀ (k n : ℕ), ∃ (C : ℝ), ∀ (x : ℝ), a - 1 ≤ x → ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C) : ∃ (F : SchwartzMap ℝ ℂ), Set.EqOn f (⇑F) (Set.Ici a)