Bridge: Pietsch Nuclearity → Bochner IsHilbertNuclear #
Proves that a locally convex space satisfying Pietsch's nuclear dominance condition
is a IsHilbertNuclear in the sense of Bochner/Minlos (Hilbertian seminorms with
Hilbert-Schmidt embeddings).
Strategy #
Given Pietsch nuclearity (every continuous seminorm p is dominated by a nuclear
expansion p(x) ≤ Σₖ |fₖ(x)| · cₖ with |fₖ| ≤ q), we:
- Define a Hilbertian lift
r(x) = √(Σₖ fₖ(x)² · cₖ)which satisfies the parallelogram law and dominatespvia Cauchy-Schwarz. - Prove a Bessel inequality for bounded functionals on Hilbertian seminorms:
if
|φ(x)| ≤ R(x)and{eⱼ}is R-orthonormal, thenΣⱼ φ(eⱼ)² ≤ 1. - Combine to show the inclusion map is Hilbert-Schmidt.
- Build a recursive family
r(n)of Hilbertian seminorms generating the topology with HS embeddings between consecutive levels.
References #
- Pietsch, "Nuclear Locally Convex Spaces" (1972), §4
- Trèves, "Topological Vector Spaces", Ch. 50-51
Pietsch Nuclear Definition (local copy) #
A locally convex TVS is Pietsch nuclear if for every continuous seminorm p,
there exist CLFs fₙ and non-negative reals cₙ with Σ cₙ < ∞, and a
continuous seminorm q ≥ p, such that |fₙ(x)| ≤ q(x) and
p(x) ≤ Σₙ |fₙ(x)| · cₙ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Hilbertian Lift #
Summability of the weighted square series: ∑ₙ fₙ(x)² · cₙ < ∞.
This uses the bound |fₙ(x)| ≤ q(x) to dominate by q(x)² · ∑ cₙ.
The Hilbertian lift of a nuclear expansion: r(x) = √(Σₖ fₖ(x)² · cₖ).
This seminorm satisfies the parallelogram law and dominates the original
seminorm via Cauchy-Schwarz.
The bound |fₙ(x)| ≤ q(x) ensures the series converges and the
triangle inequality holds (Minkowski's inequality for weighted ℓ²).
Equations
- hilbertianLift f c hc_nn hc_sum q hfq = Seminorm.of (fun (x : E) => √(∑' (n : ℕ), (f n) x ^ 2 * c n)) ⋯ ⋯
Instances For
The Hilbertian lift evaluates as r(x) = √(Σₖ fₖ(x)² · cₖ).
The Hilbertian lift satisfies the parallelogram law.
Proof: fₙ(x+y)² + fₙ(x-y)² = (fₙx + fₙy)² + (fₙx - fₙy)² = 2(fₙx² + fₙy²)
for each n (using linearity of fₙ), then sum and take √.
Cauchy-Schwarz: the nuclear expansion is bounded by √(Σcₖ) · r(x).
Σₖ |fₖ(x)|·cₖ ≤ √(Σₖ fₖ(x)²·cₖ) · √(Σₖ cₖ) = √(Σcₖ) · r(x)
Functionals bounded by a dominating seminorm q are also bounded by the
Hilbertian lift: r(x) ≤ √(Σcₖ) · q(x).
Bilinearity of Polarization Inner Product (Jordan-von Neumann) #
ip(x₁ + x₂, y) = ip(x₁, y) + ip(x₂, y) (additivity from parallelogram law).
Uses four applications of the parallelogram identity with different argument pairs, then combines by linear arithmetic.
ip(∑ xⱼ, y) = ∑ ip(xⱼ, y) (finite sum in first argument).
ip(a • x, y) = a * ip(x, y) (real homogeneity).
Proof: t ↦ ip(t•x, y) is additive (from innerProd_add_left) and continuous
(since R is Lipschitz). A continuous additive function ℝ → ℝ is ℝ-linear
by map_real_smul.
Bessel Inequality for Hilbertian Seminorms #
R(∑ⱼ aⱼ • vⱼ)² = ∑ⱼ aⱼ² for R-orthonormal {vⱼ} (by induction using Pythagoras).
Bessel inequality for bounded functionals on Hilbertian seminorms.
If R is a Hilbertian seminorm and φ : E →L[ℝ] ℝ satisfies |φ(x)| ≤ R(x),
then for any finite R-orthonormal sequence {eⱼ}, we have Σⱼ φ(eⱼ)² ≤ 1.
Proof: let w = Σⱼ φ(vⱼ)·vⱼ. By orthonormality R(w)² = Σⱼ φ(vⱼ)²,
by linearity φ(w) = Σⱼ φ(vⱼ)², and |φ(w)| ≤ R(w).
So S ≤ R(w) = √S, giving S ≤ 1.
HS Embedding from Nuclear Factorization #
If R is Hilbertian and p(x) ≤ Σₖ |fₖ(x)| · cₖ where each fₖ is
bounded by R, then the inclusion Ê_R → Ê_p is Hilbert-Schmidt.
For any finite R-orthonormal sequence {eⱼ}:
Σⱼ p(eⱼ)² ≤ Σⱼ (Σₖ |fₖ(eⱼ)|·cₖ)²
≤ (Σₖ cₖ) · Σₖ cₖ·(Σⱼ |fₖ(eⱼ)|²) [Cauchy-Schwarz + swap]
≤ (Σₖ cₖ)² [Bessel: Σⱼ|fₖ(eⱼ)|² ≤ 1]
Recursive Hilbertian Family Construction #
Main Bridge Theorem #
Pietsch nuclearity implies IsHilbertNuclear.
A locally convex space satisfying Pietsch's nuclear dominance condition
(every continuous seminorm is dominated by a nuclear expansion) is a
IsHilbertNuclear in the Hilbertian-seminorm sense.
The proof constructs a recursive family of Hilbertian seminorms from the Pietsch factorizations and shows they have Hilbert-Schmidt embeddings.