Exact source: MathlibAnnex/Analysis/CStarAlgebra/ApproximateIntertwining.lean, lines 114–135.
Back to Two-sided inner sequences imply pure-state homogeneity
1import Mathlib.Algebra.Star.UnitaryStarAlgAut 2import Mathlib.Analysis.CStarAlgebra.Hom 3import Mathlib.Topology.Algebra.InfiniteSum.Real 4 5/-! 6# Two-sided pointwise limits of C-star algebra automorphisms 7 8The forward and inverse pointwise limits are kept together. This is the 9closure step required by an alternating approximately-inner construction: 10pointwise convergence of the forward maps alone would not prove surjectivity. 11-/ 12 13set_option autoImplicit false 14 15open Filter 16 17namespace MathlibAnnex.CStarAlgebra 18 19variable {A : Type*} [CStarAlgebra A] 20 21/-- Summable pointwise increments give the Cauchy input used by the 22two-sided limit construction. This records the actual norm budget rather 23than 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 := by 26 apply cauchySeq_of_summable_dist 27 simpa only [Nat.succ_eq_add_one, dist_eq_norm, norm_sub_rev] using hf 28 29/-- Point-norm approximate innerness, with one unitary serving the whole 30finite 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‖ < epsilon 35 36/-- 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)) 40 41theorem 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)) 45 46/-- 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 where 49 toFun := pointwiseLimit f hf 50 map_one' := by 51 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf 1) 52 simp 53 map_mul' a b := by 54 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf (a * b)) 55 simpa only [map_mul] using 56 (tendsto_pointwiseLimit f hf a).mul (tendsto_pointwiseLimit f hf b) 57 map_zero' := by 58 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf 0) 59 simp 60 map_add' a b := by 61 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf (a + b)) 62 simpa only [map_add] using 63 (tendsto_pointwiseLimit f hf a).add (tendsto_pointwiseLimit f hf b) 64 commutes' c := by 65 apply tendsto_nhds_unique (tendsto_pointwiseLimit f hf ((algebraMap ℂ A) c)) 66 simpa only [Algebra.algebraMap_eq_smul_one, map_smul, map_one] using 67 (tendsto_const_nhds : Tendsto (fun _ : ℕ => c • (1 : A)) atTop (nhds (c • 1))) 68 map_star' a := by 69 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) := by 72 funext n 73 exact map_star (f n) a 74 rw [hfun] 75 exact hstar 76 77@[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 := rfl 80 81/-- Isometric diagonal approximation identifies the value of the pointwise 82limit at a moving input. -/ 83theorem pointwiseLimitHom_apply_eq_of_diagonal 84 (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 := by 88 have hfixed : Tendsto (fun n => f n b) atTop 89 (nhds (pointwiseLimitHom f hf b)) := tendsto_pointwiseLimit f hf b 90 have hto_c : Tendsto (fun n => f n b) atTop (nhds c) := by 91 rw [Metric.tendsto_atTop] 92 intro epsilon hepsilon 93 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 calc 101 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 := by 105 apply add_lt_add 106 · simpa only [dist_comm] using hg_n 107 · exact hd_n 108 _ = epsilon := by ring 109 exact tendsto_nhds_unique hfixed hto_c 110 111/-- A two-sided pointwise Cauchy sequence of star-algebra equivalences has a 112star-algebra equivalence as its limit. The diagonal composition hypotheses 113are the forward/inverse controls needed to prevent a merely injective limit. -/ 114noncomputable def pointwiseLimitEquiv 115 (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 := by 121 let F := pointwiseLimitHom f hf 122 let G := pointwiseLimitHom g hg 123 have hFG (a : A) : F (G a) = a := by 124 apply pointwiseLimitHom_apply_eq_of_diagonal f hf (fun n => g n a) (G a) a 125 · exact tendsto_pointwiseLimit g hg a 126 · exact hfg a 127 have hGF (a : A) : G (F a) = a := by 128 apply pointwiseLimitHom_apply_eq_of_diagonal g hg (fun n => f n a) (F a) a 129 · exact tendsto_pointwiseLimit f hf a 130 · exact hgf a 131 exact StarAlgEquiv.ofBijective F ⟨ 132 fun x y hxy => by rw [← hGF x, ← hGF y, hxy], 133 fun y => ⟨G y, hFG y⟩⟩ 134 135@[simp] theorem pointwiseLimitEquiv_apply 136 (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 := rfl 142 143/-- A pointwise limit of inner automorphisms is point-norm approximately 144inner on every finite set. Surjectivity of the limit is supplied separately 145by the inverse and diagonal hypotheses of `pointwiseLimitEquiv`. -/ 146theorem isPointNormApproximatelyInner_pointwiseLimitEquiv 147 (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) := by 154 intro F epsilon hepsilon 155 have hconv (a : A) : Tendsto (fun n => f n a) atTop 156 (nhds (pointwiseLimitEquiv f g hf hg hfg hgf a)) := by 157 simpa only [pointwiseLimitEquiv_apply, pointwiseLimitHom_apply] using 158 tendsto_pointwiseLimit f hf a 159 have hfinite : ∀ᶠ n in atTop, ∀ a ∈ F, 160 ‖pointwiseLimitEquiv f g hf hg hfg hgf a - f n a‖ < epsilon := by 161 apply (F.eventually_all).2 162 intro a _ha 163 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 hn 167 simpa only [Metric.mem_ball, dist_eq_norm, norm_sub_rev] using hn 168 obtain ⟨n, hn⟩ := hfinite.exists 169 obtain ⟨u, hu⟩ := hinner n 170 refine ⟨u, fun a ha => ?_⟩ 171 rw [← hu] 172 exact hn a ha 173 174/-- The state equation also passes to the same forward pointwise limit. 175Together with the preceding theorem this is the non-circular global closure 176used after a local alternating construction has produced its two sequences. -/ 177theorem pointwiseLimitEquiv_state_and_approximatelyInner 178 (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) := by 188 refine ⟨?_, isPointNormApproximatelyInner_pointwiseLimitEquiv 189 f g hf hg hfg hgf hinner⟩ 190 intro a 191 apply tendsto_nhds_unique 192 ((phi.continuous.tendsto _).comp (show Tendsto (fun n => f n a) atTop 193 (nhds (pointwiseLimitEquiv f g hf hg hfg hgf a)) by 194 simpa only [pointwiseLimitEquiv_apply, pointwiseLimitHom_apply] using 195 tendsto_pointwiseLimit f hf a)) 196 exact hstate a 197 198/-- The two-sided pointwise limit when the inverse sequence is literally the 199sequence of inverse automorphisms. Requiring both pointwise Cauchy conditions 200is essential; the diagonal composition conditions are then exact. -/ 201noncomputable def twoSidedPointwiseLimit 202 (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 hfinv 207 (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))) 211 212@[simp] theorem twoSidedPointwiseLimit_apply 213 (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 rfl 218 219/-- The inverse of the two-sided pointwise limit is the pointwise limit of 220the actual inverse sequence. -/ 221theorem twoSidedPointwiseLimit_symm_apply 222 (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 := by 227 apply (twoSidedPointwiseLimit f hf hfinv).injective 228 calc 229 _ = a := (twoSidedPointwiseLimit f hf hfinv).apply_symm_apply a 230 _ = _ := by 231 symm 232 change pointwiseLimitHom f hf 233 (pointwiseLimitHom (fun n ↦ (f n).symm) hfinv a) = a 234 apply pointwiseLimitHom_apply_eq_of_diagonal f hf 235 (fun n ↦ (f n).symm a) 236 · exact tendsto_pointwiseLimit (fun n ↦ (f n).symm) hfinv a 237 · simpa using (tendsto_const_nhds : 238 Tendsto (fun _ : ℕ ↦ a) atTop (nhds a)) 239 240/-- Summable forward and inverse pointwise increments are a concrete budget 241for the two Cauchy hypotheses of `twoSidedPointwiseLimit`. -/ 242theorem twoSidedPointwiseCauchy_of_summable 243 (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)⟩ 251 252/-- Global approximately-inner state transport from a genuine two-sided 253inner-automorphism sequence. This is the reusable limit endpoint for the 254alternating local construction; no convergence of the implementing 255unitaries themselves is assumed. -/ 256theorem twoSidedPointwiseLimit_state_and_approximatelyInner 257 (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) := by 265 exact pointwiseLimitEquiv_state_and_approximatelyInner 266 f (fun n => (f n).symm) hf hfinv 267 (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 hstate 272 273end MathlibAnnex.CStarAlgebra