Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/RootCorner.lean
Pinned GitHub source · Raw UTF-8 source
Back to Realizing a finite Gram matrix in a represented CAR corner
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteStages2import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances3import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order4import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap56/-!7# The finite-stage root corner89The distinguished coordinate defines the product-vector functional at every binary10matrix stage. Its rank-one corner has an exact compression formula for every stage11element, before any completion or limiting argument is used.12-/1314set_option autoImplicit false1516open scoped CStarAlgebra ComplexOrder Matrix1718namespace MathlibAnnex.CStarAlgebra.CAR1920/-- The rank-one projection onto the distinguished zero coordinate. -/21noncomputable def rootProjection (n : ℕ) : Stage n :=22 CStarMatrix.ofMatrix (Matrix.single 0 0 (1 : ℂ))2324/-- 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 := by27 classical28 apply CStarMatrix.ext29 intro i j30 by_cases hi : i = 0 <;> by_cases hj : j = 031 · subst i32 subst j33 simp [rootProjection, CStarMatrix.mul_apply, Matrix.single]34 · subst i35 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]3940/-- 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 := by44 rw [rootProjection_mul_mul, sub_self, norm_zero]4546theorem isStarProjection_rootProjection (n : ℕ) :47 IsStarProjection (rootProjection n) := by48 constructor49 · rw [isIdempotentElem_iff]50 simpa using rootProjection_mul_mul n (1 : Stage n)51 · rw [isSelfAdjoint_iff]52 apply CStarMatrix.ext53 intro i j54 simp [rootProjection, CStarMatrix.star_apply, Matrix.single, and_comm]5556/-- Evaluation at the distinguished diagonal coordinate. -/57def rootLinear (n : ℕ) : Stage n →ₗ[ℂ] ℂ where58 toFun x := x 0 059 map_add' _ _ := rfl60 map_smul' _ _ := rfl6162/-- The distinguished-coordinate functional is continuous for the operator norm. -/63noncomputable def rootFunctional (n : ℕ) : Stage n →L[ℂ] ℂ :=64 (rootLinear n).mkContinuous 1 fun x => by65 simpa [rootLinear] using (CStarMatrix.norm_entry_le_norm (M := x) (i := (0 : Fin (2 ^ n)))66 (j := (0 : Fin (2 ^ n))))6768@[simp]69theorem rootFunctional_apply (n : ℕ) (x : Stage n) : rootFunctional n x = x 0 0 :=70 rfl7172/-- 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 := by76 change step n x 0 0 = x 0 077 simp [step, stepIndexEquiv, amplify, Matrix.reindex_apply, finProdFinEquiv]78 congr 1 <;> apply Fin.ext <;> simp7980/-- 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) := by84 rw [rootProjection_mul_mul]85 congr 186 exact rootFunctional_step n x8788@[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 := by92 rw [rootProjection_step_mul_mul, sub_self, norm_zero]9394/-- Positivity of the distinguished-coordinate functional. -/95theorem rootLinear_nonneg (n : ℕ) (x : Stage n) (hx : 0 ≤ x) :96 0 ≤ rootLinear n x := by97 letI : NonnegSpectrumClass ℝ (Stage n) :=98 CStarAlgebra.instNonnegSpectrumClass'99 letI : NonUnitalContinuousFunctionalCalculus ℂ (Stage n) IsStarNormal :=100 (IsStarNormal.instNonUnitalContinuousFunctionalCalculus101 (A := Stage n)).toNonUnitalContinuousFunctionalCalculus102 letI : NonUnitalContinuousFunctionalCalculus ℝ (Stage n) IsSelfAdjoint :=103 IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus104 rcases CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx with ⟨y, rfl⟩105 change 0 ≤ (star y * y) 0 0106 rw [CStarMatrix.mul_apply]107 simp only [CStarMatrix.star_apply]108 exact Finset.sum_nonneg fun k _ => star_mul_self_nonneg (y k 0)109110/-- The normalized positive functional at the root coordinate. -/111noncomputable def rootPositiveFunctional (n : ℕ) : Stage n →ₚ[ℂ] ℂ :=112 PositiveLinearMap.mk₀ (rootLinear n) (rootLinear_nonneg n)113114@[simp]115theorem rootPositiveFunctional_apply (n : ℕ) (x : Stage n) :116 rootPositiveFunctional n x = x 0 0 := rfl117118@[simp]119theorem rootPositiveFunctional_one (n : ℕ) : rootPositiveFunctional n 1 = 1 := by120 exact CStarMatrix.one_apply_eq 0121122@[simp]123theorem rootPositiveFunctional_step (n : ℕ) (x : Stage n) :124 rootPositiveFunctional (n + 1) (step n x) = rootPositiveFunctional n x := by125 exact rootFunctional_step n x126127end MathlibAnnex.CStarAlgebra.CAR