DyninMityaginSpace Instance for Schwartz Space

Derives the DyninMityaginSpace (SchwartzMap D ℝ) instance from the topological isomorphism SchwartzMap D ℝ ≃L[ℝ] RapidDecaySeq constructed in SchwartzNuclear.HermiteTensorProduct.

Main result

• schwartzDyninMityaginSpace: the DyninMityaginSpace instance for Schwartz space on any nontrivial finite-dimensional real normed space.

@[implicit_reducible]

noncomputable instance GaussianField.schwartzDyninMityaginSpace {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] [FiniteDimensional ℝ D] [Nontrivial D] : DyninMityaginSpace (SchwartzMap D ℝ)

Schwartz space is a nuclear Fréchet space.

The instance uses the Schwartz seminorm family (k, l) ↦ p_{k,l} and a basis/coefficient system derived from the topological isomorphism SchwartzMap D ℝ ≃L[ℝ] RapidDecaySeq.

Proved via the topological isomorphism SchwartzMap D ℝ ≃L[ℝ] RapidDecaySeq constructed from multi-dimensional Hermite analysis.

Equations

• GaussianField.schwartzDyninMityaginSpace = GaussianField.DyninMityaginSpace.ofRapidDecayEquiv (fun (kl : ℕ × ℕ) => SchwartzMap.seminorm ℝ kl.1 kl.2) ⋯ (GaussianField.schwartzRapidDecayEquiv D)

@[implicit_reducible]

noncomputable instance GaussianField.schwartzDyninMityaginSpace1D : DyninMityaginSpace (SchwartzMap ℝ ℝ)

Specialized DyninMityaginSpace instance for SchwartzMap ℝ ℝ using schwartzRapidDecayEquiv1D directly, avoiding the toEuclidean detour. This is preferred by instance resolution since ℝ is more specific than D.

Equations

• One or more equations did not get rendered due to their size.

instance GaussianField.schwartzHasBiorthogonalBasis1D : DyninMityaginSpace.HasBiorthogonalBasis (SchwartzMap ℝ ℝ)

HasBiorthogonalBasis for SchwartzMap ℝ ℝ from the Hermite basis.

@[implicit_reducible]

noncomputable instance GaussianField.schwartzDyninMityaginSpaceEuclidean (d : ℕ) : DyninMityaginSpace (SchwartzMap (EuclideanSpace ℝ (Fin (d + 1))) ℝ)

Specialized DyninMityaginSpace instance for SchwartzMap (EuclideanSpace ℝ (Fin (d+1))) ℝ using schwartzRapidDecayEquivNd directly, avoiding the toEuclidean detour. This ensures that DyninMityaginSpace.coeff produces the Hermite coefficients from the standard multi-index encoding, matching the basis used by schwartzPeelOff.

Equations

• One or more equations did not get rendered due to their size.

Separability

RapidDecaySeq is separable because the basis vectors basisVec m span a dense subspace (by hasSum_basisVec). Schwartz space inherits separability via the CLE schwartzRapidDecayEquiv.

instance GaussianField.rapidDecaySeqSeparableSpace : TopologicalSpace.SeparableSpace RapidDecaySeq

RapidDecaySeq is separable: the countable set {basisVec m | m ∈ ℕ} spans a dense subspace (every element is the limit of finite linear combinations by hasSum_basisVec).

instance GaussianField.schwartzSeparableSpace {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] [FiniteDimensional ℝ D] [Nontrivial D] : TopologicalSpace.SeparableSpace (SchwartzMap D ℝ)

Schwartz space is separable.

Proved via the topological isomorphism SchwartzMap D ℝ ≃L[ℝ] RapidDecaySeq: since RapidDecaySeq is separable (countable Hermite basis spans a dense subspace), and a CLE is a homeomorphism, Schwartz space is separable.