The multiple of a Schwartz map by x

In this module we define the continuous linear map from the Schwartz space 𝓢(ℝ, 𝕜) to itself which takes a Schwartz map η to the Schwartz map x * η.

def Distribution.powOneMul (𝕜 : Type) [RCLike 𝕜] : SchwartzMap ℝ 𝕜 →L[𝕜] SchwartzMap ℝ 𝕜

The continuous linear map 𝓢(ℝ, 𝕜) →L[𝕜] 𝓢(ℝ, 𝕜) taking a Schwartz map η to x * η.

Equations

• Distribution.powOneMul 𝕜 = SchwartzMap.mkCLM (fun (ψ : SchwartzMap ℝ 𝕜) (x : ℝ) => ↑x * ψ x) ⋯ ⋯ ⋯ ⋯

theorem Distribution.powOneMul_apply (𝕜 : Type) [RCLike 𝕜] (ψ : SchwartzMap ℝ 𝕜) (x : ℝ) : ((powOneMul 𝕜) ψ) x = ↑x * ψ x