Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Homogeneity.lean, lines 22–32.
Back to Approximately inner homogeneity of pure CAR states · Back to Pure-state homogeneity of the completed CAR algebra
1import MathlibAnnex.Analysis.CStarAlgebra.ApproximateIntertwining 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteAverage 3import MathlibAnnex.Analysis.CStarAlgebra.CAR.NoCompacts 4import MathlibAnnex.Analysis.CStarAlgebra.PureStateHomogeneity.KishimotoOzawaSakai 5 6/-! 7# The CAR homogeneity endpoint and its two-sided limit adapter 8 9`PureStateHomogeneity` is the exact CAR-specialized endpoint (`K_CAR`). The 10second definition records the constructive output still required from the 11local pure-state movement argument. The theorem in this file closes that 12output by the proved two-sided point-norm limit machinery; it does not assume 13an automorphism or homogeneity as an input. 14-/ 15 16set_option autoImplicit false 17 18open Filter 19 20namespace MathlibAnnex.CStarAlgebra.CAR 21 22/-- Approximate-inner homogeneity for the actual completed CAR algebra. This 23is the exact `K_CAR` proposition and is deliberately distinct from the 24all-simple-algebras statement `MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty`. -/ 25def PureStateHomogeneity : Prop := 26 ∀ (phi psi : Limit →L[ℂ] ℂ), MathlibAnnex.CStarAlgebra.IsPureState Limit phi → 27 MathlibAnnex.CStarAlgebra.IsPureState Limit psi → 28 ∃ alpha : Limit ≃⋆ₐ[ℂ] Limit, 29 (∀ a : Limit, phi (alpha a) = psi a) ∧ 30 ∀ (F : Finset Limit) (epsilon : ℝ), 0 < epsilon → 31 ∃ v : unitary Limit, ∀ a ∈ F, 32 ‖alpha a - (v : Limit) * a * star (v : Limit)‖ < epsilon 33 34/-- Asymptotically-inner homogeneity for the completed CAR algebra. The 35implementing path is parametrized by `ℝ` and starts at one. Negative-time 36constancy is a property of the concrete path built below, not a field of this 37predicate. Both the automorphisms and their actual inverses converge 38point-norm. -/ 39def AsymptoticallyInnerPureStateHomogeneity : Prop := 40 ∀ (phi psi : Limit →L[ℂ] ℂ), MathlibAnnex.CStarAlgebra.IsPureState Limit phi → 41 MathlibAnnex.CStarAlgebra.IsPureState Limit psi → 42 ∃ alpha : Limit ≃⋆ₐ[ℂ] Limit, ∃ U : ℝ → unitary Limit, 43 Continuous U ∧ U 0 = 1 ∧ 44 (∀ a : Limit, phi (alpha a) = psi a) ∧ 45 (∀ a : Limit, Tendsto 46 (fun t ↦ Unitary.conjStarAlgAut ℂ Limit (U t) a) 47 atTop (nhds (alpha a))) ∧ 48 ∀ a : Limit, Tendsto 49 (fun t ↦ (Unitary.conjStarAlgAut ℂ Limit (U t)).symm a) 50 atTop (nhds (alpha.symm a)) 51 52set_option maxHeartbeats 800000 in 53/-- Forgetting the path, asymptotically-inner homogeneity implies the 54original point-norm approximately-inner endpoint. -/ 55theorem homogeneity_of_asymptoticallyInner 56 (h : AsymptoticallyInnerPureStateHomogeneity) : PureStateHomogeneity := by 57 intro phi psi hphi hpsi 58 obtain ⟨alpha, U, _hU, _hU0, hstate, hforward, _hinverse⟩ := 59 h phi psi hphi hpsi 60 refine ⟨alpha, hstate, ?_⟩ 61 intro F epsilon hepsilon 62 have hfinite : ∀ᶠ t in atTop, ∀ a ∈ F, 63 ‖alpha a - Unitary.conjStarAlgAut ℂ Limit (U t) a‖ < epsilon := by 64 apply (F.eventually_all).2 65 intro a _ha 66 have ha := (hforward a) (Metric.ball_mem_nhds _ hepsilon) 67 filter_upwards [ha] with t ht 68 change dist (Unitary.conjStarAlgAut ℂ Limit (U t) a) (alpha a) < epsilon at ht 69 rw [dist_eq_norm, norm_sub_rev] at ht 70 exact ht 71 obtain ⟨t, ht⟩ := hfinite.exists 72 refine ⟨U t, ?_⟩ 73 intro a ha 74 change ‖alpha a - Unitary.conjStarAlgAut ℂ Limit (U t) a‖ < epsilon 75 exact ht a ha 76 77/-- Concrete two-sided output expected from an alternating local movement 78construction. It asks for inner automorphisms, pointwise Cauchy control of 79both them and their actual inverses, and convergence of the transported 80state. It contains no endpoint automorphism field. -/ 81def HasInnerIntertwiningSequence (phi psi : Limit →L[ℂ] ℂ) : Prop := 82 ∃ f : ℕ → StarAlgEquiv ℂ Limit Limit, 83 (∀ a, CauchySeq (fun n => f n a)) ∧ 84 (∀ a, CauchySeq (fun n => (f n).symm a)) ∧ 85 (∀ n, ∃ u : unitary Limit, 86 f n = Unitary.conjStarAlgAut ℂ Limit u) ∧ 87 ∀ a, Tendsto (fun n => phi (f n a)) atTop (nhds (psi a)) 88 89/-- The proved two-sided limit turns the exact constructive sequence contract 90into the exact CAR endpoint. In particular, surjectivity is not inferred 91from a forward pointwise limit alone. -/ 92theorem homogeneity_of_innerIntertwiningSequences 93 (hlocal : ∀ (phi psi : Limit →L[ℂ] ℂ), 94 MathlibAnnex.CStarAlgebra.IsPureState Limit phi → MathlibAnnex.CStarAlgebra.IsPureState Limit psi → 95 HasInnerIntertwiningSequence phi psi) : 96 PureStateHomogeneity := by 97 intro phi psi hphi hpsi 98 obtain ⟨f, hf, hfinv, hinner, hstate⟩ := hlocal phi psi hphi hpsi 99 let alpha := MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit f hf hfinv 100 have hend := 101 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit_state_and_approximatelyInner 102 f hf hfinv hinner phi psi hstate 103 refine ⟨alpha, hend.1, ?_⟩ 104 exact hend.2 105 106end MathlibAnnex.CStarAlgebra.CAR