Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/FiniteTrace.lean
Pinned GitHub source · Raw UTF-8 source
Back to The normalized trace on a finite CAR stage · Back to Constructing the normalized trace on the completed CAR algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.RootCorner2import Mathlib.LinearAlgebra.Matrix.Trace34/-!5# Normalized traces of the binary matrix stages67Every estimate is proved at a finite stage. The compatibility proof uses the8actual embedding `step`, including its coordinate reindexing.9-/1011set_option autoImplicit false1213open scoped ComplexOrder1415namespace MathlibAnnex.CStarAlgebra.CAR1617/-- The average of the diagonal entries of a binary matrix stage. -/18noncomputable def stageTraceLinear (n : ℕ) : Stage n →ₗ[ℂ] ℂ where19 toFun a := (2 ^ n : ℂ)⁻¹ * ∑ i, a i i20 map_add' a b := by simp only [CStarMatrix.add_apply, Finset.sum_add_distrib, mul_add]21 map_smul' c a := by22 change (2 ^ n : ℂ)⁻¹ * (∑ i, c * a i i) =23 c * ((2 ^ n : ℂ)⁻¹ * ∑ i, a i i)24 rw [← Finset.mul_sum]25 ring2627@[simp]28theorem stageTraceLinear_apply (n : ℕ) (a : Stage n) :29 stageTraceLinear n a = (2 ^ n : ℂ)⁻¹ * ∑ i, a i i := rfl3031/-- The normalized matrix trace is contractive in the C⋆-norm. -/32theorem norm_stageTraceLinear_le (n : ℕ) (a : Stage n) :33 ‖stageTraceLinear n a‖ ≤ ‖a‖ := by34 have hpos : (0 : ℝ) < 2 ^ n := pow_pos (by norm_num) n35 calc36 ‖stageTraceLinear n a‖ = (2 ^ n : ℝ)⁻¹ * ‖∑ i, a i i‖ := by37 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‖ := by41 gcongr with i42 exact CStarMatrix.norm_entry_le_norm43 _ = ‖a‖ := by44 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]4748/-- The finite-stage trace, bundled as a continuous linear map. -/49noncomputable def stageTrace (n : ℕ) : Stage n →L[ℂ] ℂ :=50 (stageTraceLinear n).mkContinuous 1 fun a ↦ by51 simpa only [one_mul] using norm_stageTraceLinear_le n a5253@[simp]54theorem stageTrace_apply (n : ℕ) (a : Stage n) :55 stageTrace n a = (2 ^ n : ℂ)⁻¹ * ∑ i, a i i := rfl5657theorem norm_stageTrace_le (n : ℕ) (a : Stage n) :58 ‖stageTrace n a‖ ≤ ‖a‖ := norm_stageTraceLinear_le n a5960@[simp]61theorem stageTrace_one (n : ℕ) : stageTrace n 1 = 1 := by62 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))6667/-- 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) := by70 rw [stageTrace_apply]71 have hcoef : (0 : ℂ) ≤ (2 ^ n : ℂ)⁻¹ := by72 have hr : (0 : ℝ) ≤ (2 ^ n : ℝ)⁻¹ := inv_nonneg.mpr (by positivity)73 simpa only [Complex.ofReal_inv, Complex.ofReal_pow, Complex.ofReal_ofNat] using74 (Complex.zero_le_real.mpr hr)75 apply mul_nonneg hcoef76 apply Finset.sum_nonneg77 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)8182/-- 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) := by85 simp only [stageTrace_apply, CStarMatrix.mul_apply]86 congr 187 rw [Finset.sum_comm]88 apply Finset.sum_congr rfl89 intro i _90 apply Finset.sum_congr rfl91 intro j _92 exact mul_comm _ _9394private 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 := by97 simp [step, amplify, CStarMatrix.reindexₐ_apply, Matrix.reindex_apply,98 Matrix.kronecker_apply]99100private theorem sum_step_diagonal (n : ℕ) (a : Stage n) :101 (∑ k : Fin (2 ^ (n + 1)), step n a k k) = 2 * ∑ i, a i i := by102 calc103 (∑ 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)).symm107 _ = ∑ i : Fin (2 ^ n), ∑ b : Fin 2, a i i := by108 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]111112@[simp]113theorem stageTrace_step (n : ℕ) (a : Stage n) :114 stageTrace (n + 1) (step n a) = stageTrace n a := by115 rw [stageTrace_apply, sum_step_diagonal, stageTrace_apply, pow_succ]116 field_simp <;> ring117118@[simp]119theorem stageTrace_rootProjection (n : ℕ) :120 stageTrace n (rootProjection n) = (2 ^ n : ℂ)⁻¹ := by121 simp [stageTrace_apply, rootProjection, Matrix.single]122123end MathlibAnnex.CStarAlgebra.CAR