Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/FiniteAverage.lean
Pinned GitHub source · Raw UTF-8 source
Back to Normalization and the trace identity determine the CAR trace · Back to A finite-row average centralizes its matrix stage
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Completion2import MathlibAnnex.Analysis.CStarAlgebra.FiniteRow3import MathlibAnnex.Analysis.CStarAlgebra.PositiveMapBound4import MathlibAnnex.Analysis.CStarAlgebra.VectorGram56/-!7# Finite-row averaging in the completed CAR algebra89For a full matrix stage, the single column `e_(i,0)` gives an exactly10normalized row. Its associated positive map commutes with that whole stage,11and the elementary norm bound is independent of the matrix dimension. Dense12finite-stage approximation then gives simultaneous approximate centrality on13an arbitrary finite subset of the actual completed CAR algebra.14-/1516set_option autoImplicit false1718open scoped ComplexOrder Matrix1920namespace MathlibAnnex.CStarAlgebra.CAR2122/-- 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)2526@[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 := by28 simp [matrixUnit, Matrix.single]2930@[simp] theorem star_matrixUnit (n : ℕ) (i j : Fin (2 ^ n)) :31 star (matrixUnit n i j) = matrixUnit n j i := by32 ext k l33 simp [matrixUnit, CStarMatrix.star_apply, Matrix.single, and_comm]3435@[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 := by37 change CStarMatrix.ofMatrix (Matrix.single i j 1 * Matrix.single j k 1) = _38 rw [Matrix.single_mul_single_same]39 simp [matrixUnit]4041@[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 := by43 change CStarMatrix.ofMatrix (Matrix.single i j 1 * Matrix.single k l 1) = _44 rw [Matrix.single_mul_single_of_ne _ _ _ _ h]45 rfl4647@[simp] theorem sum_matrixUnit_diag (n : ℕ) :48 ∑ i : Fin (2 ^ n), matrixUnit n i i = 1 := by49 change CStarMatrix.ofMatrix (∑ i : Fin (2 ^ n), Matrix.single i i 1) = _50 rw [Matrix.sum_single_one]51 rfl5253/-- 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)5657@[simp] theorem star_limitMatrixUnit (n : ℕ) (i j : Fin (2 ^ n)) :58 star (limitMatrixUnit n i j) = limitMatrixUnit n j i := by59 rw [limitMatrixUnit, ← map_star, star_matrixUnit]60 rfl6162@[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 := by65 by_cases h : j = k66 · subst k67 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]7273@[simp] theorem sum_limitMatrixUnit_diag (n : ℕ) :74 ∑ i : Fin (2 ^ n), limitMatrixUnit n i i = 1 := by75 calc76 ∑ i : Fin (2 ^ n), limitMatrixUnit n i i =77 ofStage n (∑ i : Fin (2 ^ n), matrixUnit n i i) := by78 rw [map_sum]79 rfl80 _ = 1 := by rw [sum_matrixUnit_diag, map_one]8182/-- The finite-row average associated to a full matrix stage. -/83noncomputable def rowAverageLinear (n : ℕ) : Limit →ₗ[ℂ] Limit where84 toFun b := ∑ i : Fin (2 ^ n),85 limitMatrixUnit n i 0 * b * limitMatrixUnit n 0 i86 map_add' b c := by87 simp only [mul_add, add_mul, Finset.sum_add_distrib]88 map_smul' c b := by89 simp only [RingHom.id_apply, Algebra.smul_def]90 rw [Finset.mul_sum]91 apply Finset.sum_congr rfl92 intro i _93 calc94 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 := by100 rw [Algebra.commutes c (limitMatrixUnit n i 0)]101 _ = (algebraMap ℂ Limit) c *102 (limitMatrixUnit n i 0 * b * limitMatrixUnit n 0 i) := by103 simp only [mul_assoc]104105@[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 := rfl108109@[simp] theorem rowAverageLinear_one (n : ℕ) : rowAverageLinear n 1 = 1 := by110 simp [rowAverageLinear]111112theorem rowAverageLinear_nonneg (n : ℕ) (b : Limit) (hb : 0 ≤ b) :113 0 ≤ rowAverageLinear n b := by114 rw [rowAverageLinear_apply]115 apply Finset.sum_nonneg116 intro i _117 simpa only [star_limitMatrixUnit] using118 (star_right_conjugate_nonneg hb (limitMatrixUnit n i 0))119120noncomputable def rowAveragePositive (n : ℕ) : Limit →ₚ[ℂ] Limit :=121 PositiveLinearMap.mk₀ (rowAverageLinear n) (rowAverageLinear_nonneg n)122123theorem norm_rowAverageLinear_le (n : ℕ) (b : Limit) :124 ‖rowAverageLinear n b‖ ≤ 4 * ‖b‖ := by125 exact MathlibAnnex.CStarAlgebra.norm_apply_le_four (rowAveragePositive n)126 (rowAverageLinear_one n) b127128/-- 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)131132@[simp] theorem rowAverage_apply (n : ℕ) (b : Limit) :133 rowAverage n b = rowAverageLinear n b := rfl134135/-- Commuting with `a` after applying the finite-row average. -/136noncomputable def commutatorAverageLinear (n : ℕ) (a : Limit) : Limit →ₗ[ℂ] Limit where137 toFun b := a * rowAverageLinear n b - rowAverageLinear n b * a138 map_add' b c := by simp only [map_add, mul_add, add_mul, sub_add_sub_comm]139 map_smul' c b := by140 rw [map_smul]141 simp only [RingHom.id_apply, Algebra.smul_def]142 rw [mul_sub]143 congr 1144 · calc145 a * ((algebraMap ℂ Limit) c * rowAverageLinear n b) =146 (a * (algebraMap ℂ Limit) c) * rowAverageLinear n b := by147 rw [mul_assoc]148 _ = ((algebraMap ℂ Limit) c * a) * rowAverageLinear n b := by149 rw [Algebra.commutes c a]150 _ = (algebraMap ℂ Limit) c * (a * rowAverageLinear n b) := by151 rw [mul_assoc]152 · rw [mul_assoc]153154theorem norm_commutatorAverageLinear_le (n : ℕ) (a b : Limit) :155 ‖commutatorAverageLinear n a b‖ ≤ (8 * ‖a‖) * ‖b‖ := by156 change ‖a * rowAverageLinear n b - rowAverageLinear n b * a‖ ≤ _157 calc158 ‖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 ring163 _ ≤ 2 * ‖a‖ * (4 * ‖b‖) := by164 gcongr165 exact norm_rowAverageLinear_le n b166 _ = (8 * ‖a‖) * ‖b‖ := by ring167168/-- 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)172173@[simp] theorem commutatorAverage_apply (n : ℕ) (a b : Limit) :174 commutatorAverage n a b =175 a * rowAverageLinear n b - rowAverageLinear n b * a := rfl176177theorem 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 := by180 calc181 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) := by184 rw [rowAverageLinear_apply, Finset.mul_sum]185 _ = limitMatrixUnit n k 0 * b * limitMatrixUnit n 0 l := by186 rw [Finset.sum_eq_single l]187 · simp [← mul_assoc]188 · intro i _ hil189 have hli : l ≠ i := Ne.symm hil190 simp [← mul_assoc, hli]191 · simp192 _ = ∑ i : Fin (2 ^ n),193 (limitMatrixUnit n i 0 * b * limitMatrixUnit n 0 i) *194 limitMatrixUnit n k l := by195 rw [Finset.sum_eq_single k]196 · simp [mul_assoc]197 · intro i _ hik198 simp [mul_assoc, hik]199 · simp200 _ = rowAverageLinear n b * limitMatrixUnit n k l := by201 rw [rowAverageLinear_apply, Finset.sum_mul]202203set_option backward.isDefEq.respectTransparency false in204theorem 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 := by206 apply (CStarMatrix.ofMatrixₗ (R := ℂ)).symm.injective207 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 1211 rw [Matrix.matrix_eq_sum_single (CStarMatrix.ofMatrix.symm c)]212 apply Finset.sum_congr rfl213 intro i _214 apply Finset.sum_congr rfl215 intro j _216 ext k l217 simp [Matrix.single]218219theorem 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 := by222 conv_lhs => rw [stage_eq_sum_smul_matrixUnit n c]223 simp only [map_sum, map_smul, limitMatrixUnit]224225theorem ofStage_commute_rowAverage (n : ℕ) (c : Stage n) (b : Limit) :226 ofStage n c * rowAverageLinear n b = rowAverageLinear n b * ofStage n c := by227 rw [ofStage_eq_sum_smul_limitMatrixUnit]228 apply (Commute.sum_left Finset.univ _ _ fun i _ =>229 Commute.sum_left Finset.univ _ _ fun j _ => ?_).eq230 exact (show Commute (limitMatrixUnit n i j) (rowAverageLinear n b) from231 limitMatrixUnit_commute_rowAverage n i j b).smul_left (c i j)232233theorem exists_stage_approx (a : Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :234 ∃ n, ∃ c : Stage n, ‖a - ofStage n c‖ < epsilon := by235 obtain ⟨y, hy, hya⟩ := dense_stageRange.exists_dist_lt a hepsilon236 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⟩239240theorem exists_common_stage_approx (F : Finset Limit) {epsilon : ℝ}241 (hepsilon : 0 < epsilon) :242 ∃ n, ∀ a ∈ F, ∃ c : Stage n, ‖a - ofStage n c‖ < epsilon := by243 classical244 induction F using Finset.induction with245 | empty =>246 exact ⟨0, by simp⟩247 | @insert a F ha ih =>248 obtain ⟨n, c, hc⟩ := exists_stage_approx a hepsilon249 obtain ⟨m, hm⟩ := ih250 refine ⟨max n m, ?_⟩251 intro x hx252 rcases Finset.mem_insert.mp hx with rfl | hx253 · refine ⟨embed n (max n m) (le_max_left n m) c, ?_⟩254 simpa only [ofStage_embed] using hc255 · obtain ⟨d, hd⟩ := hm x hx256 refine ⟨embed m (max n m) (le_max_right n m) d, ?_⟩257 simpa only [ofStage_embed] using hd258259theorem 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‖ := by262 let p := rowAverageLinear n b263 let d := a - ofStage n c264 have hcomm : ofStage n c * p = p * ofStage n c :=265 ofStage_commute_rowAverage n c b266 have hid : a * p - p * a = d * p - p * d := by267 dsimp only [d]268 noncomm_ring [hcomm]269 rw [hid]270 calc271 ‖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 ring275 _ ≤ 2 * ‖d‖ * (4 * ‖b‖) := by276 gcongr277 exact norm_rowAverageLinear_le n b278 _ = 8 * ‖a - ofStage n c‖ * ‖b‖ := by279 dsimp only [d]280 ring281282theorem norm_commutatorAverage_le_of_stage (n : ℕ) (a : Limit) (c : Stage n) :283 ‖commutatorAverage n a‖ ≤ 8 * ‖a - ofStage n c‖ := by284 apply ContinuousLinearMap.opNorm_le_bound _ (by positivity)285 intro b286 simpa only [commutatorAverage_apply, mul_assoc] using287 norm_commutator_rowAverage_le n a b c288289@[simp] theorem row_isometry_sum (n : ℕ) :290 ∑ i : Fin (2 ^ n), limitMatrixUnit n i 0 * star (limitMatrixUnit n i 0) = 1 := by291 simpa using sum_limitMatrixUnit_diag n292293/-- Exact normalization survives every unital star representation. -/294theorem map_row_isometry_sum295 {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 := by299 calc300 ∑ i : Fin (2 ^ n),301 rho (limitMatrixUnit n i 0) * star (rho (limitMatrixUnit n i 0)) =302 ∑ i : Fin (2 ^ n), rho303 (limitMatrixUnit n i 0 * star (limitMatrixUnit n i 0)) := by304 apply Finset.sum_congr rfl305 intro i _306 rw [map_mul, map_star]307 _ = rho (∑ i : Fin (2 ^ n),308 limitMatrixUnit n i 0 * star (limitMatrixUnit n i 0)) := by309 rw [map_sum]310 _ = 1 := by rw [row_isometry_sum, map_one]311312/-- Consequently the Property 1.3 compression equation is exact for every313operator `E`; no faithfulness or finite-rank assumption is needed here. -/314theorem map_row_isometry_sum_mul315 {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 := by319 rw [map_row_isometry_sum rho n, one_mul]320321/-- In a Hilbert-space representation, the pulled-back row vectors have322exact total squared norm. This is the normalization used by the subsequent323Gram comparison; no orthogonality of the row vectors is asserted. -/324theorem sum_norm_sq_map_limitMatrixUnit_star325 {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 := by329 exact MathlibAnnex.Analysis.CStarAlgebra.Representation.sum_norm_sq_map_star_eq330 rho ξ (fun i => limitMatrixUnit n i 0) (row_isometry_sum n)331332/-- 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‖ := by341 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 b344 obtain ⟨c, hc⟩ := hn a ha345 calc346 ‖a * rowAverageLinear n b - rowAverageLinear n b * a‖ ≤347 8 * ‖a - ofStage n c‖ * ‖b‖ := norm_commutator_rowAverage_le n a b c348 _ ≤ epsilon * ‖b‖ := by349 gcongr350 exact (lt_div_iff₀' (by norm_num : (0 : ℝ) < 8)).mp hc |>.le351352/-- The actual completed CAR algebra supplies the source-independent353finite-row averaging property. -/354theorem hasFiniteRowAveraging_limit :355 MathlibAnnex.CStarAlgebra.HasFiniteRowAveraging Limit := by356 intro F epsilon hepsilon357 obtain ⟨n, hrow, hcomm⟩ := exists_row_approx_central F hepsilon358 refine ⟨2 ^ n, (fun i => limitMatrixUnit n i 0), hrow, ?_⟩359 intro a ha b360 simpa only [MathlibAnnex.CStarAlgebra.finiteRowAverage,361 star_limitMatrixUnit, rowAverageLinear_apply] using hcomm a ha b362363/-- Operator-norm form of the CAR finite-row property. This is the exact364`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 := by371 obtain ⟨n, hn⟩ := exists_common_stage_approx F (show 0 < epsilon / 8 by positivity)372 refine ⟨n, row_isometry_sum n, ?_⟩373 intro a ha374 obtain ⟨c, hc⟩ := hn a ha375 calc376 ‖commutatorAverage n a‖ ≤ 8 * ‖a - ofStage n c‖ :=377 norm_commutatorAverage_le_of_stage n a c378 _ < epsilon := (lt_div_iff₀' (by norm_num : (0 : ℝ) < 8)).mp hc379380end MathlibAnnex.CStarAlgebra.CAR