Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Homogeneity.lean
Pinned GitHub source · Raw UTF-8 source
Back to Pure-state homogeneity of the completed CAR algebra · Back to Two-sided inner sequences imply pure-state homogeneity
1import MathlibAnnex.Analysis.CStarAlgebra.ApproximateIntertwining2import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteAverage3import MathlibAnnex.Analysis.CStarAlgebra.CAR.NoCompacts4import MathlibAnnex.Analysis.CStarAlgebra.PureStateHomogeneity.KishimotoOzawaSakai56/-!7# The CAR homogeneity endpoint and its two-sided limit adapter89`PureStateHomogeneity` is the exact CAR-specialized endpoint (`K_CAR`). The10second definition records the constructive output still required from the11local pure-state movement argument. The theorem in this file closes that12output by the proved two-sided point-norm limit machinery; it does not assume13an automorphism or homogeneity as an input.14-/1516set_option autoImplicit false1718open Filter1920namespace MathlibAnnex.CStarAlgebra.CAR2122/-- Approximate-inner homogeneity for the actual completed CAR algebra. This23is the exact `K_CAR` proposition and is deliberately distinct from the24all-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)‖ < epsilon3334/-- Asymptotically-inner homogeneity for the completed CAR algebra. The35implementing path is parametrized by `ℝ` and starts at one. Negative-time36constancy is a property of the concrete path built below, not a field of this37predicate. Both the automorphisms and their actual inverses converge38point-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, Tendsto46 (fun t ↦ Unitary.conjStarAlgAut ℂ Limit (U t) a)47 atTop (nhds (alpha a))) ∧48 ∀ a : Limit, Tendsto49 (fun t ↦ (Unitary.conjStarAlgAut ℂ Limit (U t)).symm a)50 atTop (nhds (alpha.symm a))5152set_option maxHeartbeats 800000 in53/-- Forgetting the path, asymptotically-inner homogeneity implies the54original point-norm approximately-inner endpoint. -/55theorem homogeneity_of_asymptoticallyInner56 (h : AsymptoticallyInnerPureStateHomogeneity) : PureStateHomogeneity := by57 intro phi psi hphi hpsi58 obtain ⟨alpha, U, _hU, _hU0, hstate, hforward, _hinverse⟩ :=59 h phi psi hphi hpsi60 refine ⟨alpha, hstate, ?_⟩61 intro F epsilon hepsilon62 have hfinite : ∀ᶠ t in atTop, ∀ a ∈ F,63 ‖alpha a - Unitary.conjStarAlgAut ℂ Limit (U t) a‖ < epsilon := by64 apply (F.eventually_all).265 intro a _ha66 have ha := (hforward a) (Metric.ball_mem_nhds _ hepsilon)67 filter_upwards [ha] with t ht68 change dist (Unitary.conjStarAlgAut ℂ Limit (U t) a) (alpha a) < epsilon at ht69 rw [dist_eq_norm, norm_sub_rev] at ht70 exact ht71 obtain ⟨t, ht⟩ := hfinite.exists72 refine ⟨U t, ?_⟩73 intro a ha74 change ‖alpha a - Unitary.conjStarAlgAut ℂ Limit (U t) a‖ < epsilon75 exact ht a ha7677/-- Concrete two-sided output expected from an alternating local movement78construction. It asks for inner automorphisms, pointwise Cauchy control of79both them and their actual inverses, and convergence of the transported80state. 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))8889/-- The proved two-sided limit turns the exact constructive sequence contract90into the exact CAR endpoint. In particular, surjectivity is not inferred91from a forward pointwise limit alone. -/92theorem homogeneity_of_innerIntertwiningSequences93 (hlocal : ∀ (phi psi : Limit →L[ℂ] ℂ),94 MathlibAnnex.CStarAlgebra.IsPureState Limit phi → MathlibAnnex.CStarAlgebra.IsPureState Limit psi →95 HasInnerIntertwiningSequence phi psi) :96 PureStateHomogeneity := by97 intro phi psi hphi hpsi98 obtain ⟨f, hf, hfinv, hinner, hstate⟩ := hlocal phi psi hphi hpsi99 let alpha := MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit f hf hfinv100 have hend :=101 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit_state_and_approximatelyInner102 f hf hfinv hinner phi psi hstate103 refine ⟨alpha, hend.1, ?_⟩104 exact hend.2105106end MathlibAnnex.CStarAlgebra.CAR