Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/DifferenceShell.lean, lines 77–93.
Back to A fixed representative family of CAR shell data
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CompletedSource 2import MathlibAnnex.Algebra.Shell 3 4/-! 5# Difference shells in the completed CAR source 6 7The decreasing root flag is converted to the orthogonal shell sequence used 8by the analytic sum. Matching is applied directly to these differences: no 9difference of links for the nested flag projections is used. 10-/ 11 12set_option autoImplicit false 13 14open Filter Topology 15open scoped BigOperators ComplexOrder 16 17namespace MathlibAnnex.CStarAlgebra.CAR 18 19/-- The `n`-th orthogonal shell of the completed root flag. -/ 20noncomputable def rootShell (n : ℕ) : Limit := 21 rootFlag n - rootFlag (n + 1) 22 23@[simp] 24theorem rootShell_eq_shell (n : ℕ) : 25 rootShell n = MathlibAnnex.Algebra.shell rootFlag n := 26 rfl 27 28/-- Successive differences of the completed root flag are genuine star projections. -/ 29theorem isStarProjection_rootShell (n : ℕ) : IsStarProjection (rootShell n) := by 30 have hmul : rootFlag n * rootFlag (n + 1) = rootFlag (n + 1) := 31 ((isStarProjection_rootFlag (n + 1)).le_iff_mul_eq_right 32 (isStarProjection_rootFlag n)).1 (rootFlag_succ_le n) 33 exact (isStarProjection_rootFlag (n + 1)).sub_of_mul_eq_right 34 (isStarProjection_rootFlag n) hmul 35 36@[simp] 37theorem star_rootShell_mul_rootShell (n : ℕ) : 38 star (rootShell n) * rootShell n = rootShell n := by 39 rw [(isStarProjection_rootShell n).isSelfAdjoint.star_eq, 40 (isStarProjection_rootShell n).isIdempotentElem.eq] 41 42@[simp] 43theorem rootShell_mul_star_rootShell (n : ℕ) : 44 rootShell n * star (rootShell n) = rootShell n := by 45 rw [(isStarProjection_rootShell n).isSelfAdjoint.star_eq, 46 (isStarProjection_rootShell n).isIdempotentElem.eq] 47 48/-- The first `N` genuine shells telescope to the complement of the `N`-th flag. -/ 49theorem sum_rootShell_range (N : ℕ) : 50 ∑ n ∈ Finset.range N, rootShell n = 1 - rootFlag N := by 51 calc 52 ∑ n ∈ Finset.range N, rootShell n = 53 ∑ n ∈ Finset.range N, MathlibAnnex.Algebra.shell rootFlag n := by 54 simp only [rootShell_eq_shell] 55 _ = rootFlag 0 - rootFlag N := 56 MathlibAnnex.Algebra.sum_shell_range rootFlag N 57 _ = 1 - rootFlag N := by rw [rootFlag_zero] 58 59/-- For each selected pure-state class, KOS chooses one automorphism and that 60same automorphism matches every genuine difference shell. -/ 61theorem exists_representative_rootShell_family_of_kishimotoOzawaSakai 62 (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) 63 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 64 ∃ alpha : Limit ≃⋆ₐ[ℂ] Limit, 65 (∀ a : Limit, 66 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1 (alpha a) = 67 completedRootPureState.1 a) ∧ 68 ∃ w : ℕ → Limit, ∀ n, 69 star (w n) * w n = alpha (rootShell n) ∧ 70 w n * star (w n) = rootShell n := by 71 exact MathlibAnnex.CStarAlgebra.exists_shell_family_of_kishimotoOzawaSakai hKOS Limit isSimpleCStarAlgebra_limit 72 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1 73 completedRootPureState.1 74 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).2 75 completedRootPureState.2 rootShell isStarProjection_rootShell 76 77/-- At the distinguished class the canonical choices are the identity 78automorphism and the shells themselves. -/ 79theorem rootShell_identity_family : 80 (∀ a : Limit, 81 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState 82 completedRootPureState.classOf).1 83 ((StarAlgEquiv.refl ℂ Limit) a) = completedRootPureState.1 a) ∧ 84 ∀ n, 85 star (rootShell n) * rootShell n = 86 (StarAlgEquiv.refl ℂ Limit) (rootShell n) ∧ 87 rootShell n * star (rootShell n) = rootShell n := by 88 constructor 89 · intro a 90 simp 91 · intro n 92 exact ⟨star_rootShell_mul_rootShell n, 93 rootShell_mul_star_rootShell n⟩ 94 95/-- Root compression transported by a star-algebra equivalence. The inverse 96is applied to the tested element; norm preservation is obtained from the 97standard C-star equivalence API rather than added as source data. -/ 98theorem tendsto_norm_transported_compressionError 99 (alpha : Limit ≃⋆ₐ[ℂ] Limit) (phi : Limit →L[ℂ] ℂ) 100 (hstate : ∀ a : Limit, phi (alpha a) = rootState a) 101 (b : Limit) : 102 Tendsto 103 (fun n ↦ ‖alpha (rootFlag n) * b * alpha (rootFlag n) - 104 phi b • alpha (rootFlag n)‖) 105 atTop (nhds 0) := by 106 have hstate' : rootState (alpha.symm b) = phi b := by 107 simpa using (hstate (alpha.symm b)).symm 108 have hnorm (n : ℕ) : 109 ‖alpha (rootFlag n) * b * alpha (rootFlag n) - 110 phi b • alpha (rootFlag n)‖ = 111 ‖compressionError n (alpha.symm b)‖ := by 112 rw [← StarAlgEquiv.norm_map alpha (compressionError n (alpha.symm b))] 113 simp [compressionError, hstate'] 114 exact (tendsto_norm_compressionError (alpha.symm b)).congr' 115 (Filter.Eventually.of_forall fun n ↦ (hnorm n).symm) 116 117/-- Vector-valued form of transported compression, used by represented 118matrix-coefficient arguments. -/ 119theorem tendsto_transported_compressionError 120 (alpha : Limit ≃⋆ₐ[ℂ] Limit) (phi : Limit →L[ℂ] ℂ) 121 (hstate : ∀ a : Limit, phi (alpha a) = rootState a) 122 (b : Limit) : 123 Tendsto 124 (fun n ↦ alpha (rootFlag n) * b * alpha (rootFlag n) - 125 phi b • alpha (rootFlag n)) 126 atTop (nhds 0) := by 127 rw [tendsto_zero_iff_norm_tendsto_zero] 128 exact tendsto_norm_transported_compressionError alpha phi hstate b 129 130end MathlibAnnex.CStarAlgebra.CAR