Schwartz space

TheoremThe Gaussian is a Schwartz function#●ready to prove

Let \(E\) be a finite-dimensional real inner product space. Then there is a real-valued Schwartz function \(g\) on \(E\) such that \(g(x) = e^{-\|x\|^2}\) for every \(x \in E\).

public theorem_wanted gaussian_mem_schwartz
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] :
    ∃ g : 𝓢(E, ℝ), ∀ x, g x = Real.exp (-‖x‖ ^ 2)
Sources

TheoremLinear maps on Schwartz space commuting with \(x\) and \(d/dx\) are scalars#●ready to prove

Let \(\mathcal{S}(\mathbb{R})\) be the space of complex-valued Schwartz functions on \(\mathbb{R}\), and let \(M:\mathcal{S}(\mathbb{R})\to\mathcal{S}(\mathbb{R})\) be a \(\mathbb{C}\)-linear map with \((Mf)(x)=x f(x)\) for all \(f\in\mathcal{S}(\mathbb{R})\) and \(x\in\mathbb{R}\). If \(T:\mathcal{S}(\mathbb{R})\to\mathcal{S}(\mathbb{R})\) is a \(\mathbb{C}\)-linear map (not assumed continuous) with \(TM=MT\) and \(T\frac{d}{dx}=\frac{d}{dx}T\), then there exists \(c\in\mathbb{C}\) such that \(Tf=cf\) for all \(f\in\mathcal{S}(\mathbb{R})\).

public theorem_wanted exists_eq_smul_of_comp_mul_eq_of_comp_deriv_eq
    (T : SchwartzMap ℝ ℂ →ₗ[ℂ] SchwartzMap ℝ ℂ)
    (M : SchwartzMap ℝ ℂ →ₗ[ℂ] SchwartzMap ℝ ℂ)
    (hM : ∀ f : SchwartzMap ℝ ℂ, ∀ x : ℝ, M f x = (x : ℂ) * f x)
    (hTM : T.comp M = M.comp T)
    (hTd :
      T.comp (SchwartzMap.derivCLM ℂ ℂ).toLinearMap =
        (SchwartzMap.derivCLM ℂ ℂ).toLinearMap.comp T) :
    ∃ c : ℂ, ∀ f : SchwartzMap ℝ ℂ, T f = c • f
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; General theory of linear operators), problem ma_proofbench_l2_54.
2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.