EuclideanMatrixNorms.lean

1 import Mathlib.Analysis.CStarAlgebra.Matrix
2 import Mathlib.Analysis.InnerProductSpace.ProdL2
3 
4 set_option autoImplicit false
5 
6 namespace Komorebi.LSM.EuclideanMatrixNorms
7 open scoped Matrix
8 
9 variable {D : Type*}
10 
11 /-- Entry flattening into an actual Euclidean space; no matrix norm instance is used. -/
12 noncomputable def flatten : Matrix D D ℝ ≃ₗ[ℝ] EuclideanSpace ℝ (D × D) where
13   toFun A := WithLp.toLp 2 (fun p => A p.1 p.2)
14   invFun x i j := x (i,j)
15   left_inv A := rfl
16   right_inv x := by ext p; rfl
17   map_add' A B := by ext p; rfl
18   map_smul' a A := by ext p; rfl
19 
20 @[simp] theorem flatten_apply (A : Matrix D D ℝ) (i j : D) :
21     flatten A (i,j) = A i j := rfl
22 
23 @[simp] theorem flatten_symm_apply (x : EuclideanSpace ℝ (D × D)) (i j : D) :
24     flatten.symm x i j = x (i,j) := rfl
25 
26 variable [Fintype D] [DecidableEq D]
27 
28 /-- The actual Frobenius norm, through Euclidean entry flattening. -/
29 noncomputable def frobenius (A : Matrix D D ℝ) : ℝ := ‖flatten A‖
30 
31 /-- The operator norm on Euclidean vectors (the real spectral norm). -/
32 noncomputable def spectralNorm (A : Matrix D D ℝ) : ℝ :=
33   ‖Matrix.toEuclideanCLM (𝕜 := ℝ) A‖
34 
35 omit [DecidableEq D] in
36 theorem frobenius_nonneg (A : Matrix D D ℝ) : 0 ≤ frobenius A := norm_nonneg _
37 
38 theorem spectralNorm_nonneg (A : Matrix D D ℝ) : 0 ≤ spectralNorm A := norm_nonneg _
39 
40 omit [DecidableEq D] in
41 theorem frobenius_sq (A : Matrix D D ℝ) :
42     frobenius A ^ 2 = ∑ i, ∑ j, A i j ^ 2 := by
43   rw [frobenius, EuclideanSpace.real_norm_sq_eq]
44   simp [Fintype.sum_prod_type]
45 
46 omit [DecidableEq D] in
47 theorem frobenius_transpose (A : Matrix D D ℝ) : frobenius Aᵀ = frobenius A := by
48   have hs : frobenius Aᵀ ^ 2 = frobenius A ^ 2 := by
49     simp only [frobenius_sq, Matrix.transpose_apply]
50     exact Finset.sum_comm
51   nlinarith [frobenius_nonneg Aᵀ, frobenius_nonneg A]
52 
53 omit [DecidableEq D] in
54 theorem frobenius_add_le (A B : Matrix D D ℝ) :
55     frobenius (A+B) ≤ frobenius A + frobenius B := by
56   exact (by simpa only [frobenius, map_add] using norm_add_le (flatten A) (flatten B))
57 
58 omit [DecidableEq D] in
59 @[simp] theorem frobenius_zero : frobenius (0 : Matrix D D ℝ) = 0 := by
60   simp [frobenius]
61 
62 omit [DecidableEq D] in
63 @[simp] theorem frobenius_neg (A : Matrix D D ℝ) : frobenius (-A) = frobenius A := by
64   simp [frobenius]
65 
66 omit [DecidableEq D] in
67 theorem frobenius_sub_le (A B : Matrix D D ℝ) :
68     frobenius (A-B) ≤ frobenius A + frobenius B := by
69   simpa only [frobenius, map_sub] using norm_sub_le (flatten A) (flatten B)
70 
71 omit [DecidableEq D] in
72 theorem frobenius_sub_rev (A B : Matrix D D ℝ) : frobenius (A-B) = frobenius (B-A) := by
73   simpa only [frobenius, map_sub] using norm_sub_rev (flatten A) (flatten B)
74 
75 omit [DecidableEq D] in
76 theorem frobenius_smul (c : ℝ) (A : Matrix D D ℝ) :
77     frobenius (c • A) = |c| * frobenius A := by
78   simp [frobenius, norm_smul, Real.norm_eq_abs]
79 
80 omit [DecidableEq D] in
81 @[simp] theorem frobenius_eq_zero (A : Matrix D D ℝ) : frobenius A = 0 ↔ A = 0 := by
82   rw [frobenius, norm_eq_zero]
83   constructor
84   · intro h
85     exact flatten.injective (by simpa using h)
86   · rintro rfl
87     simp
88 
89 theorem spectralNorm_transpose (A : Matrix D D ℝ) : spectralNorm Aᵀ = spectralNorm A := by
90   simpa only [spectralNorm, Matrix.l2_opNorm_toEuclideanCLM,
91     Matrix.conjTranspose_eq_transpose_of_trivial] using (Matrix.l2_opNorm_conjTranspose A)
92 
93 /-- Left multiplication is bounded by the spectral norm on the left and Frobenius on the right. -/
94 theorem frobenius_mul_left (A H : Matrix D D ℝ) :
95     frobenius (A*H) ≤ spectralNorm A * frobenius H := by
96   have hcol (j : D) :
97       (∑ i, (A*H) i j ^ 2) ≤ spectralNorm A ^ 2 * (∑ i, H i j ^ 2) := by
98     let x : EuclideanSpace ℝ D := WithLp.toLp 2 (fun i => H i j)
99     have h := (Matrix.toEuclideanCLM (𝕜 := ℝ) A).le_opNorm x
100     have he : Matrix.toEuclideanCLM (𝕜 := ℝ) A x =
101         WithLp.toLp 2 (fun i => (A*H) i j) := by
102       ext i
103       simp [Matrix.mul_apply, Matrix.mulVec, dotProduct, x]
104     rw [he] at h
105     have hs : ‖WithLp.toLp 2 (fun i => (A*H) i j)‖ ^ 2 ≤
106         spectralNorm A ^ 2 * ‖x‖ ^ 2 := by
107       change ‖WithLp.toLp 2 (fun i => (A*H) i j)‖ ≤ spectralNorm A * ‖x‖ at h
108       nlinarith [norm_nonneg (WithLp.toLp 2 (fun i => (A*H) i j)),
109         norm_nonneg x, spectralNorm_nonneg A]
110     simpa only [EuclideanSpace.real_norm_sq_eq, x] using hs
111   have hs : frobenius (A*H) ^ 2 ≤ (spectralNorm A * frobenius H) ^ 2 := by
112     rw [frobenius_sq, mul_pow, frobenius_sq]
113     calc
114       (∑ i, ∑ j, (A*H) i j ^ 2) = ∑ j, ∑ i, (A*H) i j ^ 2 := Finset.sum_comm
115       _ ≤ ∑ j, spectralNorm A ^ 2 * (∑ i, H i j ^ 2) := Finset.sum_le_sum (fun j _ => hcol j)
116       _ = spectralNorm A ^ 2 * (∑ i, ∑ j, H i j ^ 2) := by
117         rw [← Finset.mul_sum, Finset.sum_comm]
118   nlinarith [frobenius_nonneg (A*H), frobenius_nonneg H, spectralNorm_nonneg A,
119     mul_nonneg (spectralNorm_nonneg A) (frobenius_nonneg H)]
120 
121 /-- The corresponding right multiplication bound follows by transposition. -/
122 theorem frobenius_mul_right (H A : Matrix D D ℝ) :
123     frobenius (H*A) ≤ frobenius H * spectralNorm A := by
124   have h := frobenius_mul_left Aᵀ Hᵀ
125   simpa only [← Matrix.transpose_mul, frobenius_transpose, spectralNorm_transpose,
126     mul_comm (spectralNorm A)] using h
127 
128 /-- The sharp mixed-norm perturbation bound for the literal quadratic congruence. -/
129 theorem frobenius_congruence_sub_le (A B H : Matrix D D ℝ) :
130     frobenius (Aᵀ*H*A - Bᵀ*H*B) ≤
131       (spectralNorm A + spectralNorm B) * spectralNorm (A-B) * frobenius H := by
132   have he : Aᵀ*H*A - Bᵀ*H*B = (A-B)ᵀ*H*A + Bᵀ*H*(A-B) := by
133     rw [Matrix.transpose_sub]
134     noncomm_ring
135   have h₁ := (frobenius_mul_right ((A-B)ᵀ*H) A).trans
136     (mul_le_mul_of_nonneg_right (frobenius_mul_left (A-B)ᵀ H)
137       (spectralNorm_nonneg A))
138   have h₂ := (frobenius_mul_right (Bᵀ*H) (A-B)).trans
139     (mul_le_mul_of_nonneg_right (frobenius_mul_left Bᵀ H)
140       (spectralNorm_nonneg (A-B)))
141   rw [spectralNorm_transpose] at h₁ h₂
142   rw [he]
143   exact (frobenius_add_le _ _).trans (by nlinarith)
144 
145 end Komorebi.LSM.EuclideanMatrixNorms

Back to source controls