/-
Copyright (c) 2025 Michael R. Douglas, Sarah Hoback. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

# 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
-/

import Mathlib.Analysis.LocallyConvex.WithSeminorms
import Mathlib.Topology.Algebra.Module.Spaces.WeakDual
import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
import Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

open scoped BigOperators

noncomputable section

/-! ### Nuclear Operators -/

/-- A continuous linear map between normed spaces is **nuclear** if it admits a
    representation T(x) = ∑ₙ (φₙ x) • yₙ where ∑ₙ ‖φₙ‖ · ‖yₙ‖ < ∞. -/
def IsNuclearMap {E F : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
    (T : E →L[ℝ] F) : Prop :=
  ∃ (φ : ℕ → (E →L[ℝ] ℝ)) (y : ℕ → F),
    Summable (fun n => ‖φ n‖ * ‖y n‖) ∧
    ∀ x, T x = ∑' n, (φ n x) • y n

/-! ### Hilbertian Seminorms -/

/-- A seminorm is **Hilbertian** (comes from an inner product) iff it satisfies
    the parallelogram law. -/
def Seminorm.IsHilbertian {E : Type*} [AddCommGroup E] [Module ℝ E]
    (p : Seminorm ℝ E) : Prop :=
  ∀ x y : E, p (x + y) ^ 2 + p (x - y) ^ 2 = 2 * (p x ^ 2 + p y ^ 2)

/-- The inner product induced by a Hilbertian seminorm via polarization. -/
noncomputable def Seminorm.innerProd {E : Type*} [AddCommGroup E] [Module ℝ E]
    (p : Seminorm ℝ E) (x y : E) : ℝ :=
  (p (x + y) ^ 2 - p (x - y) ^ 2) / 4

/-- A finite sequence is **p-orthonormal**: ⟨eᵢ, eⱼ⟩_p = δᵢⱼ. -/
def Seminorm.IsOrthonormalSeq {E : Type*} [AddCommGroup E] [Module ℝ E]
    (p : Seminorm ℝ E) {n : ℕ} (e : Fin n → E) : Prop :=
  ∀ i j, p.innerProd (e i) (e j) = if i = j then 1 else 0

/-! ### Hilbert-Schmidt Embeddings -/

/-- The canonical inclusion Ê_p → Ê_q is **Hilbert-Schmidt**: the sum ∑ q(eₖ)²
    is uniformly bounded over all finite p-orthonormal sequences. -/
def Seminorm.IsHilbertSchmidtEmbedding {E : Type*} [AddCommGroup E] [Module ℝ E]
    (p q : Seminorm ℝ E) : Prop :=
  q ≤ p ∧
  ∃ (C : ℝ), ∀ (n : ℕ) (e : Fin n → E),
    p.IsOrthonormalSeq e →
    ∑ i, q (e i) ^ 2 ≤ C

/-! ### Nuclear Spaces -/

/-- 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. -/
class IsHilbertNuclear (E : Type*) [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] : Prop where
  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 -/

variable {E : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace 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. -/
instance : MeasurableSpace (WeakDual ℝ E) :=
  ⨆ (f : E), (borel ℝ).comap (fun l : WeakDual ℝ E => (l : E →L[ℝ] ℝ) f)

/-- Each evaluation map `l ↦ l(f)` is measurable w.r.t. the cylinder σ-algebra. -/
lemma WeakDual.eval_measurable (f : E) :
    Measurable (fun l : WeakDual ℝ E => (l : E →L[ℝ] ℝ) f) := by
  rw [measurable_iff_comap_le]
  exact le_iSup (fun (g : E) =>
    (borel ℝ).comap (fun l : WeakDual ℝ E => (l : E →L[ℝ] ℝ) g)) f

end