Exact source: MathlibAnnex/Analysis/CStarAlgebra/ApproximateIntertwining.lean
Pinned GitHub source · Raw UTF-8 source
Back to A two-sided inner intertwining sequence for two states · Back to Two-sided inner sequences imply pure-state homogeneity
1import Mathlib.Algebra.Star.UnitaryStarAlgAut2import Mathlib.Analysis.CStarAlgebra.Hom3import Mathlib.Topology.Algebra.InfiniteSum.Real45/-!6# Two-sided pointwise limits of C-star algebra automorphisms78The forward and inverse pointwise limits are kept together. This is the9closure step required by an alternating approximately-inner construction:10pointwise convergence of the forward maps alone would not prove surjectivity.11-/1213set_option autoImplicit false1415open Filter1617namespace MathlibAnnex.CStarAlgebra1819variable {A : Type*} [CStarAlgebra A]2021/-- Summable pointwise increments give the Cauchy input used by the22two-sided limit construction. This records the actual norm budget rather23than requiring convergence of the implementing unitaries. -/24theorem cauchySeq_of_summable_norm_step (f : ℕ → A)25 (hf : Summable fun n => ‖f (n + 1) - f n‖) : CauchySeq f := by26 apply cauchySeq_of_summable_dist27 simpa only [Nat.succ_eq_add_one, dist_eq_norm, norm_sub_rev] using hf2829/-- Point-norm approximate innerness, with one unitary serving the whole30finite set. -/31def IsPointNormApproximatelyInner (alpha : A ≃⋆ₐ[ℂ] A) : Prop :=32 ∀ (F : Finset A) (epsilon : ℝ), 0 < epsilon →33 ∃ u : unitary A, ∀ a ∈ F,34 ‖alpha a - Unitary.conjStarAlgAut ℂ A u a‖ < epsilon3536/-- The chosen pointwise limit of a pointwise Cauchy automorphism sequence. -/37noncomputable def pointwiseLimit (f : ℕ → StarAlgEquiv ℂ A A)38 (hf : ∀ a, CauchySeq (fun n => f n a)) (a : A) : A :=39 Classical.choose (cauchySeq_tendsto_of_complete (hf a))4041theorem tendsto_pointwiseLimit (f : ℕ → StarAlgEquiv ℂ A A)42 (hf : ∀ a, CauchySeq (fun n => f n a)) (a : A) :43 Tendsto (fun n => f n a) atTop (nhds (pointwiseLimit f hf a)) :=44 Classical.choose_spec (cauchySeq_tendsto_of_complete (hf a))4546/-- Algebraic operations pass to the chosen pointwise limit. -/47noncomputable def pointwiseLimitHom (f : ℕ → StarAlgEquiv ℂ A A)48 (hf : ∀ a, CauchySeq (fun n => f n a)) : A →⋆ₐ[ℂ] A where49 toFun := pointwiseLimit f hf50 map_one' := by51 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf 1)52 simp53 map_mul' a b := by54 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf (a * b))55 simpa only [map_mul] using56 (tendsto_pointwiseLimit f hf a).mul (tendsto_pointwiseLimit f hf b)57 map_zero' := by58 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf 0)59 simp60 map_add' a b := by61 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf (a + b))62 simpa only [map_add] using63 (tendsto_pointwiseLimit f hf a).add (tendsto_pointwiseLimit f hf b)64 commutes' c := by65 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf ((algebraMap ℂ A) c))66 simpa only [Algebra.algebraMap_eq_smul_one, map_smul, map_one] using67 (tendsto_const_nhds : Tendsto (fun _ : ℕ => c • (1 : A)) atTop (nhds (c • 1)))68 map_star' a := by69 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf (star a))70 have hstar := (continuous_star.tendsto _).comp (tendsto_pointwiseLimit f hf a)71 have hfun : (fun n => f n (star a)) = star ∘ (fun n => f n a) := by72 funext n73 exact map_star (f n) a74 rw [hfun]75 exact hstar7677@[simp] theorem pointwiseLimitHom_apply (f : ℕ → StarAlgEquiv ℂ A A)78 (hf : ∀ a, CauchySeq (fun n => f n a)) (a : A) :79 pointwiseLimitHom f hf a = pointwiseLimit f hf a := rfl8081/-- Isometric diagonal approximation identifies the value of the pointwise82limit at a moving input. -/83theorem pointwiseLimitHom_apply_eq_of_diagonal84 (f : ℕ → StarAlgEquiv ℂ A A) (hf : ∀ a, CauchySeq (fun n => f n a))85 (g : ℕ → A) (b c : A) (hg : Tendsto g atTop (nhds b))86 (hdiag : Tendsto (fun n => f n (g n)) atTop (nhds c)) :87 pointwiseLimitHom f hf b = c := by88 have hfixed : Tendsto (fun n => f n b) atTop89 (nhds (pointwiseLimitHom f hf b)) := tendsto_pointwiseLimit f hf b90 have hto_c : Tendsto (fun n => f n b) atTop (nhds c) := by91 rw [Metric.tendsto_atTop]92 intro epsilon hepsilon93 obtain ⟨Ng, hNg⟩ := (Metric.tendsto_atTop.mp hg) (epsilon / 2) (by positivity)94 obtain ⟨Nd, hNd⟩ := (Metric.tendsto_atTop.mp hdiag) (epsilon / 2) (by positivity)95 refine ⟨max Ng Nd, fun n hn => ?_⟩96 have hg_n := hNg n (le_trans (le_max_left Ng Nd) hn)97 have hd_n := hNd n (le_trans (le_max_right Ng Nd) hn)98 have hdist : dist (f n b) (f n (g n)) = dist b (g n) :=99 (StarAlgEquiv.isometry (f n)).dist_eq b (g n)100 calc101 dist (f n b) c ≤ dist (f n b) (f n (g n)) + dist (f n (g n)) c :=102 dist_triangle _ _ _103 _ = dist b (g n) + dist (f n (g n)) c := by rw [hdist]104 _ < epsilon / 2 + epsilon / 2 := by105 apply add_lt_add106 · simpa only [dist_comm] using hg_n107 · exact hd_n108 _ = epsilon := by ring109 exact tendsto_nhds_unique hfixed hto_c110111/-- A two-sided pointwise Cauchy sequence of star-algebra equivalences has a112star-algebra equivalence as its limit. The diagonal composition hypotheses113are the forward/inverse controls needed to prevent a merely injective limit. -/114noncomputable def pointwiseLimitEquiv115 (f g : ℕ → StarAlgEquiv ℂ A A)116 (hf : ∀ a, CauchySeq (fun n => f n a))117 (hg : ∀ a, CauchySeq (fun n => g n a))118 (hfg : ∀ a, Tendsto (fun n => f n (g n a)) atTop (nhds a))119 (hgf : ∀ a, Tendsto (fun n => g n (f n a)) atTop (nhds a)) :120 StarAlgEquiv ℂ A A := by121 let F := pointwiseLimitHom f hf122 let G := pointwiseLimitHom g hg123 have hFG (a : A) : F (G a) = a := by124 apply pointwiseLimitHom_apply_eq_of_diagonal f hf (fun n => g n a) (G a) a125 · exact tendsto_pointwiseLimit g hg a126 · exact hfg a127 have hGF (a : A) : G (F a) = a := by128 apply pointwiseLimitHom_apply_eq_of_diagonal g hg (fun n => f n a) (F a) a129 · exact tendsto_pointwiseLimit f hf a130 · exact hgf a131 exact StarAlgEquiv.ofBijective F ⟨132 fun x y hxy => by rw [← hGF x, ← hGF y, hxy],133 fun y => ⟨G y, hFG y⟩⟩134135@[simp] theorem pointwiseLimitEquiv_apply136 (f g : ℕ → StarAlgEquiv ℂ A A)137 (hf : ∀ a, CauchySeq (fun n => f n a))138 (hg : ∀ a, CauchySeq (fun n => g n a))139 (hfg : ∀ a, Tendsto (fun n => f n (g n a)) atTop (nhds a))140 (hgf : ∀ a, Tendsto (fun n => g n (f n a)) atTop (nhds a)) (a : A) :141 pointwiseLimitEquiv f g hf hg hfg hgf a = pointwiseLimitHom f hf a := rfl142143/-- A pointwise limit of inner automorphisms is point-norm approximately144inner on every finite set. Surjectivity of the limit is supplied separately145by the inverse and diagonal hypotheses of `pointwiseLimitEquiv`. -/146theorem isPointNormApproximatelyInner_pointwiseLimitEquiv147 (f g : ℕ → StarAlgEquiv ℂ A A)148 (hf : ∀ a, CauchySeq (fun n => f n a))149 (hg : ∀ a, CauchySeq (fun n => g n a))150 (hfg : ∀ a, Tendsto (fun n => f n (g n a)) atTop (nhds a))151 (hgf : ∀ a, Tendsto (fun n => g n (f n a)) atTop (nhds a))152 (hinner : ∀ n, ∃ u : unitary A, f n = Unitary.conjStarAlgAut ℂ A u) :153 IsPointNormApproximatelyInner (pointwiseLimitEquiv f g hf hg hfg hgf) := by154 intro F epsilon hepsilon155 have hconv (a : A) : Tendsto (fun n => f n a) atTop156 (nhds (pointwiseLimitEquiv f g hf hg hfg hgf a)) := by157 simpa only [pointwiseLimitEquiv_apply, pointwiseLimitHom_apply] using158 tendsto_pointwiseLimit f hf a159 have hfinite : ∀ᶠ n in atTop, ∀ a ∈ F,160 ‖pointwiseLimitEquiv f g hf hg hfg hgf a - f n a‖ < epsilon := by161 apply (F.eventually_all).2162 intro a _ha163 have ha : ∀ᶠ n in atTop,164 f n a ∈ Metric.ball (pointwiseLimitEquiv f g hf hg hfg hgf a) epsilon :=165 (hconv a) (Metric.ball_mem_nhds _ hepsilon)166 filter_upwards [ha] with n hn167 simpa only [Metric.mem_ball, dist_eq_norm, norm_sub_rev] using hn168 obtain ⟨n, hn⟩ := hfinite.exists169 obtain ⟨u, hu⟩ := hinner n170 refine ⟨u, fun a ha => ?_⟩171 rw [← hu]172 exact hn a ha173174/-- The state equation also passes to the same forward pointwise limit.175Together with the preceding theorem this is the non-circular global closure176used after a local alternating construction has produced its two sequences. -/177theorem pointwiseLimitEquiv_state_and_approximatelyInner178 (f g : ℕ → StarAlgEquiv ℂ A A)179 (hf : ∀ a, CauchySeq (fun n => f n a))180 (hg : ∀ a, CauchySeq (fun n => g n a))181 (hfg : ∀ a, Tendsto (fun n => f n (g n a)) atTop (nhds a))182 (hgf : ∀ a, Tendsto (fun n => g n (f n a)) atTop (nhds a))183 (hinner : ∀ n, ∃ u : unitary A, f n = Unitary.conjStarAlgAut ℂ A u)184 (phi psi : A →L[ℂ] ℂ)185 (hstate : ∀ a, Tendsto (fun n => phi (f n a)) atTop (nhds (psi a))) :186 (∀ a, phi (pointwiseLimitEquiv f g hf hg hfg hgf a) = psi a) ∧187 IsPointNormApproximatelyInner (pointwiseLimitEquiv f g hf hg hfg hgf) := by188 refine ⟨?_, isPointNormApproximatelyInner_pointwiseLimitEquiv189 f g hf hg hfg hgf hinner⟩190 intro a191 apply tendsto_nhds_unique192 ((phi.continuous.tendsto _).comp (show Tendsto (fun n => f n a) atTop193 (nhds (pointwiseLimitEquiv f g hf hg hfg hgf a)) by194 simpa only [pointwiseLimitEquiv_apply, pointwiseLimitHom_apply] using195 tendsto_pointwiseLimit f hf a))196 exact hstate a197198/-- The two-sided pointwise limit when the inverse sequence is literally the199sequence of inverse automorphisms. Requiring both pointwise Cauchy conditions200is essential; the diagonal composition conditions are then exact. -/201noncomputable def twoSidedPointwiseLimit202 (f : ℕ → StarAlgEquiv ℂ A A)203 (hf : ∀ a, CauchySeq (fun n => f n a))204 (hfinv : ∀ a, CauchySeq (fun n => (f n).symm a)) :205 StarAlgEquiv ℂ A A :=206 pointwiseLimitEquiv f (fun n => (f n).symm) hf hfinv207 (fun a => by simpa using (tendsto_const_nhds :208 Tendsto (fun _ : ℕ => a) atTop (nhds a)))209 (fun a => by simpa using (tendsto_const_nhds :210 Tendsto (fun _ : ℕ => a) atTop (nhds a)))211212@[simp] theorem twoSidedPointwiseLimit_apply213 (f : ℕ → StarAlgEquiv ℂ A A)214 (hf : ∀ a, CauchySeq (fun n => f n a))215 (hfinv : ∀ a, CauchySeq (fun n => (f n).symm a)) (a : A) :216 twoSidedPointwiseLimit f hf hfinv a = pointwiseLimitHom f hf a :=217 rfl218219/-- The inverse of the two-sided pointwise limit is the pointwise limit of220the actual inverse sequence. -/221theorem twoSidedPointwiseLimit_symm_apply222 (f : ℕ → StarAlgEquiv ℂ A A)223 (hf : ∀ a, CauchySeq (fun n ↦ f n a))224 (hfinv : ∀ a, CauchySeq (fun n ↦ (f n).symm a)) (a : A) :225 (twoSidedPointwiseLimit f hf hfinv).symm a =226 pointwiseLimitHom (fun n ↦ (f n).symm) hfinv a := by227 apply (twoSidedPointwiseLimit f hf hfinv).injective228 calc229 _ = a := (twoSidedPointwiseLimit f hf hfinv).apply_symm_apply a230 _ = _ := by231 symm232 change pointwiseLimitHom f hf233 (pointwiseLimitHom (fun n ↦ (f n).symm) hfinv a) = a234 apply pointwiseLimitHom_apply_eq_of_diagonal f hf235 (fun n ↦ (f n).symm a)236 · exact tendsto_pointwiseLimit (fun n ↦ (f n).symm) hfinv a237 · simpa using (tendsto_const_nhds :238 Tendsto (fun _ : ℕ ↦ a) atTop (nhds a))239240/-- Summable forward and inverse pointwise increments are a concrete budget241for the two Cauchy hypotheses of `twoSidedPointwiseLimit`. -/242theorem twoSidedPointwiseCauchy_of_summable243 (f : ℕ → StarAlgEquiv ℂ A A)244 (hforward : ∀ a, Summable fun n => ‖f (n + 1) a - f n a‖)245 (hinverse : ∀ a, Summable fun n =>246 ‖(f (n + 1)).symm a - (f n).symm a‖) :247 (∀ a, CauchySeq (fun n => f n a)) ∧248 ∀ a, CauchySeq (fun n => (f n).symm a) :=249 ⟨fun a => cauchySeq_of_summable_norm_step _ (hforward a),250 fun a => cauchySeq_of_summable_norm_step _ (hinverse a)⟩251252/-- Global approximately-inner state transport from a genuine two-sided253inner-automorphism sequence. This is the reusable limit endpoint for the254alternating local construction; no convergence of the implementing255unitaries themselves is assumed. -/256theorem twoSidedPointwiseLimit_state_and_approximatelyInner257 (f : ℕ → StarAlgEquiv ℂ A A)258 (hf : ∀ a, CauchySeq (fun n => f n a))259 (hfinv : ∀ a, CauchySeq (fun n => (f n).symm a))260 (hinner : ∀ n, ∃ u : unitary A, f n = Unitary.conjStarAlgAut ℂ A u)261 (phi psi : A →L[ℂ] ℂ)262 (hstate : ∀ a, Tendsto (fun n => phi (f n a)) atTop (nhds (psi a))) :263 (∀ a, phi (twoSidedPointwiseLimit f hf hfinv a) = psi a) ∧264 IsPointNormApproximatelyInner (twoSidedPointwiseLimit f hf hfinv) := by265 exact pointwiseLimitEquiv_state_and_approximatelyInner266 f (fun n => (f n).symm) hf hfinv267 (fun a => by simpa using (tendsto_const_nhds :268 Tendsto (fun _ : ℕ => a) atTop (nhds a)))269 (fun a => by simpa using (tendsto_const_nhds :270 Tendsto (fun _ : ℕ => a) atTop (nhds a)))271 hinner phi psi hstate272273end MathlibAnnex.CStarAlgebra