DiagonalNuclear.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import Mathlib.Analysis.InnerProductSpace.l2Space
6 import Mathlib.Analysis.InnerProductSpace.Adjoint
7 import Mathlib.Topology.Algebra.InfiniteSum.ContinuousEval
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open InnerProductSpace
12 open scoped InnerProductSpace Classical
13 
14 /-- The nuclear rank-one characterization of trace class on a Hilbert space. -/
15 def IsHilbertTraceClass {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
16     (T : E →L[ℂ] E) : Prop :=
17   ∃ (ι : Type) (x y : ι → E), Summable (fun i => ‖x i‖ * ‖y i‖) ∧
18     HasSum (fun i => rankOne ℂ (x i) (y i)) T
19 
20 def diagonalHilbertBasis (ι : Type) : HilbertBasis ι ℂ (lp (fun _ : ι => ℂ) 2) :=
21   HilbertBasis.ofRepr (LinearIsometryEquiv.refl ℂ _)
22 
23 @[simp] theorem diagonalHilbertBasis_inner {ι : Type} (i : ι) (x : lp (fun _ : ι => ℂ) 2) :
24     ⟪diagonalHilbertBasis ι i, x⟫_ℂ = x i := by
25   exact ((diagonalHilbertBasis ι).repr_apply_apply x i).symm
26 
27 @[simp] theorem diagonalHilbertBasis_norm {ι : Type} (i : ι) : ‖diagonalHilbertBasis ι i‖ = 1 :=
28   (diagonalHilbertBasis ι).orthonormal.norm_eq_one i
29 
30 @[simp] theorem diagonalHilbertBasis_apply {ι : Type} (i j : ι) :
31     diagonalHilbertBasis ι i j = if j = i then 1 else 0 := by
32   have h := congrArg (fun v : lp (fun _ : ι => ℂ) 2 => v j) ((diagonalHilbertBasis ι).repr_self i)
33   simpa [diagonalHilbertBasis, lp.single_apply, Pi.single_apply, eq_comm] using h
34 
35 def diagonalRankOne {ι : Type} (a : ι → ℂ) (i : ι) :
36     lp (fun _ : ι => ℂ) 2 →L[ℂ] lp (fun _ : ι => ℂ) 2 :=
37   rankOne ℂ (a i • diagonalHilbertBasis ι i) (diagonalHilbertBasis ι i)
38 
39 @[simp] theorem diagonalRankOne_norm {ι : Type} (a : ι → ℂ) (i : ι) :
40     ‖diagonalRankOne a i‖ = ‖a i‖ := by simp [diagonalRankOne, norm_smul]
41 
42 theorem diagonalRankOne_summable {ι : Type} {a : ι → ℂ} (ha : Summable (fun i => ‖a i‖)) :
43     Summable (diagonalRankOne a) := by
44   apply Summable.of_norm
45   simpa using ha
46 
47 def diagonalOperator {ι : Type} (a : ι → ℂ) :
48     lp (fun _ : ι => ℂ) 2 →L[ℂ] lp (fun _ : ι => ℂ) 2 := ∑' i, diagonalRankOne a i
49 
50 theorem diagonalOperator_traceClass {ι : Type} {a : ι → ℂ}
51     (ha : Summable (fun i => ‖a i‖)) : IsHilbertTraceClass (diagonalOperator a) := by
52   refine ⟨ι, (fun i => a i • diagonalHilbertBasis ι i), diagonalHilbertBasis ι, ?_, ?_⟩
53   · simpa [norm_smul] using ha
54   · exact (diagonalRankOne_summable ha).hasSum
55 
56 theorem diagonalOperator_apply {ι : Type} {a : ι → ℂ}
57     (ha : Summable (fun i => ‖a i‖)) (x : lp (fun _ : ι => ℂ) 2) (j : ι) :
58     diagonalOperator a x j = a j * x j := by
59   have hs := hasSum_apply (diagonalRankOne_summable ha).hasSum x
60   have hv := hs.mapL (lp.evalCLM ℂ (fun _ : ι => ℂ) 2 j)
61   have he (i : ι) : (lp.evalCLM ℂ (fun _ : ι => ℂ) 2 j) (diagonalRankOne a i x) =
62       x i * (a i * (if j = i then 1 else 0)) := by
63     change (diagonalRankOne a i x) j = _
64     simp [diagonalRankOne, rankOne_apply, lp.coeFn_smul, diagonalHilbertBasis_apply, mul_comm]
65   simp only [he] at hv
66   change HasSum _ (diagonalOperator a x j) at hv
67   simpa [mul_assoc, mul_comm, mul_left_comm, eq_comm] using hv.tsum_eq.symm
68 
69 theorem diagonalOperator_apply_basis {ι : Type} {a : ι → ℂ}
70     (ha : Summable (fun i => ‖a i‖)) (i : ι) :
71     diagonalOperator a (diagonalHilbertBasis ι i) = a i • diagonalHilbertBasis ι i := by
72   ext j
73   simp [diagonalOperator_apply ha, diagonalHilbertBasis_apply]
74   split_ifs with h <;> simp_all
75 
76 theorem diagonalOperator_pow_apply {ι : Type} {a : ι → ℂ}
77     (ha : Summable (fun i => ‖a i‖)) (m : ℕ) (x : lp (fun _ : ι => ℂ) 2) (j : ι) :
78     (diagonalOperator a ^ m) x j = a j ^ m * x j := by
79   induction m with
80   | zero => simp
81   | succ m ih =>
82       rw [pow_succ']
83       change diagonalOperator a ((diagonalOperator a ^ m) x) j = _
84       rw [diagonalOperator_apply ha, ih, pow_succ']
85       ring
86 
87 end
88 end Komorebi.PaperIV

Back to source controls