Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/FiniteTrace.lean, lines 17–25.
Back to The normalized trace on a finite CAR stage
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.RootCorner 2import Mathlib.LinearAlgebra.Matrix.Trace 3 4/-! 5# Normalized traces of the binary matrix stages 6 7Every estimate is proved at a finite stage. The compatibility proof uses the 8actual embedding `step`, including its coordinate reindexing. 9-/ 10 11set_option autoImplicit false 12 13open scoped ComplexOrder 14 15namespace MathlibAnnex.CStarAlgebra.CAR 16 17/-- The average of the diagonal entries of a binary matrix stage. -/ 18noncomputable def stageTraceLinear (n : ℕ) : Stage n →ₗ[ℂ] ℂ where 19 toFun a := (2 ^ n : ℂ)⁻¹ * ∑ i, a i i 20 map_add' a b := by simp only [CStarMatrix.add_apply, Finset.sum_add_distrib, mul_add] 21 map_smul' c a := by 22 change (2 ^ n : ℂ)⁻¹ * (∑ i, c * a i i) = 23 c * ((2 ^ n : ℂ)⁻¹ * ∑ i, a i i) 24 rw [← Finset.mul_sum] 25 ring 26 27@[simp] 28theorem stageTraceLinear_apply (n : ℕ) (a : Stage n) : 29 stageTraceLinear n a = (2 ^ n : ℂ)⁻¹ * ∑ i, a i i := rfl 30 31/-- The normalized matrix trace is contractive in the C⋆-norm. -/ 32theorem norm_stageTraceLinear_le (n : ℕ) (a : Stage n) : 33 ‖stageTraceLinear n a‖ ≤ ‖a‖ := by 34 have hpos : (0 : ℝ) < 2 ^ n := pow_pos (by norm_num) n 35 calc 36 ‖stageTraceLinear n a‖ = (2 ^ n : ℝ)⁻¹ * ‖∑ i, a i i‖ := by 37 simp only [stageTraceLinear_apply, norm_mul, norm_inv, norm_pow, Complex.norm_two] 38 _ ≤ (2 ^ n : ℝ)⁻¹ * ∑ i, ‖a i i‖ := 39 mul_le_mul_of_nonneg_left (norm_sum_le _ _) (inv_nonneg.mpr hpos.le) 40 _ ≤ (2 ^ n : ℝ)⁻¹ * ∑ _i : Fin (2 ^ n), ‖a‖ := by 41 gcongr with i 42 exact CStarMatrix.norm_entry_le_norm 43 _ = ‖a‖ := by 44 simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, 45 nsmul_eq_mul, Nat.cast_pow, Nat.cast_ofNat] 46 rw [← mul_assoc, inv_mul_cancel₀ hpos.ne', one_mul] 47 48/-- The finite-stage trace, bundled as a continuous linear map. -/ 49noncomputable def stageTrace (n : ℕ) : Stage n →L[ℂ] ℂ := 50 (stageTraceLinear n).mkContinuous 1 fun a ↦ by 51 simpa only [one_mul] using norm_stageTraceLinear_le n a 52 53@[simp] 54theorem stageTrace_apply (n : ℕ) (a : Stage n) : 55 stageTrace n a = (2 ^ n : ℂ)⁻¹ * ∑ i, a i i := rfl 56 57theorem norm_stageTrace_le (n : ℕ) (a : Stage n) : 58 ‖stageTrace n a‖ ≤ ‖a‖ := norm_stageTraceLinear_le n a 59 60@[simp] 61theorem stageTrace_one (n : ℕ) : stageTrace n 1 = 1 := by 62 rw [stageTrace_apply] 63 simp only [CStarMatrix.one_apply_eq, Finset.sum_const, Finset.card_univ, 64 Fintype.card_fin, nsmul_eq_mul, mul_one, Nat.cast_pow, Nat.cast_ofNat] 65 exact inv_mul_cancel₀ (pow_ne_zero n (by norm_num)) 66 67/-- Positivity is checked entrywise on a star square. -/ 68theorem stageTrace_star_mul_self_nonneg (n : ℕ) (a : Stage n) : 69 0 ≤ stageTrace n (star a * a) := by 70 rw [stageTrace_apply] 71 have hcoef : (0 : ℂ) ≤ (2 ^ n : ℂ)⁻¹ := by 72 have hr : (0 : ℝ) ≤ (2 ^ n : ℝ)⁻¹ := inv_nonneg.mpr (by positivity) 73 simpa only [Complex.ofReal_inv, Complex.ofReal_pow, Complex.ofReal_ofNat] using 74 (Complex.zero_le_real.mpr hr) 75 apply mul_nonneg hcoef 76 apply Finset.sum_nonneg 77 intro i _ 78 rw [CStarMatrix.mul_apply] 79 simp only [CStarMatrix.star_apply] 80 exact Finset.sum_nonneg fun k _ ↦ star_mul_self_nonneg (a k i) 81 82/-- Traciality follows from interchanging the two finite sums. -/ 83theorem stageTrace_mul_comm (n : ℕ) (a b : Stage n) : 84 stageTrace n (a * b) = stageTrace n (b * a) := by 85 simp only [stageTrace_apply, CStarMatrix.mul_apply] 86 congr 1 87 rw [Finset.sum_comm] 88 apply Finset.sum_congr rfl 89 intro i _ 90 apply Finset.sum_congr rfl 91 intro j _ 92 exact mul_comm _ _ 93 94private theorem step_diagonal (n : ℕ) (a : Stage n) 95 (i : Fin (2 ^ n)) (b : Fin 2) : 96 step n a (stepIndexEquiv n (i, b)) (stepIndexEquiv n (i, b)) = a i i := by 97 simp [step, amplify, CStarMatrix.reindexₐ_apply, Matrix.reindex_apply, 98 Matrix.kronecker_apply] 99 100private theorem sum_step_diagonal (n : ℕ) (a : Stage n) : 101 (∑ k : Fin (2 ^ (n + 1)), step n a k k) = 2 * ∑ i, a i i := by 102 calc 103 (∑ k : Fin (2 ^ (n + 1)), step n a k k) = 104 ∑ z : Fin (2 ^ n) × Fin 2, 105 step n a (stepIndexEquiv n z) (stepIndexEquiv n z) := 106 ((stepIndexEquiv n).sum_comp (fun k ↦ step n a k k)).symm 107 _ = ∑ i : Fin (2 ^ n), ∑ b : Fin 2, a i i := by 108 rw [Fintype.sum_prod_type] 109 simp only [step_diagonal] 110 _ = 2 * ∑ i, a i i := by simp [Fin.sum_univ_two, Finset.sum_add_distrib, two_mul] 111 112@[simp] 113theorem stageTrace_step (n : ℕ) (a : Stage n) : 114 stageTrace (n + 1) (step n a) = stageTrace n a := by 115 rw [stageTrace_apply, sum_step_diagonal, stageTrace_apply, pow_succ] 116 field_simp <;> ring 117 118@[simp] 119theorem stageTrace_rootProjection (n : ℕ) : 120 stageTrace n (rootProjection n) = (2 ^ n : ℂ)⁻¹ := by 121 simp [stageTrace_apply, rootProjection, Matrix.single] 122 123end MathlibAnnex.CStarAlgebra.CAR