Nuclear Operators and Nuclear Spaces

Definitions of nuclear operators, Hilbertian seminorms, and nuclear spaces via Hilbert-Schmidt embeddings. Adapted from OSforGFF/IsHilbertNuclear.lean.

References

• Trèves, "Topological Vector Spaces", Ch. 50-51
• Gel'fand-Vilenkin, "Generalized Functions" Vol. 4, Ch. 3-4
• Reed-Simon, "Methods of Modern Mathematical Physics" Vol. 1, §V.3

Nuclear Operators

def IsNuclearMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [hF : CompleteSpace F] (T : E →L[ℝ] F) : Prop

A continuous linear map between normed spaces is nuclear if it admits a representation T(x) = ∑ₙ (φₙ x) • yₙ where ∑ₙ ‖φₙ‖ · ‖yₙ‖ < ∞.

Equations

• IsNuclearMap T = ∃ (φ : ℕ → E →L[ℝ] ℝ) (y : ℕ → F), (Summable fun (n : ℕ) => ‖φ n‖ * ‖y n‖) ∧ ∀ (x : E), T x = ∑' (n : ℕ), (φ n) x • y n

Hilbertian Seminorms

def Seminorm.IsHilbertian {E : Type u_1} [AddCommGroup E] [Module ℝ E] (p : Seminorm ℝ E) : Prop

A seminorm is Hilbertian (comes from an inner product) iff it satisfies the parallelogram law.

Equations

• p.IsHilbertian = ∀ (x y : E), p (x + y) ^ 2 + p (x - y) ^ 2 = 2 * (p x ^ 2 + p y ^ 2)

noncomputable def Seminorm.innerProd {E : Type u_1} [AddCommGroup E] [Module ℝ E] (p : Seminorm ℝ E) (x y : E) : ℝ

The inner product induced by a Hilbertian seminorm via polarization.

Equations

• p.innerProd x y = (p (x + y) ^ 2 - p (x - y) ^ 2) / 4

def Seminorm.IsOrthonormalSeq {E : Type u_1} [AddCommGroup E] [Module ℝ E] (p : Seminorm ℝ E) {n : ℕ} (e : Fin n → E) : Prop

A finite sequence is p-orthonormal: ⟨eᵢ, eⱼ⟩_p = δᵢⱼ.

Equations

• p.IsOrthonormalSeq e = ∀ (i j : Fin n), p.innerProd (e i) (e j) = if i = j then 1 else 0

Hilbert-Schmidt Embeddings

def Seminorm.IsHilbertSchmidtEmbedding {E : Type u_1} [AddCommGroup E] [Module ℝ E] (p q : Seminorm ℝ E) : Prop

The canonical inclusion Ê_p → Ê_q is Hilbert-Schmidt: the sum ∑ q(eₖ)² is uniformly bounded over all finite p-orthonormal sequences.

Equations

• p.IsHilbertSchmidtEmbedding q = (q ≤ p ∧ ∃ (C : ℝ), ∀ (n : ℕ) (e : Fin n → E), p.IsOrthonormalSeq e → ∑ i : Fin n, q (e i) ^ 2 ≤ C)

Nuclear Spaces

class IsHilbertNuclear (E : Type u_1) [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] : Prop

A nuclear space is a locally convex space whose topology is generated by a countable family of Hilbertian seminorms with Hilbert-Schmidt inclusion maps.

Reference: Trèves, "Topological Vector Spaces", Ch. 50, Thm 50.1; Gel'fand-Vilenkin Vol. 4, Ch. 3-4.

• nuclear_hilbert_embeddings : ∃ (p : ℕ → Seminorm ℝ E), (∀ (n : ℕ), (p n).IsHilbertian) ∧ (WithSeminorms fun (n : ℕ) => p n) ∧ ∀ (n : ℕ), (p (n + 1)).IsHilbertSchmidtEmbedding (p n)

Measurable Structure on WeakDual

@[implicit_reducible]

noncomputable instance instMeasurableSpaceWeakDualRealLeanPool {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] : MeasurableSpace (WeakDual ℝ E)

Cylinder σ-algebra on WeakDual ℝ E, generated by evaluation maps. For separable nuclear spaces, this equals the Borel σ-algebra (Bogachev, "Gaussian Measures", Thm 3.6.1), so using it directly avoids needing to prove that difficult direction.

Equations

• instMeasurableSpaceWeakDualRealLeanPool = ⨆ (f : E), MeasurableSpace.comap (fun (l : WeakDual ℝ E) => l f) (borel ℝ)

theorem WeakDual.eval_measurable {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (f : E) : Measurable fun (l : WeakDual ℝ E) => l f

Each evaluation map l ↦ l(f) is measurable w.r.t. the cylinder σ-algebra.