Documentation

LeanPool.OSforGFF.GaussianField.Nuclear.NuclearSpace

Nuclear Spaces (Pietsch characterization) #

Defines the standard NuclearSpace typeclass (Pietsch characterization) and proves that the Dynin-Mityagin characterization (DyninMityaginSpace) implies it.

Two notions of nuclearity #

The DyninMityaginSpace typeclass uses the Dynin-Mityagin characterization: a Schauder basis with polynomial growth/decay in seminorms. This is strictly stronger than Pietsch nuclearity (seminorm nuclear dominance) because it additionally requires the existence of a Schauder basis.

The converse (Pietsch → Dynin-Mityagin) holds only for nuclear Fréchet spaces that already possess a Schauder basis (the Dynin-Mityagin theorem). We do not formalize that direction since our applications (Schwartz spaces) obtain the DM structure directly from the Hermite basis.

Main definitions and results #

References #

Nuclear Space Definition (Pietsch) #

source
class GaussianField.NuclearSpace (E : Type u_1) [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] :
Prop

A locally convex topological vector space over ℝ is nuclear if for every continuous seminorm p, there exist continuous linear functionals (fₙ : E →L[ℝ] ℝ) and non-negative reals (cₙ) with Σ cₙ < ∞, and a continuous seminorm q ≥ p, such that:

(1) p(x) ≤ Σₙ ‖fₙ(x)‖ · cₙ for all x (2) ‖fₙ(x)‖ ≤ q(x) for all x, n

This is Pietsch's characterization, equivalent to Grothendieck's definition that the canonical map E_q → E_p between seminorm completions is nuclear.

Instances

    Hahn-Banach for Continuous Seminorms #

    source
    theorem GaussianField.exists_CLF_le_seminorm {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (q : Seminorm ℝ E) (hq : Continuous ⇑q) (f : E) :
    ∃ (φ : E →L[ℝ] ℝ), φ f = q f ∧ ∀ (x : E), |φ x| ≤ q x

    Hahn-Banach for continuous seminorms.

    For a continuous seminorm q and any vector f, there exists a continuous linear functional φ attaining q at f and bounded by q everywhere.

    Helper Lemmas for the Bridge Proof #

    source
    theorem GaussianField.finset_sup_poly_bound {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} (p' : ι → Seminorm ℝ E) (s : Finset ι) (x : ℕ → E) (hx : ∀ i ∈ s, ∃ C > 0, ∃ (t : ℕ), ∀ (m : ℕ), (p' i) (x m) ≤ C * (1 + ↑m) ^ t) :
    ∃ D > 0, ∃ (S : ℕ), ∀ (m : ℕ), (s.sup p') (x m) ≤ D * (1 + ↑m) ^ S

    Auxiliary: a finset sup of seminorms applied to a sequence with polynomial growth in each seminorm has a uniform polynomial bound.

    Given p' : ι → Seminorm ℝ E and a finite set s, if each p' i for i ∈ s satisfies p' i (x m) ≤ Cᵢ · (1+m)^{tᵢ}, then (s.sup p') (x m) ≤ D · (1+m)^S where S = max tᵢ and D = ∑ Cᵢ.

    source
    theorem GaussianField.seminorm_le_nuclear_expansion {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [hN : DyninMityaginSpace E] (q : Seminorm ℝ E) (hq : Continuous ⇑q) (f : E) :
    q f ≤ ∑' (m : ℕ), |(DyninMityaginSpace.coeff m) f| * q (DyninMityaginSpace.basis m)

    Seminorm bound from Schauder expansion.

    For a continuous seminorm q and a Schauder basis with expansion f = ∑ₘ cₘ(f) · ψₘ, the triangle inequality gives q(f) ≤ ∑ₘ |cₘ(f)| · q(ψₘ).

    The proof uses Hahn-Banach to find a CLF φ with φ(f) = q(f) and |φ| ≤ q, then applies the Schauder expansion to φ and bounds the resulting tsum.

    Strong Convergence of Schauder Expansion #

    source
    theorem GaussianField.DyninMityaginSpace.summable_coeff_seminorm_basis {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [hN : DyninMityaginSpace E] (i : ι E) (f : E) :
    Summable fun (m : ℕ) => |(coeff m) f| * (p i) (basis m)

    Summability of the Schauder expansion terms in a single seminorm.

    For any seminorm index i and vector f, the series ∑ₘ |cₘ(f)| · pᵢ(ψₘ) converges. The proof combines coefficient decay (exponent S+2) with basis growth (exponent S) to produce a summable majorant 1/(1+m)².

    source
    theorem GaussianField.DyninMityaginSpace.hasSum_basis {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [hN : DyninMityaginSpace E] (f : E) :
    HasSum (fun (m : ℕ) => (coeff m) f • basis m) f

    Strong convergence of the Schauder expansion.

    For any f : E in a DyninMityaginSpace, the series ∑ₘ cₘ(f) • ψₘ converges to f in the locally convex topology. The proof uses Hahn-Banach for each seminorm to bound the remainder by the tail of the summable series ∑ₘ |cₘ(f)| · pᵢ(ψₘ).

    Bridge: Dynin-Mityagin → Pietsch #

    source
    theorem GaussianField.DyninMityaginSpace.toNuclearSpace (E : Type u_1) [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [hN : DyninMityaginSpace E] :
    NuclearSpace E

    Dynin-Mityagin implies Pietsch nuclearity.

    A GaussianField.DyninMityaginSpace (Schauder basis with polynomial growth/decay) gives rise to a NuclearSpace (Pietsch nuclear dominance).

    Proof sketch. Given a continuous seminorm p:

    1. Bound p by the defining seminorms: p ≤ C₁ · (s₁.sup hN.p)
    2. Get uniform polynomial growth: (s₁.sup hN.p)(ψₘ) ≤ D · (1+m)^S
    3. Get coefficient decay with extra room: |cₘ(f)| · (1+m)^{S+2} ≤ C₂ · (s₂.sup hN.p)(f)
    4. Define CLFs fₘ := (1+m)^{S+2} · cₘ and coefficients aₘ := C₁ · D · (1+m)^{-(2:ℤ)} (summable since exponent < -1)
    5. The dominating seminorm is q := C₁ · s₁.sup(p) + C₂ · s₂.sup(p)