Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/FiniteAverage.lean, lines 62–71.
Back to A finite-row average centralizes its matrix stage · Back to Normalization and the trace identity determine the CAR trace
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Completion 2import MathlibAnnex.Analysis.CStarAlgebra.FiniteRow 3import MathlibAnnex.Analysis.CStarAlgebra.PositiveMapBound 4import MathlibAnnex.Analysis.CStarAlgebra.VectorGram 5 6/-! 7# Finite-row averaging in the completed CAR algebra 8 9For a full matrix stage, the single column `e_(i,0)` gives an exactly 10normalized row. Its associated positive map commutes with that whole stage, 11and the elementary norm bound is independent of the matrix dimension. Dense 12finite-stage approximation then gives simultaneous approximate centrality on 13an arbitrary finite subset of the actual completed CAR algebra. 14-/ 15 16set_option autoImplicit false 17 18open scoped ComplexOrder Matrix 19 20namespace MathlibAnnex.CStarAlgebra.CAR 21 22/-- A standard matrix unit in a binary CAR stage. -/ 23noncomputable def matrixUnit (n : ℕ) (i j : Fin (2 ^ n)) : Stage n := 24 CStarMatrix.ofMatrix (Matrix.single i j 1) 25 26@[simp] theorem matrixUnit_apply (n : ℕ) (i j k l : Fin (2 ^ n)) : 27 matrixUnit n i j k l = if i = k ∧ j = l then 1 else 0 := by 28 simp [matrixUnit, Matrix.single] 29 30@[simp] theorem star_matrixUnit (n : ℕ) (i j : Fin (2 ^ n)) : 31 star (matrixUnit n i j) = matrixUnit n j i := by 32 ext k l 33 simp [matrixUnit, CStarMatrix.star_apply, Matrix.single, and_comm] 34 35@[simp] theorem matrixUnit_mul_same (n : ℕ) (i j k : Fin (2 ^ n)) : 36 matrixUnit n i j * matrixUnit n j k = matrixUnit n i k := by 37 change CStarMatrix.ofMatrix (Matrix.single i j 1 * Matrix.single j k 1) = _ 38 rw [Matrix.single_mul_single_same] 39 simp [matrixUnit] 40 41@[simp] theorem matrixUnit_mul_of_ne (n : ℕ) (i j k l : Fin (2 ^ n)) (h : j ≠ k) : 42 matrixUnit n i j * matrixUnit n k l = 0 := by 43 change CStarMatrix.ofMatrix (Matrix.single i j 1 * Matrix.single k l 1) = _ 44 rw [Matrix.single_mul_single_of_ne _ _ _ _ h] 45 rfl 46 47@[simp] theorem sum_matrixUnit_diag (n : ℕ) : 48 ∑ i : Fin (2 ^ n), matrixUnit n i i = 1 := by 49 change CStarMatrix.ofMatrix (∑ i : Fin (2 ^ n), Matrix.single i i 1) = _ 50 rw [Matrix.sum_single_one] 51 rfl 52 53/-- A standard matrix unit viewed in the actual completed CAR algebra. -/ 54noncomputable def limitMatrixUnit (n : ℕ) (i j : Fin (2 ^ n)) : Limit := 55 ofStage n (matrixUnit n i j) 56 57@[simp] theorem star_limitMatrixUnit (n : ℕ) (i j : Fin (2 ^ n)) : 58 star (limitMatrixUnit n i j) = limitMatrixUnit n j i := by 59 rw [limitMatrixUnit, ← map_star, star_matrixUnit] 60 rfl 61 62@[simp] theorem limitMatrixUnit_mul (n : ℕ) (i j k l : Fin (2 ^ n)) : 63 limitMatrixUnit n i j * limitMatrixUnit n k l = 64 if j = k then limitMatrixUnit n i l else 0 := by 65 by_cases h : j = k 66 · subst k 67 rw [limitMatrixUnit, limitMatrixUnit, ← map_mul, matrixUnit_mul_same] 68 simp [limitMatrixUnit] 69 · rw [limitMatrixUnit, limitMatrixUnit, ← map_mul, matrixUnit_mul_of_ne _ _ _ _ _ h, 70 map_zero] 71 simp [h] 72 73@[simp] theorem sum_limitMatrixUnit_diag (n : ℕ) : 74 ∑ i : Fin (2 ^ n), limitMatrixUnit n i i = 1 := by 75 calc 76 ∑ i : Fin (2 ^ n), limitMatrixUnit n i i = 77 ofStage n (∑ i : Fin (2 ^ n), matrixUnit n i i) := by 78 rw [map_sum] 79 rfl 80 _ = 1 := by rw [sum_matrixUnit_diag, map_one] 81 82/-- The finite-row average associated to a full matrix stage. -/ 83noncomputable def rowAverageLinear (n : ℕ) : Limit →ₗ[ℂ] Limit where 84 toFun b := ∑ i : Fin (2 ^ n), 85 limitMatrixUnit n i 0 * b * limitMatrixUnit n 0 i 86 map_add' b c := by 87 simp only [mul_add, add_mul, Finset.sum_add_distrib] 88 map_smul' c b := by 89 simp only [RingHom.id_apply, Algebra.smul_def] 90 rw [Finset.mul_sum] 91 apply Finset.sum_congr rfl 92 intro i _ 93 calc 94 limitMatrixUnit n i 0 * ((algebraMap ℂ Limit) c * b) * 95 limitMatrixUnit n 0 i = 96 (limitMatrixUnit n i 0 * (algebraMap ℂ Limit) c) * b * 97 limitMatrixUnit n 0 i := by simp only [mul_assoc] 98 _ = ((algebraMap ℂ Limit) c * limitMatrixUnit n i 0) * b * 99 limitMatrixUnit n 0 i := by 100 rw [Algebra.commutes c (limitMatrixUnit n i 0)] 101 _ = (algebraMap ℂ Limit) c * 102 (limitMatrixUnit n i 0 * b * limitMatrixUnit n 0 i) := by 103 simp only [mul_assoc] 104 105@[simp] theorem rowAverageLinear_apply (n : ℕ) (b : Limit) : 106 rowAverageLinear n b = ∑ i : Fin (2 ^ n), 107 limitMatrixUnit n i 0 * b * limitMatrixUnit n 0 i := rfl 108 109@[simp] theorem rowAverageLinear_one (n : ℕ) : rowAverageLinear n 1 = 1 := by 110 simp [rowAverageLinear] 111 112theorem rowAverageLinear_nonneg (n : ℕ) (b : Limit) (hb : 0 ≤ b) : 113 0 ≤ rowAverageLinear n b := by 114 rw [rowAverageLinear_apply] 115 apply Finset.sum_nonneg 116 intro i _ 117 simpa only [star_limitMatrixUnit] using 118 (star_right_conjugate_nonneg hb (limitMatrixUnit n i 0)) 119 120noncomputable def rowAveragePositive (n : ℕ) : Limit →ₚ[ℂ] Limit := 121 PositiveLinearMap.mk₀ (rowAverageLinear n) (rowAverageLinear_nonneg n) 122 123theorem norm_rowAverageLinear_le (n : ℕ) (b : Limit) : 124 ‖rowAverageLinear n b‖ ≤ 4 * ‖b‖ := by 125 exact MathlibAnnex.CStarAlgebra.norm_apply_le_four (rowAveragePositive n) 126 (rowAverageLinear_one n) b 127 128/-- The finite-row average as a bounded linear operator. -/ 129noncomputable def rowAverage (n : ℕ) : Limit →L[ℂ] Limit := 130 (rowAverageLinear n).mkContinuous 4 (norm_rowAverageLinear_le n) 131 132@[simp] theorem rowAverage_apply (n : ℕ) (b : Limit) : 133 rowAverage n b = rowAverageLinear n b := rfl 134 135/-- Commuting with `a` after applying the finite-row average. -/ 136noncomputable def commutatorAverageLinear (n : ℕ) (a : Limit) : Limit →ₗ[ℂ] Limit where 137 toFun b := a * rowAverageLinear n b - rowAverageLinear n b * a 138 map_add' b c := by simp only [map_add, mul_add, add_mul, sub_add_sub_comm] 139 map_smul' c b := by 140 rw [map_smul] 141 simp only [RingHom.id_apply, Algebra.smul_def] 142 rw [mul_sub] 143 congr 1 144 · calc 145 a * ((algebraMap ℂ Limit) c * rowAverageLinear n b) = 146 (a * (algebraMap ℂ Limit) c) * rowAverageLinear n b := by 147 rw [mul_assoc] 148 _ = ((algebraMap ℂ Limit) c * a) * rowAverageLinear n b := by 149 rw [Algebra.commutes c a] 150 _ = (algebraMap ℂ Limit) c * (a * rowAverageLinear n b) := by 151 rw [mul_assoc] 152 · rw [mul_assoc] 153 154theorem norm_commutatorAverageLinear_le (n : ℕ) (a b : Limit) : 155 ‖commutatorAverageLinear n a b‖ ≤ (8 * ‖a‖) * ‖b‖ := by 156 change ‖a * rowAverageLinear n b - rowAverageLinear n b * a‖ ≤ _ 157 calc 158 ‖a * rowAverageLinear n b - rowAverageLinear n b * a‖ ≤ 159 ‖a * rowAverageLinear n b‖ + ‖rowAverageLinear n b * a‖ := norm_sub_le _ _ 160 _ ≤ ‖a‖ * ‖rowAverageLinear n b‖ + ‖rowAverageLinear n b‖ * ‖a‖ := 161 add_le_add (norm_mul_le _ _) (norm_mul_le _ _) 162 _ = 2 * ‖a‖ * ‖rowAverageLinear n b‖ := by ring 163 _ ≤ 2 * ‖a‖ * (4 * ‖b‖) := by 164 gcongr 165 exact norm_rowAverageLinear_le n b 166 _ = (8 * ‖a‖) * ‖b‖ := by ring 167 168/-- The averaged commutator as a bounded linear operator on the CAR algebra. -/ 169noncomputable def commutatorAverage (n : ℕ) (a : Limit) : Limit →L[ℂ] Limit := 170 (commutatorAverageLinear n a).mkContinuous (8 * ‖a‖) 171 (norm_commutatorAverageLinear_le n a) 172 173@[simp] theorem commutatorAverage_apply (n : ℕ) (a b : Limit) : 174 commutatorAverage n a b = 175 a * rowAverageLinear n b - rowAverageLinear n b * a := rfl 176 177theorem limitMatrixUnit_commute_rowAverage (n : ℕ) (k l : Fin (2 ^ n)) (b : Limit) : 178 limitMatrixUnit n k l * rowAverageLinear n b = 179 rowAverageLinear n b * limitMatrixUnit n k l := by 180 calc 181 limitMatrixUnit n k l * rowAverageLinear n b = 182 ∑ i : Fin (2 ^ n), limitMatrixUnit n k l * 183 (limitMatrixUnit n i 0 * b * limitMatrixUnit n 0 i) := by 184 rw [rowAverageLinear_apply, Finset.mul_sum] 185 _ = limitMatrixUnit n k 0 * b * limitMatrixUnit n 0 l := by 186 rw [Finset.sum_eq_single l] 187 · simp [← mul_assoc] 188 · intro i _ hil 189 have hli : l ≠ i := Ne.symm hil 190 simp [← mul_assoc, hli] 191 · simp 192 _ = ∑ i : Fin (2 ^ n), 193 (limitMatrixUnit n i 0 * b * limitMatrixUnit n 0 i) * 194 limitMatrixUnit n k l := by 195 rw [Finset.sum_eq_single k] 196 · simp [mul_assoc] 197 · intro i _ hik 198 simp [mul_assoc, hik] 199 · simp 200 _ = rowAverageLinear n b * limitMatrixUnit n k l := by 201 rw [rowAverageLinear_apply, Finset.sum_mul] 202 203set_option backward.isDefEq.respectTransparency false in 204theorem stage_eq_sum_smul_matrixUnit (n : ℕ) (c : Stage n) : 205 c = ∑ i : Fin (2 ^ n), ∑ j : Fin (2 ^ n), c i j • matrixUnit n i j := by 206 apply (CStarMatrix.ofMatrixₗ (R := ℂ)).symm.injective 207 simp only [map_sum, map_smul] 208 change CStarMatrix.ofMatrix.symm c = 209 ∑ i : Fin (2 ^ n), ∑ j : Fin (2 ^ n), 210 c i j • Matrix.single i j 1 211 rw [Matrix.matrix_eq_sum_single (CStarMatrix.ofMatrix.symm c)] 212 apply Finset.sum_congr rfl 213 intro i _ 214 apply Finset.sum_congr rfl 215 intro j _ 216 ext k l 217 simp [Matrix.single] 218 219theorem ofStage_eq_sum_smul_limitMatrixUnit (n : ℕ) (c : Stage n) : 220 ofStage n c = 221 ∑ i : Fin (2 ^ n), ∑ j : Fin (2 ^ n), c i j • limitMatrixUnit n i j := by 222 conv_lhs => rw [stage_eq_sum_smul_matrixUnit n c] 223 simp only [map_sum, map_smul, limitMatrixUnit] 224 225theorem ofStage_commute_rowAverage (n : ℕ) (c : Stage n) (b : Limit) : 226 ofStage n c * rowAverageLinear n b = rowAverageLinear n b * ofStage n c := by 227 rw [ofStage_eq_sum_smul_limitMatrixUnit] 228 apply (Commute.sum_left Finset.univ _ _ fun i _ => 229 Commute.sum_left Finset.univ _ _ fun j _ => ?_).eq 230 exact (show Commute (limitMatrixUnit n i j) (rowAverageLinear n b) from 231 limitMatrixUnit_commute_rowAverage n i j b).smul_left (c i j) 232 233theorem exists_stage_approx (a : Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 234 ∃ n, ∃ c : Stage n, ‖a - ofStage n c‖ < epsilon := by 235 obtain ⟨y, hy, hya⟩ := dense_stageRange.exists_dist_lt a hepsilon 236 rcases Set.mem_iUnion.mp hy with ⟨n, hn⟩ 237 rcases hn with ⟨c, rfl⟩ 238 exact ⟨n, c, by simpa only [dist_eq_norm, norm_sub_rev] using hya⟩ 239 240theorem exists_common_stage_approx (F : Finset Limit) {epsilon : ℝ} 241 (hepsilon : 0 < epsilon) : 242 ∃ n, ∀ a ∈ F, ∃ c : Stage n, ‖a - ofStage n c‖ < epsilon := by 243 classical 244 induction F using Finset.induction with 245 | empty => 246 exact ⟨0, by simp⟩ 247 | @insert a F ha ih => 248 obtain ⟨n, c, hc⟩ := exists_stage_approx a hepsilon 249 obtain ⟨m, hm⟩ := ih 250 refine ⟨max n m, ?_⟩ 251 intro x hx 252 rcases Finset.mem_insert.mp hx with rfl | hx 253 · refine ⟨embed n (max n m) (le_max_left n m) c, ?_⟩ 254 simpa only [ofStage_embed] using hc 255 · obtain ⟨d, hd⟩ := hm x hx 256 refine ⟨embed m (max n m) (le_max_right n m) d, ?_⟩ 257 simpa only [ofStage_embed] using hd 258 259theorem norm_commutator_rowAverage_le (n : ℕ) (a b : Limit) (c : Stage n) : 260 ‖a * rowAverageLinear n b - rowAverageLinear n b * a‖ ≤ 261 8 * ‖a - ofStage n c‖ * ‖b‖ := by 262 let p := rowAverageLinear n b 263 let d := a - ofStage n c 264 have hcomm : ofStage n c * p = p * ofStage n c := 265 ofStage_commute_rowAverage n c b 266 have hid : a * p - p * a = d * p - p * d := by 267 dsimp only [d] 268 noncomm_ring [hcomm] 269 rw [hid] 270 calc 271 ‖d * p - p * d‖ ≤ ‖d * p‖ + ‖p * d‖ := norm_sub_le _ _ 272 _ ≤ ‖d‖ * ‖p‖ + ‖p‖ * ‖d‖ := 273 add_le_add (norm_mul_le _ _) (norm_mul_le _ _) 274 _ = 2 * ‖d‖ * ‖p‖ := by ring 275 _ ≤ 2 * ‖d‖ * (4 * ‖b‖) := by 276 gcongr 277 exact norm_rowAverageLinear_le n b 278 _ = 8 * ‖a - ofStage n c‖ * ‖b‖ := by 279 dsimp only [d] 280 ring 281 282theorem norm_commutatorAverage_le_of_stage (n : ℕ) (a : Limit) (c : Stage n) : 283 ‖commutatorAverage n a‖ ≤ 8 * ‖a - ofStage n c‖ := by 284 apply ContinuousLinearMap.opNorm_le_bound _ (by positivity) 285 intro b 286 simpa only [commutatorAverage_apply, mul_assoc] using 287 norm_commutator_rowAverage_le n a b c 288 289@[simp] theorem row_isometry_sum (n : ℕ) : 290 ∑ i : Fin (2 ^ n), limitMatrixUnit n i 0 * star (limitMatrixUnit n i 0) = 1 := by 291 simpa using sum_limitMatrixUnit_diag n 292 293/-- Exact normalization survives every unital star representation. -/ 294theorem map_row_isometry_sum 295 {B : Type*} [Semiring B] [StarRing B] [Algebra ℂ B] 296 (rho : Limit →⋆ₐ[ℂ] B) (n : ℕ) : 297 ∑ i : Fin (2 ^ n), 298 rho (limitMatrixUnit n i 0) * star (rho (limitMatrixUnit n i 0)) = 1 := by 299 calc 300 ∑ i : Fin (2 ^ n), 301 rho (limitMatrixUnit n i 0) * star (rho (limitMatrixUnit n i 0)) = 302 ∑ i : Fin (2 ^ n), rho 303 (limitMatrixUnit n i 0 * star (limitMatrixUnit n i 0)) := by 304 apply Finset.sum_congr rfl 305 intro i _ 306 rw [map_mul, map_star] 307 _ = rho (∑ i : Fin (2 ^ n), 308 limitMatrixUnit n i 0 * star (limitMatrixUnit n i 0)) := by 309 rw [map_sum] 310 _ = 1 := by rw [row_isometry_sum, map_one] 311 312/-- Consequently the Property 1.3 compression equation is exact for every 313operator `E`; no faithfulness or finite-rank assumption is needed here. -/ 314theorem map_row_isometry_sum_mul 315 {B : Type*} [Semiring B] [StarRing B] [Algebra ℂ B] 316 (rho : Limit →⋆ₐ[ℂ] B) (n : ℕ) (E : B) : 317 (∑ i : Fin (2 ^ n), 318 rho (limitMatrixUnit n i 0) * star (rho (limitMatrixUnit n i 0))) * E = E := by 319 rw [map_row_isometry_sum rho n, one_mul] 320 321/-- In a Hilbert-space representation, the pulled-back row vectors have 322exact total squared norm. This is the normalization used by the subsequent 323Gram comparison; no orthogonality of the row vectors is asserted. -/ 324theorem sum_norm_sq_map_limitMatrixUnit_star 325 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 326 (rho : Limit →⋆ₐ[ℂ] (H →L[ℂ] H)) (n : ℕ) (ξ : H) : 327 ∑ i : Fin (2 ^ n), 328 ‖rho (star (limitMatrixUnit n i 0)) ξ‖ ^ 2 = ‖ξ‖ ^ 2 := by 329 exact MathlibAnnex.Analysis.CStarAlgebra.Representation.sum_norm_sq_map_star_eq 330 rho ξ (fun i => limitMatrixUnit n i 0) (row_isometry_sum n) 331 332/-- Actual CAR finite-row averaging with a dimension-independent estimate. 333The same row works simultaneously for the finite set and every test element `b`. -/ 334theorem exists_row_approx_central (F : Finset Limit) {epsilon : ℝ} 335 (hepsilon : 0 < epsilon) : 336 ∃ n, 337 (∑ i : Fin (2 ^ n), 338 limitMatrixUnit n i 0 * star (limitMatrixUnit n i 0) = 1) ∧ 339 ∀ a ∈ F, ∀ b : Limit, 340 ‖a * rowAverageLinear n b - rowAverageLinear n b * a‖ ≤ epsilon * ‖b‖ := by 341 obtain ⟨n, hn⟩ := exists_common_stage_approx F (show 0 < epsilon / 8 by positivity) 342 refine ⟨n, row_isometry_sum n, ?_⟩ 343 intro a ha b 344 obtain ⟨c, hc⟩ := hn a ha 345 calc 346 ‖a * rowAverageLinear n b - rowAverageLinear n b * a‖ ≤ 347 8 * ‖a - ofStage n c‖ * ‖b‖ := norm_commutator_rowAverage_le n a b c 348 _ ≤ epsilon * ‖b‖ := by 349 gcongr 350 exact (lt_div_iff₀' (by norm_num : (0 : ℝ) < 8)).mp hc |>.le 351 352/-- The actual completed CAR algebra supplies the source-independent 353finite-row averaging property. -/ 354theorem hasFiniteRowAveraging_limit : 355 MathlibAnnex.CStarAlgebra.HasFiniteRowAveraging Limit := by 356 intro F epsilon hepsilon 357 obtain ⟨n, hrow, hcomm⟩ := exists_row_approx_central F hepsilon 358 refine ⟨2 ^ n, (fun i => limitMatrixUnit n i 0), hrow, ?_⟩ 359 intro a ha b 360 simpa only [MathlibAnnex.CStarAlgebra.finiteRowAverage, 361 star_limitMatrixUnit, rowAverageLinear_apply] using hcomm a ha b 362 363/-- Operator-norm form of the CAR finite-row property. This is the exact 364`ad a ∘ Ad x` estimate used in Property 1.3, with an exactly normalized row. -/ 365theorem exists_row_average_opNorm_lt (F : Finset Limit) {epsilon : ℝ} 366 (hepsilon : 0 < epsilon) : 367 ∃ n, 368 (∑ i : Fin (2 ^ n), 369 limitMatrixUnit n i 0 * star (limitMatrixUnit n i 0) = 1) ∧ 370 ∀ a ∈ F, ‖commutatorAverage n a‖ < epsilon := by 371 obtain ⟨n, hn⟩ := exists_common_stage_approx F (show 0 < epsilon / 8 by positivity) 372 refine ⟨n, row_isometry_sum n, ?_⟩ 373 intro a ha 374 obtain ⟨c, hc⟩ := hn a ha 375 calc 376 ‖commutatorAverage n a‖ ≤ 8 * ‖a - ofStage n c‖ := 377 norm_commutatorAverage_le_of_stage n a c 378 _ < epsilon := (lt_div_iff₀' (by norm_num : (0 : ℝ) < 8)).mp hc 379 380end MathlibAnnex.CStarAlgebra.CAR