Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/ShellMatching.lean
Pinned GitHub source · Raw UTF-8 source
Back to Choosing the CAR shell family from proved homogeneity · Back to Exact projection links for one approximately inner automorphism
1import MathlibAnnex.Analysis.CStarAlgebra.CloseProjections2import MathlibAnnex.Analysis.CStarAlgebra.ShellMatching3import MathlibAnnex.Analysis.CStarAlgebra.PureStateHomogeneity.KishimotoOzawaSakai45/-!6# Conditional exact matching of a source shell78KOS remains an explicit argument. Approximate innerness is invoked on the9singleton finite set containing the root shell; the near-projection theorem10then turns that approximation into exact matching.11-/1213set_option autoImplicit false1415namespace MathlibAnnex.CStarAlgebra1617open MathlibAnnex.CStarAlgebra1819universe u v2021/-- Exact shell matching for one projection from point-norm approximate innerness of a22fixed automorphism. -/23theorem exists_shell_of_approximately_inner24 (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 := by31 classical32 obtain ⟨g, hg⟩ := happrox {f} 1 zero_lt_one33 have hclose : ‖alpha f - (g : A) * f * star (g : A)‖ < 1 :=34 hg f (by simp)35 have he : IsStarProjection (alpha f) := hf.map alpha36 have hr : IsStarProjection ((g : A) * f * star (g : A)) :=37 hf.unitary_conjugate g38 obtain ⟨t, ht⟩ :=39 he.exists_unitary_conjugate_of_norm_sub_lt_one hr hclose40 let w := matchedLink g t (alpha f)41 exact ⟨w, matchedLink_supports g t (alpha f) f he ht⟩4243/-- A fixed approximately inner automorphism simultaneously determines exact links for44an arbitrary set-indexed family of projections. -/45theorem exists_shell_family_of_approximately_inner46 (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 := by55 classical56 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)⟩6162/-- KOS supplies one automorphism for the state pair; all projection shells are then63matched 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 := by75 classical76 letI : Nontrivial A := hsimple.177 obtain ⟨alpha, hstate, happrox⟩ :=78 hKOS A hsimple phi_i phi_o hpure_i hpure_o79 have hlinks : ∀ n, ∃ w : A,80 star w * w = alpha (f n) ∧ w * star w = f n := by81 intro n82 obtain ⟨g, hg⟩ := happrox {f n} 1 zero_lt_one83 have hclose : ‖alpha (f n) - (g : A) * f n * star (g : A)‖ < 1 := by84 exact hg (f n) (by simp)85 have he : IsStarProjection (alpha (f n)) := (hf n).map alpha86 have hr : IsStarProjection ((g : A) * f n * star (g : A)) :=87 (hf n).unitary_conjugate g88 obtain ⟨t, ht⟩ :=89 he.exists_unitary_conjugate_of_norm_sub_lt_one hr hclose90 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)⟩9495theorem 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 := by105 classical106 letI : Nontrivial A := hsimple.1107 obtain ⟨alpha, hstate, happrox⟩ :=108 hKOS A hsimple phi_i phi_o hpure_i hpure_o109 obtain ⟨g, hg⟩ := happrox {f} 1 zero_lt_one110 have hclose : ‖alpha f - (g : A) * f * star (g : A)‖ < 1 := by111 exact hg f (by simp)112 have he : IsStarProjection (alpha f) := hf.map alpha113 have hr : IsStarProjection ((g : A) * f * star (g : A)) :=114 hf.unitary_conjugate g115 obtain ⟨t, ht⟩ :=116 he.exists_unitary_conjugate_of_norm_sub_lt_one hr hclose117 let w := matchedLink g t (alpha f)118 have hw := matchedLink_supports g t (alpha f) f he ht119 exact ⟨alpha, hstate, w, hw⟩120121end MathlibAnnex.CStarAlgebra