Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/ShellMatching.lean, lines 21–41.
Back to Exact projection links for one approximately inner automorphism
1import MathlibAnnex.Analysis.CStarAlgebra.CloseProjections 2import MathlibAnnex.Analysis.CStarAlgebra.ShellMatching 3import MathlibAnnex.Analysis.CStarAlgebra.PureStateHomogeneity.KishimotoOzawaSakai 4 5/-! 6# Conditional exact matching of a source shell 7 8KOS remains an explicit argument. Approximate innerness is invoked on the 9singleton finite set containing the root shell; the near-projection theorem 10then turns that approximation into exact matching. 11-/ 12 13set_option autoImplicit false 14 15namespace MathlibAnnex.CStarAlgebra 16 17open MathlibAnnex.CStarAlgebra 18 19universe u v 20 21/-- Exact shell matching for one projection from point-norm approximate innerness of a 22fixed automorphism. -/ 23theorem exists_shell_of_approximately_inner 24 (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Nontrivial A] 25 (alpha : A ≃⋆ₐ[ℂ] A) 26 (happrox : ∀ (F : Finset A) (epsilon : ℝ), 0 < epsilon → 27 ∃ g : unitary A, ∀ a ∈ F, 28 ‖alpha a - (g : A) * a * star (g : A)‖ < epsilon) 29 (f : A) (hf : IsStarProjection f) : 30 ∃ w : A, star w * w = alpha f ∧ w * star w = f := by 31 classical 32 obtain ⟨g, hg⟩ := happrox {f} 1 zero_lt_one 33 have hclose : ‖alpha f - (g : A) * f * star (g : A)‖ < 1 := 34 hg f (by simp) 35 have he : IsStarProjection (alpha f) := hf.map alpha 36 have hr : IsStarProjection ((g : A) * f * star (g : A)) := 37 hf.unitary_conjugate g 38 obtain ⟨t, ht⟩ := 39 he.exists_unitary_conjugate_of_norm_sub_lt_one hr hclose 40 let w := matchedLink g t (alpha f) 41 exact ⟨w, matchedLink_supports g t (alpha f) f he ht⟩ 42 43/-- A fixed approximately inner automorphism simultaneously determines exact links for 44an arbitrary set-indexed family of projections. -/ 45theorem exists_shell_family_of_approximately_inner 46 (A : Type u) {ι : Type v} 47 [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Nontrivial A] 48 (alpha : A ≃⋆ₐ[ℂ] A) 49 (happrox : ∀ (F : Finset A) (epsilon : ℝ), 0 < epsilon → 50 ∃ g : unitary A, ∀ a ∈ F, 51 ‖alpha a - (g : A) * a * star (g : A)‖ < epsilon) 52 (f : ι → A) (hf : ∀ i, IsStarProjection (f i)) : 53 ∃ w : ι → A, ∀ i, 54 star (w i) * w i = alpha (f i) ∧ w i * star (w i) = f i := by 55 classical 56 have hlinks (i : ι) : ∃ w : A, 57 star w * w = alpha (f i) ∧ w * star w = f i := 58 exists_shell_of_approximately_inner A alpha happrox (f i) (hf i) 59 exact ⟨fun i => Classical.choose (hlinks i), 60 fun i => Classical.choose_spec (hlinks i)⟩ 61 62/-- KOS supplies one automorphism for the state pair; all projection shells are then 63matched using that same automorphism. Only the approximating unitary varies with `n`. -/ 64theorem exists_shell_family_of_kishimotoOzawaSakai (hKOS : KishimotoOzawaSakaiProperty.{u}) 65 (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 66 [TopologicalSpace.SeparableSpace A] 67 (hsimple : IsSimpleCStarAlgebra A) 68 (phi_i phi_o : A →L[ℂ] ℂ) 69 (hpure_i : IsPureState A phi_i) (hpure_o : IsPureState A phi_o) 70 (f : ℕ → A) (hf : ∀ n, IsStarProjection (f n)) : 71 ∃ alpha : A ≃⋆ₐ[ℂ] A, 72 (∀ a : A, phi_i (alpha a) = phi_o a) ∧ 73 ∃ w : ℕ → A, ∀ n, 74 star (w n) * w n = alpha (f n) ∧ w n * star (w n) = f n := by 75 classical 76 letI : Nontrivial A := hsimple.1 77 obtain ⟨alpha, hstate, happrox⟩ := 78 hKOS A hsimple phi_i phi_o hpure_i hpure_o 79 have hlinks : ∀ n, ∃ w : A, 80 star w * w = alpha (f n) ∧ w * star w = f n := by 81 intro n 82 obtain ⟨g, hg⟩ := happrox {f n} 1 zero_lt_one 83 have hclose : ‖alpha (f n) - (g : A) * f n * star (g : A)‖ < 1 := by 84 exact hg (f n) (by simp) 85 have he : IsStarProjection (alpha (f n)) := (hf n).map alpha 86 have hr : IsStarProjection ((g : A) * f n * star (g : A)) := 87 (hf n).unitary_conjugate g 88 obtain ⟨t, ht⟩ := 89 he.exists_unitary_conjugate_of_norm_sub_lt_one hr hclose 90 let w := matchedLink g t (alpha (f n)) 91 exact ⟨w, matchedLink_supports g t (alpha (f n)) (f n) he ht⟩ 92 let w : ℕ → A := fun n => Classical.choose (hlinks n) 93 exact ⟨alpha, hstate, w, fun n => Classical.choose_spec (hlinks n)⟩ 94 95theorem exists_shell_link_of_kishimotoOzawaSakai (hKOS : KishimotoOzawaSakaiProperty.{u}) 96 (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 97 [TopologicalSpace.SeparableSpace A] 98 (hsimple : IsSimpleCStarAlgebra A) 99 (phi_i phi_o : A →L[ℂ] ℂ) 100 (hpure_i : IsPureState A phi_i) (hpure_o : IsPureState A phi_o) 101 (f : A) (hf : IsStarProjection f) : 102 ∃ alpha : A ≃⋆ₐ[ℂ] A, 103 (∀ a : A, phi_i (alpha a) = phi_o a) ∧ 104 ∃ w : A, star w * w = alpha f ∧ w * star w = f := by 105 classical 106 letI : Nontrivial A := hsimple.1 107 obtain ⟨alpha, hstate, happrox⟩ := 108 hKOS A hsimple phi_i phi_o hpure_i hpure_o 109 obtain ⟨g, hg⟩ := happrox {f} 1 zero_lt_one 110 have hclose : ‖alpha f - (g : A) * f * star (g : A)‖ < 1 := by 111 exact hg f (by simp) 112 have he : IsStarProjection (alpha f) := hf.map alpha 113 have hr : IsStarProjection ((g : A) * f * star (g : A)) := 114 hf.unitary_conjugate g 115 obtain ⟨t, ht⟩ := 116 he.exists_unitary_conjugate_of_norm_sub_lt_one hr hclose 117 let w := matchedLink g t (alpha f) 118 have hw := matchedLink_supports g t (alpha f) f he ht 119 exact ⟨alpha, hstate, w, hw⟩ 120 121end MathlibAnnex.CStarAlgebra