DiagonalTrace.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.DiagonalNuclear
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open InnerProductSpace
10 open scoped InnerProductSpace Classical ENNReal
11 set_option maxHeartbeats 800000
12 
13 theorem hilbertBasis_hasSum_squared_coordinates {ι E : Type*} [NormedAddCommGroup E]
14     [InnerProductSpace ℂ E] (b : HilbertBasis ι ℂ E) (x : E) :
15     HasSum (fun i => ‖⟪b i, x⟫_ℂ‖ ^ 2) (‖x‖ ^ 2) := by
16   have h := lp.hasSum_norm (by norm_num : (0 : ℝ) < (2 : ℝ≥0∞).toReal) (b.repr x)
17   simpa only [ENNReal.toReal_ofNat, Real.rpow_two, b.repr_apply_apply, b.repr.norm_map] using h
18 
19 theorem diagonal_trace_double_summable {ι κ : Type} {a : ι → ℂ}
20     (ha : Summable (fun i => ‖a i‖)) (b : HilbertBasis κ ℂ (lp (fun _ : ι => ℂ) 2)) :
21     Summable (fun p : ι × κ => a p.1 * ⟪b p.2, diagonalHilbertBasis ι p.1⟫_ℂ *
22       ⟪diagonalHilbertBasis ι p.1, b p.2⟫_ℂ) := by
23   apply Summable.of_norm
24   have hn (i : ι) (j : κ) :
25       ‖a i * ⟪b j, diagonalHilbertBasis ι i⟫_ℂ * ⟪diagonalHilbertBasis ι i, b j⟫_ℂ‖ =
26         ‖a i‖ * ‖⟪b j, diagonalHilbertBasis ι i⟫_ℂ‖ ^ 2 := by
27     rw [norm_mul, norm_mul, norm_inner_symm]
28     ring
29   simp_rw [hn]
30   apply (summable_prod_of_nonneg (fun p => by positivity)).mpr
31   constructor
32   · intro i
33     simpa only using! (hilbertBasis_hasSum_squared_coordinates b (diagonalHilbertBasis ι i)).summable.mul_left ‖a i‖
34   · simpa [tsum_mul_left, (hilbertBasis_hasSum_squared_coordinates b _).tsum_eq] using ha
35 
36 def hilbertBasisTrace {ι E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
37     (b : HilbertBasis ι ℂ E) (T : E →L[ℂ] E) : ℂ := ∑' i, ⟪b i, T (b i)⟫_ℂ
38 
39 theorem diagonalOperator_trace_in_any_basis {ι κ : Type} {a : ι → ℂ}
40     (ha : Summable (fun i => ‖a i‖)) (b : HilbertBasis κ ℂ (lp (fun _ : ι => ℂ) 2)) :
41     HasSum (fun j => ⟪b j, diagonalOperator a (b j)⟫_ℂ) (∑' i, a i) := by
42   have hsum := diagonal_trace_double_summable ha b
43   have hj (j : κ) : HasSum (fun i => a i * ⟪b j, diagonalHilbertBasis ι i⟫_ℂ *
44       ⟪diagonalHilbertBasis ι i, b j⟫_ℂ) ⟪b j, diagonalOperator a (b j)⟫_ℂ := by
45     have h := (hasSum_apply (diagonalRankOne_summable ha).hasSum (b j)).mapL (innerSL ℂ (b j))
46     simpa [diagonalOperator, diagonalRankOne, rankOne_apply, inner_smul_right, mul_comm, mul_left_comm, mul_assoc] using! h
47   have hi (i : ι) : (∑' j, a i * ⟪b j, diagonalHilbertBasis ι i⟫_ℂ *
48       ⟪diagonalHilbertBasis ι i, b j⟫_ℂ) = a i := by
49     calc
50       _ = a i * ∑' j, ⟪diagonalHilbertBasis ι i, b j⟫_ℂ * ⟪b j, diagonalHilbertBasis ι i⟫_ℂ := by
51         rw [← tsum_mul_left]
52         apply tsum_congr
53         intro j
54         ring
55       _ = a i := by
56         rw [b.tsum_inner_mul_inner, inner_self_eq_norm_sq_to_K, diagonalHilbertBasis_norm]
57         simp
58   have hs : Summable (fun j => ∑' i, a i * ⟪b j, diagonalHilbertBasis ι i⟫_ℂ *
59       ⟪diagonalHilbertBasis ι i, b j⟫_ℂ) := hsum.prod_symm.prod
60   have he : (∑' j, ∑' i, a i * ⟪b j, diagonalHilbertBasis ι i⟫_ℂ *
61       ⟪diagonalHilbertBasis ι i, b j⟫_ℂ) = ∑' i, a i := by
62     have ht : (∑' i, ∑' j, a i * ⟪b j, diagonalHilbertBasis ι i⟫_ℂ *
63         ⟪diagonalHilbertBasis ι i, b j⟫_ℂ) =
64         ∑' j, ∑' i, a i * ⟪b j, diagonalHilbertBasis ι i⟫_ℂ *
65         ⟪diagonalHilbertBasis ι i, b j⟫_ℂ := hsum.prod_symm.tsum_comm
66     exact ht.symm.trans (tsum_congr hi)
67   have hh : HasSum (fun j => ∑' i, a i * ⟪b j, diagonalHilbertBasis ι i⟫_ℂ *
68       ⟪diagonalHilbertBasis ι i, b j⟫_ℂ) (∑' i, a i) := by
69     rw [← he]
70     exact hs.hasSum
71   simpa only [(hj _).tsum_eq] using hh
72 
73 theorem diagonalOperator_trace_eq {ι κ : Type} {a : ι → ℂ}
74     (ha : Summable (fun i => ‖a i‖)) (b : HilbertBasis κ ℂ (lp (fun _ : ι => ℂ) 2)) :
75     hilbertBasisTrace b (diagonalOperator a) = ∑' i, a i :=
76   (diagonalOperator_trace_in_any_basis ha b).tsum_eq
77 
78 theorem diagonalOperator_pow_eq {ι : Type} {a : ι → ℂ}
79     (ha : Summable (fun i => ‖a i‖)) (m : ℕ) (hm : Summable (fun i => ‖a i ^ m‖)) :
80     diagonalOperator a ^ m = diagonalOperator (fun i => a i ^ m) := by
81   ext x j
82   rw [diagonalOperator_pow_apply ha, diagonalOperator_apply hm]
83 
84 theorem diagonalOperator_pow_trace {ι κ : Type} {a : ι → ℂ}
85     (ha : Summable (fun i => ‖a i‖)) (m : ℕ) (hm : Summable (fun i => ‖a i ^ m‖))
86     (b : HilbertBasis κ ℂ (lp (fun _ : ι => ℂ) 2)) :
87     hilbertBasisTrace b (diagonalOperator a ^ m) = ∑' i, a i ^ m := by
88   rw [diagonalOperator_pow_eq ha m hm, diagonalOperator_trace_eq hm]
89 
90 end
91 end Komorebi.PaperIV

Back to source controls