Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/RootCorner.lean, lines 24–38.
Back to The decreasing root projections in the CAR completion
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteStages 2import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances 3import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 4import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap 5 6/-! 7# The finite-stage root corner 8 9The distinguished coordinate defines the product-vector functional at every binary 10matrix stage. Its rank-one corner has an exact compression formula for every stage 11element, before any completion or limiting argument is used. 12-/ 13 14set_option autoImplicit false 15 16open scoped CStarAlgebra ComplexOrder Matrix 17 18namespace MathlibAnnex.CStarAlgebra.CAR 19 20/-- The rank-one projection onto the distinguished zero coordinate. -/ 21noncomputable def rootProjection (n : ℕ) : Stage n := 22 CStarMatrix.ofMatrix (Matrix.single 0 0 (1 : ℂ)) 23 24/-- Exact finite-stage compression by the distinguished rank-one projection. -/ 25theorem rootProjection_mul_mul (n : ℕ) (x : Stage n) : 26 rootProjection n * x * rootProjection n = (x 0 0) • rootProjection n := by 27 classical 28 apply CStarMatrix.ext 29 intro i j 30 by_cases hi : i = 0 <;> by_cases hj : j = 0 31 · subst i 32 subst j 33 simp [rootProjection, CStarMatrix.mul_apply, Matrix.single] 34 · subst i 35 simp [rootProjection, CStarMatrix.mul_apply, Matrix.single, Ne.symm hj] 36 · simp [rootProjection, CStarMatrix.mul_apply, Matrix.single, Ne.symm hi] 37 · simp [rootProjection, CStarMatrix.mul_apply, Matrix.single, Ne.symm hi, 38 Ne.symm hj] 39 40/-- The finite-stage compression error vanishes for every stage element. -/ 41@[simp] 42theorem norm_rootProjection_compression_sub (n : ℕ) (x : Stage n) : 43 ‖rootProjection n * x * rootProjection n - (x 0 0) • rootProjection n‖ = 0 := by 44 rw [rootProjection_mul_mul, sub_self, norm_zero] 45 46theorem isStarProjection_rootProjection (n : ℕ) : 47 IsStarProjection (rootProjection n) := by 48 constructor 49 · rw [isIdempotentElem_iff] 50 simpa using rootProjection_mul_mul n (1 : Stage n) 51 · rw [isSelfAdjoint_iff] 52 apply CStarMatrix.ext 53 intro i j 54 simp [rootProjection, CStarMatrix.star_apply, Matrix.single, and_comm] 55 56/-- Evaluation at the distinguished diagonal coordinate. -/ 57def rootLinear (n : ℕ) : Stage n →ₗ[ℂ] ℂ where 58 toFun x := x 0 0 59 map_add' _ _ := rfl 60 map_smul' _ _ := rfl 61 62/-- The distinguished-coordinate functional is continuous for the operator norm. -/ 63noncomputable def rootFunctional (n : ℕ) : Stage n →L[ℂ] ℂ := 64 (rootLinear n).mkContinuous 1 fun x => by 65 simpa [rootLinear] using (CStarMatrix.norm_entry_le_norm (M := x) (i := (0 : Fin (2 ^ n))) 66 (j := (0 : Fin (2 ^ n)))) 67 68@[simp] 69theorem rootFunctional_apply (n : ℕ) (x : Stage n) : rootFunctional n x = x 0 0 := 70 rfl 71 72/-- The root vector functionals are compatible with the standard CAR stage embeddings. -/ 73@[simp] 74theorem rootFunctional_step (n : ℕ) (x : Stage n) : 75 rootFunctional (n + 1) (step n x) = rootFunctional n x := by 76 change step n x 0 0 = x 0 0 77 simp [step, stepIndexEquiv, amplify, Matrix.reindex_apply, finProdFinEquiv] 78 congr 1 <;> apply Fin.ext <;> simp 79 80/-- One-step local compression is exact after embedding an arbitrary old-stage element. -/ 81theorem rootProjection_step_mul_mul (n : ℕ) (x : Stage n) : 82 rootProjection (n + 1) * step n x * rootProjection (n + 1) = 83 (x 0 0) • rootProjection (n + 1) := by 84 rw [rootProjection_mul_mul] 85 congr 1 86 exact rootFunctional_step n x 87 88@[simp] 89theorem norm_rootProjection_step_compression_sub (n : ℕ) (x : Stage n) : 90 ‖rootProjection (n + 1) * step n x * rootProjection (n + 1) - 91 (x 0 0) • rootProjection (n + 1)‖ = 0 := by 92 rw [rootProjection_step_mul_mul, sub_self, norm_zero] 93 94/-- Positivity of the distinguished-coordinate functional. -/ 95theorem rootLinear_nonneg (n : ℕ) (x : Stage n) (hx : 0 ≤ x) : 96 0 ≤ rootLinear n x := by 97 letI : NonnegSpectrumClass ℝ (Stage n) := 98 CStarAlgebra.instNonnegSpectrumClass' 99 letI : NonUnitalContinuousFunctionalCalculus ℂ (Stage n) IsStarNormal := 100 (IsStarNormal.instNonUnitalContinuousFunctionalCalculus 101 (A := Stage n)).toNonUnitalContinuousFunctionalCalculus 102 letI : NonUnitalContinuousFunctionalCalculus ℝ (Stage n) IsSelfAdjoint := 103 IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus 104 rcases CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx with ⟨y, rfl⟩ 105 change 0 ≤ (star y * y) 0 0 106 rw [CStarMatrix.mul_apply] 107 simp only [CStarMatrix.star_apply] 108 exact Finset.sum_nonneg fun k _ => star_mul_self_nonneg (y k 0) 109 110/-- The normalized positive functional at the root coordinate. -/ 111noncomputable def rootPositiveFunctional (n : ℕ) : Stage n →ₚ[ℂ] ℂ := 112 PositiveLinearMap.mk₀ (rootLinear n) (rootLinear_nonneg n) 113 114@[simp] 115theorem rootPositiveFunctional_apply (n : ℕ) (x : Stage n) : 116 rootPositiveFunctional n x = x 0 0 := rfl 117 118@[simp] 119theorem rootPositiveFunctional_one (n : ℕ) : rootPositiveFunctional n 1 = 1 := by 120 exact CStarMatrix.one_apply_eq 0 121 122@[simp] 123theorem rootPositiveFunctional_step (n : ℕ) (x : Stage n) : 124 rootPositiveFunctional (n + 1) (step n x) = rootPositiveFunctional n x := by 125 exact rootFunctional_step n x 126 127end MathlibAnnex.CStarAlgebra.CAR