Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/DifferenceShell.lean
Pinned GitHub source · Raw UTF-8 source
Back to A fixed representative family of CAR shell data
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CompletedSource2import MathlibAnnex.Algebra.Shell34/-!5# Difference shells in the completed CAR source67The decreasing root flag is converted to the orthogonal shell sequence used8by the analytic sum. Matching is applied directly to these differences: no9difference of links for the nested flag projections is used.10-/1112set_option autoImplicit false1314open Filter Topology15open scoped BigOperators ComplexOrder1617namespace MathlibAnnex.CStarAlgebra.CAR1819/-- The `n`-th orthogonal shell of the completed root flag. -/20noncomputable def rootShell (n : ℕ) : Limit :=21 rootFlag n - rootFlag (n + 1)2223@[simp]24theorem rootShell_eq_shell (n : ℕ) :25 rootShell n = MathlibAnnex.Algebra.shell rootFlag n :=26 rfl2728/-- Successive differences of the completed root flag are genuine star projections. -/29theorem isStarProjection_rootShell (n : ℕ) : IsStarProjection (rootShell n) := by30 have hmul : rootFlag n * rootFlag (n + 1) = rootFlag (n + 1) :=31 ((isStarProjection_rootFlag (n + 1)).le_iff_mul_eq_right32 (isStarProjection_rootFlag n)).1 (rootFlag_succ_le n)33 exact (isStarProjection_rootFlag (n + 1)).sub_of_mul_eq_right34 (isStarProjection_rootFlag n) hmul3536@[simp]37theorem star_rootShell_mul_rootShell (n : ℕ) :38 star (rootShell n) * rootShell n = rootShell n := by39 rw [(isStarProjection_rootShell n).isSelfAdjoint.star_eq,40 (isStarProjection_rootShell n).isIdempotentElem.eq]4142@[simp]43theorem rootShell_mul_star_rootShell (n : ℕ) :44 rootShell n * star (rootShell n) = rootShell n := by45 rw [(isStarProjection_rootShell n).isSelfAdjoint.star_eq,46 (isStarProjection_rootShell n).isIdempotentElem.eq]4748/-- 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 := by51 calc52 ∑ n ∈ Finset.range N, rootShell n =53 ∑ n ∈ Finset.range N, MathlibAnnex.Algebra.shell rootFlag n := by54 simp only [rootShell_eq_shell]55 _ = rootFlag 0 - rootFlag N :=56 MathlibAnnex.Algebra.sum_shell_range rootFlag N57 _ = 1 - rootFlag N := by rw [rootFlag_zero]5859/-- For each selected pure-state class, KOS chooses one automorphism and that60same automorphism matches every genuine difference shell. -/61theorem exists_representative_rootShell_family_of_kishimotoOzawaSakai62 (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 := by71 exact MathlibAnnex.CStarAlgebra.exists_shell_family_of_kishimotoOzawaSakai hKOS Limit isSimpleCStarAlgebra_limit72 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).173 completedRootPureState.174 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).275 completedRootPureState.2 rootShell isStarProjection_rootShell7677/-- At the distinguished class the canonical choices are the identity78automorphism and the shells themselves. -/79theorem rootShell_identity_family :80 (∀ a : Limit,81 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState82 completedRootPureState.classOf).183 ((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 := by88 constructor89 · intro a90 simp91 · intro n92 exact ⟨star_rootShell_mul_rootShell n,93 rootShell_mul_star_rootShell n⟩9495/-- Root compression transported by a star-algebra equivalence. The inverse96is applied to the tested element; norm preservation is obtained from the97standard C-star equivalence API rather than added as source data. -/98theorem tendsto_norm_transported_compressionError99 (alpha : Limit ≃⋆ₐ[ℂ] Limit) (phi : Limit →L[ℂ] ℂ)100 (hstate : ∀ a : Limit, phi (alpha a) = rootState a)101 (b : Limit) :102 Tendsto103 (fun n ↦ ‖alpha (rootFlag n) * b * alpha (rootFlag n) -104 phi b • alpha (rootFlag n)‖)105 atTop (nhds 0) := by106 have hstate' : rootState (alpha.symm b) = phi b := by107 simpa using (hstate (alpha.symm b)).symm108 have hnorm (n : ℕ) :109 ‖alpha (rootFlag n) * b * alpha (rootFlag n) -110 phi b • alpha (rootFlag n)‖ =111 ‖compressionError n (alpha.symm b)‖ := by112 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)116117/-- Vector-valued form of transported compression, used by represented118matrix-coefficient arguments. -/119theorem tendsto_transported_compressionError120 (alpha : Limit ≃⋆ₐ[ℂ] Limit) (phi : Limit →L[ℂ] ℂ)121 (hstate : ∀ a : Limit, phi (alpha a) = rootState a)122 (b : Limit) :123 Tendsto124 (fun n ↦ alpha (rootFlag n) * b * alpha (rootFlag n) -125 phi b • alpha (rootFlag n))126 atTop (nhds 0) := by127 rw [tendsto_zero_iff_norm_tendsto_zero]128 exact tendsto_norm_transported_compressionError alpha phi hstate b129130end MathlibAnnex.CStarAlgebra.CAR