Dynin-Mityagin Space Typeclass

Defines the DyninMityaginSpace typeclass for locally convex spaces admitting a rapidly decaying Schauder basis. This formalizes the Dynin-Mityagin theorem: a nuclear Fréchet space with a Schauder basis is isomorphic to a Köthe sequence space with rapidly decaying weights.

The construction of Gaussian measures works for any DyninMityaginSpace E, not just Schwartz spaces.

Main definitions

• DyninMityaginSpace E — typeclass for nuclear Fréchet spaces with Schauder basis
• DyninMityaginSpace.expansion_H — recovery of the Hilbert-space expansion

References

• Dynin, Mityagin, "Criterion for nuclearity in terms of approximative dimension"
• Gel'fand-Vilenkin, "Generalized Functions" Vol. 4, Ch. 3-4

class GaussianField.DyninMityaginSpace (E : Type u_1) [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] extends T1Space E : Type (max 1 u_1)

A nuclear Fréchet space with a countable Schauder basis.

Seminorms and index type are bundled inside the class so that typeclass synthesis can infer everything from E alone. The expansion axiom is stated for scalar functionals φ : E →L[ℝ] ℝ, not arbitrary Hilbert spaces — the Hilbert-space form is recovered as expansion_H.

The class includes h_countable (countable seminorm index) and h_completeSpace (completeness w.r.t. the canonical uniform structure). Together these give BaireSpace E (see DyninMityaginSpace.instBaireSpace) via: countable seminorms → pseudometrizable + complete → Baire.

• t1 (x : E) : IsClosed {x}
• ι : Type

  Index type for the defining seminorm family.

• p : ι E → Seminorm ℝ E

  Defining seminorm family.

• h_with : WithSeminorms p
• h_countable : Countable (ι E)
• h_completeSpace : CompleteSpace E
• basis : ℕ → E

  Schauder basis vectors.

• coeff : ℕ → E →L[ℝ] ℝ

  Coefficient functionals for the basis expansion.

• expansion (φ : E →L[ℝ] ℝ) (f : E) : φ f = ∑' (m : ℕ), (coeff m) f * φ (basis m)
• basis_growth (i : ι E) : ∃ C > 0, ∃ (s : ℕ), ∀ (m : ℕ), (p i) (basis m) ≤ C * (1 + ↑m) ^ s
• coeff_decay (k : ℕ) : ∃ C > 0, ∃ (s : Finset (ι E)), ∀ (f : E) (m : ℕ), |(coeff m) f| * (1 + ↑m) ^ k ≤ C * (s.sup p) f

class GaussianField.DyninMityaginSpace.HasBiorthogonalBasis (E : Type u_1) [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [DyninMityaginSpace E] : Prop

A DyninMityaginSpace with biorthogonal basis and coefficients: coeff n (basis m) = δ_{nm}. This holds for all DM spaces constructed via ofRapidDecayEquiv (including Schwartz spaces and smooth circle functions).

Finite-dimensional spaces with eventually-zero bases do NOT satisfy this.

• coeff_basis (n m : ℕ) : (coeff n) (basis m) = if n = m then 1 else 0

theorem GaussianField.DyninMityaginSpace.expansion_H {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [DyninMityaginSpace E] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (T : E →L[ℝ] H) (w : H) (f : E) : inner ℝ w (T f) = ∑' (m : ℕ), (coeff m) f * inner ℝ w (T (basis m))

The Hilbert-space expansion recovered from the scalar axiom.

For any CLM T : E →L[ℝ] H and w : H, the map f ↦ ⟪w, T f⟫ is a scalar CLF, so the intrinsic DyninMityaginSpace.expansion applies.