Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Completion.lean, lines 539–548.
Back to The product-vector state on the completed CAR algebra · Back to Purity of the completed root state
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.PureRoot 2import Mathlib.Algebra.Colimit.DirectLimit 3import Mathlib.Topology.MetricSpace.Gluing 4import Mathlib.Algebra.Star.TransferInstance 5import Mathlib.Algebra.Algebra.TransferInstance 6import Mathlib.Analysis.Normed.Module.Completion 7import Mathlib.Analysis.Normed.Operator.Extend 8import Mathlib.Analysis.CStarAlgebra.Projection 9 10set_option autoImplicit false 11 12open scoped ComplexOrder 13open Set 14 15namespace MathlibAnnex.CStarAlgebra.CAR 16 17/-- The compatible embedding between arbitrary finite stages. -/ 18noncomputable def embed (n m : ℕ) (h : n ≤ m) : Stage n →⋆ₐ[ℂ] Stage m := 19 Nat.leRecOn h (fun {k} g => (step k).comp g) (StarAlgHom.id ℂ (Stage n)) 20 21@[simp] 22theorem embed_refl (n : ℕ) : embed n n le_rfl = StarAlgHom.id ℂ (Stage n) := by 23 unfold embed 24 exact Nat.leRecOn_self _ 25 26@[simp] 27theorem embed_succ (n m : ℕ) (h : n ≤ m) : 28 embed n (m + 1) (Nat.le.step h) = (step m).comp (embed n m h) := by 29 unfold embed 30 exact Nat.leRecOn_succ h _ 31 32@[simp] 33theorem embed_apply (n : ℕ) : ∀ (m : ℕ) (h : n ≤ m) (x : Stage n), 34 embed n m h x = Nat.leRecOn h (fun {k} y => step k y) x := by 35 apply Nat.le_induction 36 · intro x 37 rw [embed_refl] 38 exact (Nat.leRecOn_self x).symm 39 · intro m h ih x 40 rw [embed_succ, StarAlgHom.comp_apply, ih, Nat.leRecOn_succ h] 41 exact h 42 43theorem embed_trans (i j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k) : 44 embed i k (hij.trans hjk) = (embed j k hjk).comp (embed i j hij) := by 45 apply StarAlgHom.ext 46 intro x 47 simp only [StarAlgHom.comp_apply, embed_apply] 48 exact Nat.leRecOn_trans hij hjk x 49 50noncomputable instance embedDirectedSystem : 51 DirectedSystem Stage (fun _ _ h => embed _ _ h) where 52 map_self {i} x := by rw [embed_refl]; rfl 53 map_map {k j i} hij hjk x := by rw [← StarAlgHom.comp_apply, ← embed_trans] 54 55/-- The algebraic union of all binary matrix stages. -/ 56abbrev AlgCAR := DirectLimit Stage (fun _ _ h => embed _ _ h) 57 58theorem norm_embed (n : ℕ) : ∀ (m : ℕ) (h : n ≤ m) (x : Stage n), 59 ‖embed n m h x‖ = ‖x‖ := by 60 apply Nat.le_induction 61 · intro x 62 rw [embed_refl] 63 rfl 64 · intro m h ih x 65 rw [embed_succ, StarAlgHom.comp_apply, norm_step, ih] 66 exact h 67 68theorem embed_injective (n m : ℕ) (h : n ≤ m) : Function.Injective (embed n m h) := 69 fun x y hxy => by 70 rw [← sub_eq_zero, ← norm_eq_zero, ← norm_embed n m h] 71 simp only [map_sub, hxy, sub_self, norm_zero] 72 73theorem isometry_step (n : ℕ) : Isometry (step n) := 74 AddMonoidHomClass.isometry_of_norm (step n) (norm_step n) 75 76theorem isometry_stage : ∀ n, Isometry (fun x : Stage n => step n x) := 77 isometry_step 78 79/-- The metric union of the finite CAR stages. -/ 80abbrev PreCAR := Metric.InductiveLimit isometry_stage 81 82/-- The finite-stage map into the metric union. -/ 83noncomputable def toPreCAR (n : ℕ) : Stage n → PreCAR := 84 Metric.toInductiveLimit isometry_stage n 85 86theorem isometry_toPreCAR (n : ℕ) : Isometry (toPreCAR n) := 87 Metric.toInductiveLimit_isometry isometry_stage n 88 89@[simp] 90theorem toPreCAR_step (n : ℕ) (x : Stage n) : 91 toPreCAR (n + 1) (step n x) = toPreCAR n x := by 92 exact congrFun (Metric.toInductiveLimit_commute isometry_stage n) x 93 94theorem toPreCAR_embed (n : ℕ) : ∀ (m : ℕ) (h : n ≤ m) (x : Stage n), 95 toPreCAR m (embed n m h x) = toPreCAR n x := by 96 apply Nat.le_induction 97 · intro x 98 rw [embed_refl] 99 rfl 100 · intro m h ih x 101 rw [embed_succ, StarAlgHom.comp_apply, toPreCAR_step, ih] 102 exact h 103 104private theorem alg_compatible (x y : Σ n, Stage n) 105 (hxy : @Inseparable _ (Metric.inductivePremetric isometry_stage).toUniformSpace.toTopologicalSpace 106 x y) : 107 (⟦x⟧ : AlgCAR) = ⟦y⟧ := by 108 let m := max x.1 y.1 109 have hx : x.1 ≤ m := le_max_left _ _ 110 have hy : y.1 ≤ m := le_max_right _ _ 111 have hdist : Metric.inductiveLimitDist (fun n x => step n x) x y = 0 := 112 (@Metric.inseparable_iff _ (Metric.inductivePremetric isometry_stage) x y).mp hxy 113 have hd : dist (Nat.leRecOn hx (fun {k} z => step k z) x.2 : Stage m) 114 (Nat.leRecOn hy (fun {k} z => step k z) y.2 : Stage m) = 0 := by 115 rw [← Metric.inductiveLimitDist_eq_dist isometry_stage x y m hx hy] 116 exact hdist 117 have he : (Nat.leRecOn hx (fun {k} z => step k z) x.2 : Stage m) = 118 (Nat.leRecOn hy (fun {k} z => step k z) y.2 : Stage m) := dist_eq_zero.mp hd 119 apply Quotient.sound 120 exact ⟨m, hx, hy, by simpa only [embed_apply] using he⟩ 121 122/-- Forget the metric presentation of the union. -/ 123noncomputable def preToAlg : PreCAR → AlgCAR := 124 @SeparationQuotient.lift _ _ 125 (Metric.inductivePremetric isometry_stage).toUniformSpace.toTopologicalSpace 126 (fun x => (⟦x⟧ : AlgCAR)) alg_compatible 127 128@[simp] 129theorem preToAlg_toPreCAR (n : ℕ) (x : Stage n) : 130 preToAlg (toPreCAR n x) = (⟦⟨n, x⟩⟧ : AlgCAR) := by 131 rfl 132 133/-- Recover the metric presentation from the algebraic direct limit. -/ 134noncomputable def algToPre : AlgCAR → PreCAR := 135 DirectLimit.lift (fun _ _ h => embed _ _ h) (fun n => toPreCAR n) 136 (fun i j h x => (toPreCAR_embed i j h x).symm) 137 138@[simp] 139theorem algToPre_mk (n : ℕ) (x : Stage n) : 140 algToPre (⟦⟨n, x⟩⟧ : AlgCAR) = toPreCAR n x := rfl 141 142theorem algToPre_preToAlg (x : PreCAR) : algToPre (preToAlg x) = x := by 143 obtain ⟨⟨n, y⟩, rfl⟩ := Quotient.exists_rep x 144 rfl 145 146theorem preToAlg_algToPre (x : AlgCAR) : preToAlg (algToPre x) = x := by 147 obtain ⟨⟨n, y⟩, rfl⟩ := Quotient.exists_rep x 148 rfl 149 150/-- Algebraic and metric presentations of the stage union coincide. -/ 151noncomputable def preAlgEquiv : PreCAR ≃ AlgCAR where 152 toFun := preToAlg 153 invFun := algToPre 154 left_inv := algToPre_preToAlg 155 right_inv := preToAlg_algToPre 156 157noncomputable instance preRing : Ring PreCAR := preAlgEquiv.ring 158 159noncomputable instance preAlgebra : Algebra ℂ PreCAR := Equiv.algebra ℂ preAlgEquiv 160 161noncomputable instance preStarRing : StarRing PreCAR := preAlgEquiv.starRing 162 163noncomputable instance preStarModule : StarModule ℂ PreCAR := preAlgEquiv.starModule ℂ 164 165/-- The equivalence between metric and algebraic unions respects all star-algebra operations. -/ 166noncomputable def preStarAlgEquiv : PreCAR ≃⋆ₐ[ℂ] AlgCAR where 167 __ := Equiv.ringEquiv preAlgEquiv 168 map_star' x := by 169 change preToAlg (algToPre (star (preToAlg x))) = star (preToAlg x) 170 exact preToAlg_algToPre _ 171 map_smul' r x := by 172 simp [Equiv.smul_def] 173 174/-- The canonical algebraic map of a finite stage into the algebraic union. -/ 175noncomputable def algStageHom (n : ℕ) : Stage n →⋆ₐ[ℂ] AlgCAR where 176 __ := DirectLimit.Algebra.of Stage (fun _ _ h => embed _ _ h) n 177 map_star' _ := rfl 178 179/-- The canonical map of a finite stage into the metric union. -/ 180noncomputable def stageHom (n : ℕ) : Stage n →⋆ₐ[ℂ] PreCAR := 181 preStarAlgEquiv.symm.toStarAlgHom.comp (algStageHom n) 182 183@[simp] 184theorem stageHom_apply (n : ℕ) (x : Stage n) : stageHom n x = toPreCAR n x := by 185 apply preAlgEquiv.injective 186 rfl 187 188theorem stageHom_injective (n : ℕ) : Function.Injective (stageHom n) := 189 fun x y h => (isometry_toPreCAR n).injective <| by simpa only [← stageHom_apply] using h 190 191theorem exists_common_stage (x y : PreCAR) : 192 ∃ n, ∃ a b : Stage n, stageHom n a = x ∧ stageHom n b = y := by 193 obtain ⟨n, a, b, ha, hb⟩ := 194 DirectLimit.exists_eq_mk₂ (fun _ _ h => embed _ _ h) (preToAlg x) (preToAlg y) 195 refine ⟨n, a, b, ?_, ?_⟩ 196 · apply preAlgEquiv.injective 197 exact ha.symm 198 · apply preAlgEquiv.injective 199 exact hb.symm 200 201noncomputable instance preNorm : Norm PreCAR where 202 norm x := dist x 0 203 204@[simp] 205theorem norm_stageHom (n : ℕ) (x : Stage n) : ‖stageHom n x‖ = ‖x‖ := by 206 rw [stageHom_apply] 207 change dist (toPreCAR n x) 0 = ‖x‖ 208 rw [← map_zero (stageHom n), stageHom_apply, (isometry_toPreCAR n).dist_eq] 209 exact dist_zero_right x 210 211noncomputable instance preNormedAddCommGroup : NormedAddCommGroup PreCAR where 212 toNorm := preNorm 213 toAddCommGroup := preRing.toAddCommGroup 214 toMetricSpace := Metric.instMetricSpaceInductiveLimit 215 dist_eq x y := by 216 obtain ⟨n, a, b, rfl, rfl⟩ := exists_common_stage x y 217 rw [← map_neg, ← map_add, norm_stageHom] 218 calc 219 dist ((stageHom n) a) ((stageHom n) b) = dist a b := by 220 simpa only [stageHom_apply] using (isometry_toPreCAR n).dist_eq a b 221 _ = ‖-a + b‖ := NormedAddGroup.dist_eq a b 222 223noncomputable instance preNormedRing : NormedRing PreCAR where 224 __ := preNormedAddCommGroup 225 __ := preRing 226 norm_mul_le x y := by 227 obtain ⟨n, a, b, rfl, rfl⟩ := exists_common_stage x y 228 simpa only [← map_mul, norm_stageHom] using norm_mul_le a b 229 230noncomputable instance preNormedSpace : NormedSpace ℂ PreCAR where 231 norm_smul_le c x := by 232 obtain ⟨n, a, b, ha, _⟩ := exists_common_stage x x 233 rw [← ha] 234 calc 235 ‖c • stageHom n a‖ = ‖stageHom n (c • a)‖ := by rw [map_smul] 236 _ = ‖c • a‖ := norm_stageHom n _ 237 _ ≤ ‖c‖ * ‖a‖ := norm_smul_le c a 238 _ = ‖c‖ * ‖stageHom n a‖ := by rw [norm_stageHom] 239 240noncomputable instance preNormedAlgebra : NormedAlgebra ℂ PreCAR where 241 __ := preAlgebra 242 norm_smul_le := preNormedSpace.norm_smul_le 243 244noncomputable instance preCStarRing : CStarRing PreCAR where 245 norm_mul_self_le x := by 246 obtain ⟨n, a, b, ha, _⟩ := exists_common_stage x x 247 rw [← ha] 248 simpa only [← map_star, ← map_mul, norm_stageHom] using 249 (CStarRing.norm_mul_self_le a) 250 251noncomputable instance preSeparableSpace : TopologicalSpace.SeparableSpace PreCAR := 252 Metric.separableSpaceInductiveLimit_of_separableSpace isometry_stage 253 254theorem dense_stageUnion : Dense (⋃ n, Set.range (stageHom n)) := by 255 let current : MetricSpace PreCAR := inferInstance 256 let original : MetricSpace PreCAR := Metric.instMetricSpaceInductiveLimit 257 have hmetric : current = original := MetricSpace.ext (by rfl) 258 change @Dense PreCAR current.toUniformSpace.toTopologicalSpace 259 (⋃ n, Set.range (stageHom n)) 260 rw [hmetric] 261 have hrange (n : ℕ) : Set.range (stageHom n) = 262 Set.range (Metric.toInductiveLimit isometry_stage n) := by 263 ext y 264 constructor <;> rintro ⟨x, rfl⟩ 265 · exact ⟨x, stageHom_apply n x⟩ 266 · exact ⟨x, (stageHom_apply n x).symm⟩ 267 rw [show (⋃ n, Set.range (stageHom n)) = 268 ⋃ n, Set.range (Metric.toInductiveLimit isometry_stage n) by 269 apply congrArg (fun f : ℕ → Set PreCAR => ⋃ n, f n) 270 funext n 271 exact hrange n] 272 exact Metric.dense_iUnion_range_toInductiveLimit isometry_stage 273 274noncomputable instance preNontrivial : Nontrivial PreCAR := 275 ⟨⟨stageHom 0 0, stageHom 0 1, fun h => zero_ne_one (stageHom_injective 0 h)⟩⟩ 276 277/-- The norm completion of the binary matrix-stage union. -/ 278abbrev Limit := UniformSpace.Completion PreCAR 279 280private theorem limit_norm_smul_le (c : ℂ) (x : Limit) : 281 ‖c • x‖ ≤ ‖c‖ * ‖x‖ := norm_smul_le c x 282 283noncomputable instance limitNormedAlgebra : NormedAlgebra ℂ Limit where 284 toAlgebra := (inferInstance : Algebra ℂ Limit) 285 norm_smul_le := limit_norm_smul_le 286 287noncomputable instance limitStar : Star Limit where 288 star x := UniformSpace.Completion.map (star : PreCAR → PreCAR) x 289 290@[simp] 291theorem star_coe (x : PreCAR) : star (x : Limit) = (star x : PreCAR) := 292 UniformSpace.Completion.map_coe star_isometry.uniformContinuous x 293 294theorem continuous_limit_star : Continuous (star : Limit → Limit) := 295 UniformSpace.Completion.continuous_map 296 297noncomputable instance limitContinuousStar : ContinuousStar Limit := 298 ⟨continuous_limit_star⟩ 299 300noncomputable instance limitStarRing : StarRing Limit where 301 star_involutive x := by 302 refine UniformSpace.Completion.induction_on (α := PreCAR) 303 (p := fun x => star (star x) = x) x ?_ ?_ 304 · apply isClosed_eq <;> fun_prop 305 · intro a 306 simp only [star_coe, star_star] 307 star_add x y := by 308 refine UniformSpace.Completion.induction_on₂ (α := PreCAR) (β := PreCAR) 309 (p := fun x y => star (x + y) = star x + star y) x y ?_ ?_ 310 · apply isClosed_eq <;> fun_prop 311 · intro a b 312 simp only [← UniformSpace.Completion.coe_add, star_coe, star_add] 313 star_mul x y := by 314 refine UniformSpace.Completion.induction_on₂ (α := PreCAR) (β := PreCAR) 315 (p := fun x y => star (x * y) = star y * star x) x y ?_ ?_ 316 · apply isClosed_eq <;> fun_prop 317 · intro a b 318 simp only [← UniformSpace.Completion.coe_mul, star_coe, star_mul] 319 320noncomputable instance limitStarModule : StarModule ℂ Limit where 321 star_smul c x := by 322 refine UniformSpace.Completion.induction_on (α := PreCAR) 323 (p := fun x => star (c • x) = star c • star x) x ?_ ?_ 324 · exact isClosed_eq 325 (continuous_limit_star.comp (continuous_const_smul c)) 326 ((continuous_const_smul (star c)).comp continuous_limit_star) 327 · intro a 328 simp only [← UniformSpace.Completion.coe_smul, star_coe, star_smul] 329 330noncomputable instance limitCStarRing : CStarRing Limit where 331 norm_mul_self_le x := by 332 refine UniformSpace.Completion.induction_on (α := PreCAR) 333 (p := fun x => ‖x‖ * ‖x‖ ≤ ‖star x * x‖) x ?_ ?_ 334 · exact isClosed_le (continuous_norm.mul continuous_norm) 335 (continuous_norm.comp (continuous_limit_star.mul continuous_id)) 336 · intro a 337 simpa only [← UniformSpace.Completion.coe_mul, star_coe, 338 UniformSpace.Completion.norm_coe] using CStarRing.norm_mul_self_le a 339 340noncomputable instance limitCStarAlgebra : CStarAlgebra Limit where 341 toNormedRing := (inferInstance : NormedRing Limit) 342 toStarRing := limitStarRing 343 toCompleteSpace := (inferInstance : CompleteSpace Limit) 344 toCStarRing := limitCStarRing 345 toNormedAlgebra := limitNormedAlgebra 346 toStarModule := limitStarModule 347 348noncomputable instance limitPartialOrder : PartialOrder Limit := 349 CStarAlgebra.spectralOrder Limit 350 351noncomputable instance limitStarOrderedRing : StarOrderedRing Limit := 352 CStarAlgebra.spectralOrderedRing Limit 353 354noncomputable instance limitNontrivial : Nontrivial Limit := 355 ⟨⟨((0 : PreCAR) : Limit), ((1 : PreCAR) : Limit), fun h => 356 zero_ne_one (UniformSpace.Completion.coe_injective PreCAR h)⟩⟩ 357 358/-- The canonical dense star-algebra map into the completion. -/ 359noncomputable def toLimit : PreCAR →⋆ₐ[ℂ] Limit where 360 toFun x := (x : Limit) 361 map_one' := UniformSpace.Completion.coe_one PreCAR 362 map_mul' := UniformSpace.Completion.coe_mul 363 map_zero' := UniformSpace.Completion.coe_zero 364 map_add' := UniformSpace.Completion.coe_add 365 commutes' _ := rfl 366 map_star' x := (star_coe x).symm 367 368/-- The compatible isometric embedding of the `n`-th matrix stage into the completed CAR algebra. -/ 369noncomputable def ofStage (n : ℕ) : Stage n →⋆ₐ[ℂ] Limit := 370 toLimit.comp (stageHom n) 371 372@[simp] 373theorem ofStage_apply (n : ℕ) (x : Stage n) : 374 ofStage n x = (stageHom n x : Limit) := rfl 375 376@[simp] 377theorem norm_ofStage (n : ℕ) (x : Stage n) : ‖ofStage n x‖ = ‖x‖ := by 378 rw [ofStage_apply, UniformSpace.Completion.norm_coe, norm_stageHom] 379 380theorem ofStage_injective (n : ℕ) : Function.Injective (ofStage n) := 381 AddMonoidHomClass.isometry_of_norm (ofStage n) (norm_ofStage n) |>.injective 382 383@[simp] 384theorem ofStage_step (n : ℕ) (x : Stage n) : 385 ofStage (n + 1) (step n x) = ofStage n x := by 386 simp only [ofStage_apply, stageHom_apply, toPreCAR_step] 387 388theorem dense_stageRange : Dense (⋃ n, Set.range (ofStage n)) := by 389 let U : Set PreCAR := ⋃ n, Set.range (stageHom n) 390 let V : Set Limit := ⋃ n, Set.range (ofStage n) 391 have himage : ((fun x : PreCAR => (x : Limit)) '' U) ⊆ V := by 392 rintro _ ⟨x, hx, rfl⟩ 393 rcases Set.mem_iUnion.mp hx with ⟨n, hn⟩ 394 rcases hn with ⟨a, rfl⟩ 395 exact Set.mem_iUnion.2 ⟨n, ⟨a, rfl⟩⟩ 396 have hrange : Set.range (fun x : PreCAR => (x : Limit)) ⊆ closure V := 397 let hcont : Continuous (fun x : PreCAR => (x : Limit)) := 398 UniformSpace.Completion.continuous_coe PreCAR 399 (hcont.range_subset_closure_image_dense dense_stageUnion).trans (closure_mono himage) 400 exact Dense.of_closure (UniformSpace.Completion.denseRange_coe.mono hrange) 401 402noncomputable instance limitSeparableSpace : TopologicalSpace.SeparableSpace Limit := 403 UniformSpace.Completion.separableSpace_completion 404 405theorem finrank_stage (n : ℕ) : 406 Module.finrank ℂ (Stage n) = (2 ^ n) * (2 ^ n) := by 407 change Module.finrank ℂ (Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ) = _ 408 rw [Module.finrank_matrix] 409 simp 410 411theorem not_finiteDimensional : ¬ FiniteDimensional ℂ Limit := by 412 intro hfinite 413 let k := Module.finrank ℂ Limit 414 let n := k + 1 415 have hle : Module.finrank ℂ (Stage n) ≤ k := 416 (ofStage n).toLinearMap.finrank_le_finrank_of_injective (ofStage_injective n) 417 have hkpow : k < 2 ^ n := by 418 exact (Nat.lt_succ_self k).trans n.lt_two_pow_self 419 have hpowsq : 2 ^ n ≤ (2 ^ n) * (2 ^ n) := 420 Nat.le_mul_of_pos_right _ (Nat.pow_pos (by decide : 0 < 2)) 421 rw [finrank_stage] at hle 422 exact (Nat.not_lt_of_ge hle) (hkpow.trans_le hpowsq) 423 424@[simp] 425theorem rootFunctional_embed (n : ℕ) : ∀ (m : ℕ) (h : n ≤ m) (x : Stage n), 426 rootFunctional m (embed n m h x) = rootFunctional n x := by 427 apply Nat.le_induction 428 · intro x 429 rw [embed_refl] 430 rfl 431 · intro m h ih x 432 rw [embed_succ, StarAlgHom.comp_apply, rootFunctional_step, ih] 433 exact h 434 435/-- The compatible root-coordinate functional on the algebraic stage union. -/ 436noncomputable def algRootLinear : AlgCAR →ₗ[ℂ] ℂ := 437 DirectLimit.Module.lift ℂ ℕ Stage (fun _ _ h => embed _ _ h) 438 (fun n => (rootFunctional n).toLinearMap) 439 (fun i j hij x => rootFunctional_embed i j hij x) 440 441@[simp] 442theorem algRootLinear_stage (n : ℕ) (x : Stage n) : 443 algRootLinear (algStageHom n x) = rootFunctional n x := rfl 444 445/-- The root-coordinate functional on the normed stage union. -/ 446noncomputable def preRootLinear : PreCAR →ₗ[ℂ] ℂ := 447 algRootLinear.comp preStarAlgEquiv.toAlgEquiv.toLinearEquiv.toLinearMap 448 449@[simp] 450theorem preRootLinear_stage (n : ℕ) (x : Stage n) : 451 preRootLinear (stageHom n x) = rootFunctional n x := rfl 452 453theorem norm_preRootLinear_le (x : PreCAR) : ‖preRootLinear x‖ ≤ ‖x‖ := by 454 obtain ⟨n, a, b, ha, _⟩ := exists_common_stage x x 455 rw [← ha, preRootLinear_stage, norm_stageHom] 456 simpa [rootFunctional_apply] using 457 (CStarMatrix.norm_entry_le_norm (M := a) (i := (0 : Fin (2 ^ n))) 458 (j := (0 : Fin (2 ^ n)))) 459 460/-- The bounded root-coordinate functional before completion. -/ 461noncomputable def preRootFunctional : PreCAR →L[ℂ] ℂ := 462 preRootLinear.mkContinuous 1 fun x => by simpa using norm_preRootLinear_le x 463 464@[simp] 465theorem preRootFunctional_stage (n : ℕ) (x : Stage n) : 466 preRootFunctional (stageHom n x) = rootFunctional n x := rfl 467 468/-- The product-vector state candidate on the completed CAR algebra. -/ 469noncomputable def rootState : Limit →L[ℂ] ℂ := 470 preRootFunctional.extend (UniformSpace.Completion.toComplL : PreCAR →L[ℂ] Limit) 471 472@[simp] 473theorem rootState_coe (x : PreCAR) : rootState (x : Limit) = preRootFunctional x := by 474 exact ContinuousLinearMap.extend_eq preRootFunctional 475 UniformSpace.Completion.denseRange_coe 476 (UniformSpace.Completion.isUniformInducing_coe PreCAR) x 477 478@[simp] 479theorem rootState_stage (n : ℕ) (x : Stage n) : 480 rootState (ofStage n x) = rootFunctional n x := by 481 rw [ofStage_apply, rootState_coe, preRootFunctional_stage] 482 483theorem preRootFunctional_star_mul_self_nonneg (x : PreCAR) : 484 0 ≤ preRootFunctional (star x * x) := by 485 obtain ⟨n, a, b, ha, _⟩ := exists_common_stage x x 486 rw [← ha, ← map_star, ← map_mul, preRootFunctional_stage] 487 exact rootLinear_nonneg n (star a * a) (star_mul_self_nonneg a) 488 489theorem rootState_star_mul_self_nonneg (x : Limit) : 490 0 ≤ rootState (star x * x) := by 491 refine UniformSpace.Completion.induction_on (α := PreCAR) 492 (p := fun x => 0 ≤ rootState (star x * x)) x ?_ ?_ 493 · exact isClosed_le continuous_const 494 (rootState.continuous.comp (continuous_limit_star.mul continuous_id)) 495 · intro a 496 simpa only [← UniformSpace.Completion.coe_mul, star_coe, rootState_coe] using 497 preRootFunctional_star_mul_self_nonneg a 498 499theorem rootState_nonneg (x : Limit) (hx : 0 ≤ x) : 0 ≤ rootState x := by 500 rcases CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx with ⟨y, rfl⟩ 501 exact rootState_star_mul_self_nonneg y 502 503@[simp] 504theorem rootState_one : rootState (1 : Limit) = 1 := by 505 have hone : ofStage 0 (1 : Stage 0) = (1 : Limit) := map_one (ofStage 0) 506 rw [← hone, rootState_stage] 507 exact rootPositiveFunctional_one 0 508 509theorem rootState_mem_stateSpace : rootState ∈ MathlibAnnex.CStarAlgebra.stateSpace Limit := 510 ⟨rootState_nonneg, rootState_one⟩ 511 512/-- Restriction of a continuous functional to a finite stage. -/ 513noncomputable def restrictState (n : ℕ) (phi : Limit →L[ℂ] ℂ) : Stage n →L[ℂ] ℂ := 514 phi.comp ((ofStage n).toLinearMap.mkContinuous 1 fun x => by 515 simpa using (le_of_eq (norm_ofStage n x))) 516 517@[simp] 518theorem restrictState_apply (n : ℕ) (phi : Limit →L[ℂ] ℂ) (x : Stage n) : 519 restrictState n phi x = phi (ofStage n x) := rfl 520 521theorem restrictState_mem_stateSpace (n : ℕ) (phi : Limit →L[ℂ] ℂ) 522 (hphi : phi ∈ MathlibAnnex.CStarAlgebra.stateSpace Limit) : 523 restrictState n phi ∈ MathlibAnnex.CStarAlgebra.stateSpace (Stage n) := by 524 constructor 525 · intro x hx 526 letI : NonnegSpectrumClass ℝ (Stage n) := 527 CStarAlgebra.instNonnegSpectrumClass' 528 letI : NonUnitalContinuousFunctionalCalculus ℂ (Stage n) IsStarNormal := 529 (IsStarNormal.instNonUnitalContinuousFunctionalCalculus 530 (A := Stage n)).toNonUnitalContinuousFunctionalCalculus 531 letI : NonUnitalContinuousFunctionalCalculus ℝ (Stage n) IsSelfAdjoint := 532 IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus 533 rcases CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx with ⟨y, rfl⟩ 534 change 0 ≤ phi (ofStage n (star y * y)) 535 apply hphi.1 536 simpa only [map_mul, map_star] using star_mul_self_nonneg (ofStage n y) 537 · rw [restrictState_apply, map_one, hphi.2] 538 539theorem eq_rootState_of_restrict (phi : Limit →L[ℂ] ℂ) 540 (hphi : ∀ n, restrictState n phi = rootFunctional n) : phi = rootState := by 541 apply ContinuousLinearMap.coeFn_injective 542 exact phi.continuous.ext_on dense_stageRange rootState.continuous fun x hx => by 543 rcases Set.mem_iUnion.mp hx with ⟨n, hn⟩ 544 rcases hn with ⟨a, rfl⟩ 545 calc 546 phi (ofStage n a) = restrictState n phi a := rfl 547 _ = rootFunctional n a := DFunLike.congr_fun (hphi n) a 548 _ = rootState (ofStage n a) := (rootState_stage n a).symm 549 550/-- The completed product-vector state is pure, proved from its pure finite restrictions. -/ 551theorem isPureState_rootState : MathlibAnnex.CStarAlgebra.IsPureState Limit rootState := by 552 rw [MathlibAnnex.CStarAlgebra.IsPureState, mem_extremePoints_iff_left] 553 refine ⟨rootState_mem_stateSpace, ?_⟩ 554 intro phi₁ hphi₁ phi₂ hphi₂ hsegment 555 rcases hsegment with ⟨a, b, ha, hb, hab, hcomb⟩ 556 apply eq_rootState_of_restrict phi₁ 557 intro n 558 have hcomb_n : a • restrictState n phi₁ + b • restrictState n phi₂ = 559 rootFunctional n := by 560 apply ContinuousLinearMap.ext 561 intro x 562 have hx := congrArg (fun psi : Limit →L[ℂ] ℂ => psi (ofStage n x)) hcomb 563 calc 564 (a • restrictState n phi₁ + b • restrictState n phi₂) x = 565 (a • phi₁ + b • phi₂) (ofStage n x) := rfl 566 _ = rootState (ofStage n x) := hx 567 _ = rootFunctional n x := rootState_stage n x 568 have hpure := isPureState_rootFunctional n 569 rw [MathlibAnnex.CStarAlgebra.IsPureState, mem_extremePoints_iff_left] at hpure 570 exact hpure.2 (restrictState n phi₁) 571 (restrictState_mem_stateSpace n phi₁ hphi₁) 572 (restrictState n phi₂) (restrictState_mem_stateSpace n phi₂ hphi₂) 573 ⟨a, b, ha, hb, hab, hcomb_n⟩ 574 575theorem step_rootProjection_mul (n : ℕ) : 576 step n (rootProjection n) * rootProjection (n + 1) = rootProjection (n + 1) := by 577 let p := rootProjection (n + 1) 578 let q := step n (rootProjection n) 579 have hp : IsStarProjection p := isStarProjection_rootProjection (n + 1) 580 have hq : IsStarProjection q := (isStarProjection_rootProjection n).map (step n) 581 have hentry : rootFunctional (n + 1) q = 1 := by 582 change rootFunctional (n + 1) (step n (rootProjection n)) = 1 583 rw [rootFunctional_step, rootFunctional_apply] 584 simp [rootProjection] 585 have hsand : p * q * p = p := by 586 calc 587 p * q * p = rootFunctional (n + 1) q • p := rootProjection_mul_mul (n + 1) q 588 _ = p := by rw [hentry, one_smul] 589 have hz : star (q * p - p) * (q * p - p) = 0 := by 590 rw [star_sub, star_mul, hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] 591 noncomm_ring [hp.isIdempotentElem.eq, hsand] 592 rw [← mul_assoc q q p, hq.isIdempotentElem.eq] 593 simp 594 exact sub_eq_zero.mp ((CStarRing.star_mul_self_eq_zero_iff _).mp hz) 595 596/-- The common root flag in the completed CAR algebra. -/ 597noncomputable def rootFlag (n : ℕ) : Limit := 598 ofStage n (rootProjection n) 599 600@[simp] 601theorem rootFlag_zero : rootFlag 0 = 1 := by 602 rw [rootFlag] 603 have hp : rootProjection 0 = (1 : Stage 0) := by 604 apply CStarMatrix.ext 605 intro i j 606 fin_cases i 607 fin_cases j 608 simp [rootProjection] 609 rw [hp, map_one] 610 611theorem isStarProjection_rootFlag (n : ℕ) : IsStarProjection (rootFlag n) := 612 (isStarProjection_rootProjection n).map (ofStage n) 613 614@[simp] 615theorem rootState_rootFlag (n : ℕ) : rootState (rootFlag n) = 1 := by 616 rw [rootFlag, rootState_stage, rootFunctional_apply] 617 simp [rootProjection] 618 619theorem rootFlag_succ_le (n : ℕ) : rootFlag (n + 1) ≤ rootFlag n := by 620 apply (isStarProjection_rootFlag (n + 1)).le_iff_mul_eq_right 621 (isStarProjection_rootFlag n) |>.2 622 change ofStage n (rootProjection n) * ofStage (n + 1) (rootProjection (n + 1)) = 623 ofStage (n + 1) (rootProjection (n + 1)) 624 rw [← ofStage_step n (rootProjection n), ← map_mul] 625 exact congrArg (ofStage (n + 1)) (step_rootProjection_mul n) 626 627theorem antitone_rootFlag : Antitone rootFlag := 628 antitone_nat_of_succ_le rootFlag_succ_le 629 630@[simp] 631theorem ofStage_embed (n m : ℕ) (h : n ≤ m) (x : Stage n) : 632 ofStage m (embed n m h x) = ofStage n x := by 633 simp only [ofStage_apply, stageHom_apply, toPreCAR_embed] 634 635/-- Every finite-stage element has exact root compression at every later flag projection. -/ 636theorem rootFlag_mul_ofStage_mul (m n : ℕ) (h : m ≤ n) (x : Stage m) : 637 rootFlag n * ofStage m x * rootFlag n = 638 rootState (ofStage m x) • rootFlag n := by 639 rw [← ofStage_embed m n h x] 640 change ofStage n (rootProjection n) * ofStage n (embed m n h x) * 641 ofStage n (rootProjection n) = 642 rootState (ofStage n (embed m n h x)) • ofStage n (rootProjection n) 643 rw [← map_mul, ← map_mul, rootProjection_mul_mul, map_smul, 644 rootState_stage] 645 rfl 646 647/-- The norm-valued root-compression error. -/ 648noncomputable def compressionError (n : ℕ) (x : Limit) : Limit := 649 rootFlag n * x * rootFlag n - rootState x • rootFlag n 650 651theorem compressionError_sub (n : ℕ) (x y : Limit) : 652 compressionError n x - compressionError n y = compressionError n (x - y) := by 653 simp only [compressionError, map_sub, sub_smul] 654 noncomm_ring 655 656theorem norm_compressionError_le (n : ℕ) (x : Limit) : 657 ‖compressionError n x‖ ≤ (1 + ‖rootState‖) * ‖x‖ := by 658 have hq := (isStarProjection_rootFlag n).norm_le 659 have hleft : ‖rootFlag n * x * rootFlag n‖ ≤ ‖x‖ := by 660 calc 661 ‖rootFlag n * x * rootFlag n‖ ≤ ‖rootFlag n‖ * ‖x‖ * ‖rootFlag n‖ := by 662 exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right (norm_mul_le _ _) 663 (norm_nonneg _)) 664 _ ≤ 1 * ‖x‖ * 1 := by gcongr 665 _ = ‖x‖ := by ring 666 have hright : ‖rootState x • rootFlag n‖ ≤ ‖rootState‖ * ‖x‖ := by 667 rw [norm_smul] 668 calc 669 ‖rootState x‖ * ‖rootFlag n‖ ≤ (‖rootState‖ * ‖x‖) * 1 := by 670 gcongr 671 exact rootState.le_opNorm x 672 _ = ‖rootState‖ * ‖x‖ := mul_one _ 673 calc 674 ‖compressionError n x‖ ≤ 675 ‖rootFlag n * x * rootFlag n‖ + ‖rootState x • rootFlag n‖ := norm_sub_le _ _ 676 _ ≤ ‖x‖ + ‖rootState‖ * ‖x‖ := add_le_add hleft hright 677 _ = (1 + ‖rootState‖) * ‖x‖ := by ring 678 679theorem compressionError_ofStage (m n : ℕ) (h : m ≤ n) (x : Stage m) : 680 compressionError n (ofStage m x) = 0 := by 681 rw [compressionError, rootFlag_mul_ofStage_mul m n h x, sub_self] 682 683/-- Root compression converges in norm for every element of the completed CAR algebra. -/ 684theorem tendsto_norm_compressionError (x : Limit) : 685 Filter.Tendsto (fun n => ‖compressionError n x‖) Filter.atTop (nhds 0) := by 686 rw [Metric.tendsto_atTop] 687 intro ε hε 688 have hden : 0 < ‖rootState‖ + 2 := by positivity 689 obtain ⟨y, hy, hyx⟩ := dense_stageRange.exists_dist_lt x (div_pos hε hden) 690 rcases Set.mem_iUnion.mp hy with ⟨m, hm⟩ 691 rcases hm with ⟨a, rfl⟩ 692 refine ⟨m, fun n hn => ?_⟩ 693 have hzero : compressionError n (ofStage m a) = 0 := 694 compressionError_ofStage m n hn a 695 have hdist : ‖x - ofStage m a‖ < ε / (‖rootState‖ + 2) := by 696 simpa only [dist_eq_norm, norm_sub_rev] using hyx 697 have hlarge : (‖rootState‖ + 2) * ‖x - ofStage m a‖ < ε := by 698 rw [mul_comm] 699 exact (lt_div_iff₀ hden).mp hdist 700 have hcoeff : 1 + ‖rootState‖ ≤ ‖rootState‖ + 2 := by linarith 701 have herr : ‖compressionError n x‖ < ε := by 702 calc 703 ‖compressionError n x‖ = 704 ‖compressionError n x - compressionError n (ofStage m a)‖ := by rw [hzero, sub_zero] 705 _ = ‖compressionError n (x - ofStage m a)‖ := by rw [compressionError_sub] 706 _ ≤ (1 + ‖rootState‖) * ‖x - ofStage m a‖ := norm_compressionError_le n _ 707 _ ≤ (‖rootState‖ + 2) * ‖x - ofStage m a‖ := by 708 gcongr 709 _ < ε := hlarge 710 simpa [Real.dist_eq, abs_of_nonneg (norm_nonneg _)] using herr 711 712end MathlibAnnex.CStarAlgebra.CAR