Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Completion.lean
Pinned GitHub source · Raw UTF-8 source
Back to An irreducible CAR representation has no nonzero compact image · Back to The completed CAR algebra is infinite-dimensional · Back to The shell-generated algebra is not an algebra of all compact operators
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.PureRoot2import Mathlib.Algebra.Colimit.DirectLimit3import Mathlib.Topology.MetricSpace.Gluing4import Mathlib.Algebra.Star.TransferInstance5import Mathlib.Algebra.Algebra.TransferInstance6import Mathlib.Analysis.Normed.Module.Completion7import Mathlib.Analysis.Normed.Operator.Extend8import Mathlib.Analysis.CStarAlgebra.Projection910set_option autoImplicit false1112open scoped ComplexOrder13open Set1415namespace MathlibAnnex.CStarAlgebra.CAR1617/-- 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))2021@[simp]22theorem embed_refl (n : ℕ) : embed n n le_rfl = StarAlgHom.id ℂ (Stage n) := by23 unfold embed24 exact Nat.leRecOn_self _2526@[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) := by29 unfold embed30 exact Nat.leRecOn_succ h _3132@[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 := by35 apply Nat.le_induction36 · intro x37 rw [embed_refl]38 exact (Nat.leRecOn_self x).symm39 · intro m h ih x40 rw [embed_succ, StarAlgHom.comp_apply, ih, Nat.leRecOn_succ h]41 exact h4243theorem 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) := by45 apply StarAlgHom.ext46 intro x47 simp only [StarAlgHom.comp_apply, embed_apply]48 exact Nat.leRecOn_trans hij hjk x4950noncomputable instance embedDirectedSystem :51 DirectedSystem Stage (fun _ _ h => embed _ _ h) where52 map_self {i} x := by rw [embed_refl]; rfl53 map_map {k j i} hij hjk x := by rw [← StarAlgHom.comp_apply, ← embed_trans]5455/-- The algebraic union of all binary matrix stages. -/56abbrev AlgCAR := DirectLimit Stage (fun _ _ h => embed _ _ h)5758theorem norm_embed (n : ℕ) : ∀ (m : ℕ) (h : n ≤ m) (x : Stage n),59 ‖embed n m h x‖ = ‖x‖ := by60 apply Nat.le_induction61 · intro x62 rw [embed_refl]63 rfl64 · intro m h ih x65 rw [embed_succ, StarAlgHom.comp_apply, norm_step, ih]66 exact h6768theorem embed_injective (n m : ℕ) (h : n ≤ m) : Function.Injective (embed n m h) :=69 fun x y hxy => by70 rw [← sub_eq_zero, ← norm_eq_zero, ← norm_embed n m h]71 simp only [map_sub, hxy, sub_self, norm_zero]7273theorem isometry_step (n : ℕ) : Isometry (step n) :=74 AddMonoidHomClass.isometry_of_norm (step n) (norm_step n)7576theorem isometry_stage : ∀ n, Isometry (fun x : Stage n => step n x) :=77 isometry_step7879/-- The metric union of the finite CAR stages. -/80abbrev PreCAR := Metric.InductiveLimit isometry_stage8182/-- The finite-stage map into the metric union. -/83noncomputable def toPreCAR (n : ℕ) : Stage n → PreCAR :=84 Metric.toInductiveLimit isometry_stage n8586theorem isometry_toPreCAR (n : ℕ) : Isometry (toPreCAR n) :=87 Metric.toInductiveLimit_isometry isometry_stage n8889@[simp]90theorem toPreCAR_step (n : ℕ) (x : Stage n) :91 toPreCAR (n + 1) (step n x) = toPreCAR n x := by92 exact congrFun (Metric.toInductiveLimit_commute isometry_stage n) x9394theorem toPreCAR_embed (n : ℕ) : ∀ (m : ℕ) (h : n ≤ m) (x : Stage n),95 toPreCAR m (embed n m h x) = toPreCAR n x := by96 apply Nat.le_induction97 · intro x98 rw [embed_refl]99 rfl100 · intro m h ih x101 rw [embed_succ, StarAlgHom.comp_apply, toPreCAR_step, ih]102 exact h103104private theorem alg_compatible (x y : Σ n, Stage n)105 (hxy : @Inseparable _ (Metric.inductivePremetric isometry_stage).toUniformSpace.toTopologicalSpace106 x y) :107 (⟦x⟧ : AlgCAR) = ⟦y⟧ := by108 let m := max x.1 y.1109 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 hxy113 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 := by115 rw [← Metric.inductiveLimitDist_eq_dist isometry_stage x y m hx hy]116 exact hdist117 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 hd119 apply Quotient.sound120 exact ⟨m, hx, hy, by simpa only [embed_apply] using he⟩121122/-- Forget the metric presentation of the union. -/123noncomputable def preToAlg : PreCAR → AlgCAR :=124 @SeparationQuotient.lift _ _125 (Metric.inductivePremetric isometry_stage).toUniformSpace.toTopologicalSpace126 (fun x => (⟦x⟧ : AlgCAR)) alg_compatible127128@[simp]129theorem preToAlg_toPreCAR (n : ℕ) (x : Stage n) :130 preToAlg (toPreCAR n x) = (⟦⟨n, x⟩⟧ : AlgCAR) := by131 rfl132133/-- 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)137138@[simp]139theorem algToPre_mk (n : ℕ) (x : Stage n) :140 algToPre (⟦⟨n, x⟩⟧ : AlgCAR) = toPreCAR n x := rfl141142theorem algToPre_preToAlg (x : PreCAR) : algToPre (preToAlg x) = x := by143 obtain ⟨⟨n, y⟩, rfl⟩ := Quotient.exists_rep x144 rfl145146theorem preToAlg_algToPre (x : AlgCAR) : preToAlg (algToPre x) = x := by147 obtain ⟨⟨n, y⟩, rfl⟩ := Quotient.exists_rep x148 rfl149150/-- Algebraic and metric presentations of the stage union coincide. -/151noncomputable def preAlgEquiv : PreCAR ≃ AlgCAR where152 toFun := preToAlg153 invFun := algToPre154 left_inv := algToPre_preToAlg155 right_inv := preToAlg_algToPre156157noncomputable instance preRing : Ring PreCAR := preAlgEquiv.ring158159noncomputable instance preAlgebra : Algebra ℂ PreCAR := Equiv.algebra ℂ preAlgEquiv160161noncomputable instance preStarRing : StarRing PreCAR := preAlgEquiv.starRing162163noncomputable instance preStarModule : StarModule ℂ PreCAR := preAlgEquiv.starModule ℂ164165/-- The equivalence between metric and algebraic unions respects all star-algebra operations. -/166noncomputable def preStarAlgEquiv : PreCAR ≃⋆ₐ[ℂ] AlgCAR where167 __ := Equiv.ringEquiv preAlgEquiv168 map_star' x := by169 change preToAlg (algToPre (star (preToAlg x))) = star (preToAlg x)170 exact preToAlg_algToPre _171 map_smul' r x := by172 simp [Equiv.smul_def]173174/-- The canonical algebraic map of a finite stage into the algebraic union. -/175noncomputable def algStageHom (n : ℕ) : Stage n →⋆ₐ[ℂ] AlgCAR where176 __ := DirectLimit.Algebra.of Stage (fun _ _ h => embed _ _ h) n177 map_star' _ := rfl178179/-- 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)182183@[simp]184theorem stageHom_apply (n : ℕ) (x : Stage n) : stageHom n x = toPreCAR n x := by185 apply preAlgEquiv.injective186 rfl187188theorem stageHom_injective (n : ℕ) : Function.Injective (stageHom n) :=189 fun x y h => (isometry_toPreCAR n).injective <| by simpa only [← stageHom_apply] using h190191theorem exists_common_stage (x y : PreCAR) :192 ∃ n, ∃ a b : Stage n, stageHom n a = x ∧ stageHom n b = y := by193 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.injective197 exact ha.symm198 · apply preAlgEquiv.injective199 exact hb.symm200201noncomputable instance preNorm : Norm PreCAR where202 norm x := dist x 0203204@[simp]205theorem norm_stageHom (n : ℕ) (x : Stage n) : ‖stageHom n x‖ = ‖x‖ := by206 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 x210211noncomputable instance preNormedAddCommGroup : NormedAddCommGroup PreCAR where212 toNorm := preNorm213 toAddCommGroup := preRing.toAddCommGroup214 toMetricSpace := Metric.instMetricSpaceInductiveLimit215 dist_eq x y := by216 obtain ⟨n, a, b, rfl, rfl⟩ := exists_common_stage x y217 rw [← map_neg, ← map_add, norm_stageHom]218 calc219 dist ((stageHom n) a) ((stageHom n) b) = dist a b := by220 simpa only [stageHom_apply] using (isometry_toPreCAR n).dist_eq a b221 _ = ‖-a + b‖ := NormedAddGroup.dist_eq a b222223noncomputable instance preNormedRing : NormedRing PreCAR where224 __ := preNormedAddCommGroup225 __ := preRing226 norm_mul_le x y := by227 obtain ⟨n, a, b, rfl, rfl⟩ := exists_common_stage x y228 simpa only [← map_mul, norm_stageHom] using norm_mul_le a b229230noncomputable instance preNormedSpace : NormedSpace ℂ PreCAR where231 norm_smul_le c x := by232 obtain ⟨n, a, b, ha, _⟩ := exists_common_stage x x233 rw [← ha]234 calc235 ‖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 a238 _ = ‖c‖ * ‖stageHom n a‖ := by rw [norm_stageHom]239240noncomputable instance preNormedAlgebra : NormedAlgebra ℂ PreCAR where241 __ := preAlgebra242 norm_smul_le := preNormedSpace.norm_smul_le243244noncomputable instance preCStarRing : CStarRing PreCAR where245 norm_mul_self_le x := by246 obtain ⟨n, a, b, ha, _⟩ := exists_common_stage x x247 rw [← ha]248 simpa only [← map_star, ← map_mul, norm_stageHom] using249 (CStarRing.norm_mul_self_le a)250251noncomputable instance preSeparableSpace : TopologicalSpace.SeparableSpace PreCAR :=252 Metric.separableSpaceInductiveLimit_of_separableSpace isometry_stage253254theorem dense_stageUnion : Dense (⋃ n, Set.range (stageHom n)) := by255 let current : MetricSpace PreCAR := inferInstance256 let original : MetricSpace PreCAR := Metric.instMetricSpaceInductiveLimit257 have hmetric : current = original := MetricSpace.ext (by rfl)258 change @Dense PreCAR current.toUniformSpace.toTopologicalSpace259 (⋃ n, Set.range (stageHom n))260 rw [hmetric]261 have hrange (n : ℕ) : Set.range (stageHom n) =262 Set.range (Metric.toInductiveLimit isometry_stage n) := by263 ext y264 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) by269 apply congrArg (fun f : ℕ → Set PreCAR => ⋃ n, f n)270 funext n271 exact hrange n]272 exact Metric.dense_iUnion_range_toInductiveLimit isometry_stage273274noncomputable instance preNontrivial : Nontrivial PreCAR :=275 ⟨⟨stageHom 0 0, stageHom 0 1, fun h => zero_ne_one (stageHom_injective 0 h)⟩⟩276277/-- The norm completion of the binary matrix-stage union. -/278abbrev Limit := UniformSpace.Completion PreCAR279280private theorem limit_norm_smul_le (c : ℂ) (x : Limit) :281 ‖c • x‖ ≤ ‖c‖ * ‖x‖ := norm_smul_le c x282283noncomputable instance limitNormedAlgebra : NormedAlgebra ℂ Limit where284 toAlgebra := (inferInstance : Algebra ℂ Limit)285 norm_smul_le := limit_norm_smul_le286287noncomputable instance limitStar : Star Limit where288 star x := UniformSpace.Completion.map (star : PreCAR → PreCAR) x289290@[simp]291theorem star_coe (x : PreCAR) : star (x : Limit) = (star x : PreCAR) :=292 UniformSpace.Completion.map_coe star_isometry.uniformContinuous x293294theorem continuous_limit_star : Continuous (star : Limit → Limit) :=295 UniformSpace.Completion.continuous_map296297noncomputable instance limitContinuousStar : ContinuousStar Limit :=298 ⟨continuous_limit_star⟩299300noncomputable instance limitStarRing : StarRing Limit where301 star_involutive x := by302 refine UniformSpace.Completion.induction_on (α := PreCAR)303 (p := fun x => star (star x) = x) x ?_ ?_304 · apply isClosed_eq <;> fun_prop305 · intro a306 simp only [star_coe, star_star]307 star_add x y := by308 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_prop311 · intro a b312 simp only [← UniformSpace.Completion.coe_add, star_coe, star_add]313 star_mul x y := by314 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_prop317 · intro a b318 simp only [← UniformSpace.Completion.coe_mul, star_coe, star_mul]319320noncomputable instance limitStarModule : StarModule ℂ Limit where321 star_smul c x := by322 refine UniformSpace.Completion.induction_on (α := PreCAR)323 (p := fun x => star (c • x) = star c • star x) x ?_ ?_324 · exact isClosed_eq325 (continuous_limit_star.comp (continuous_const_smul c))326 ((continuous_const_smul (star c)).comp continuous_limit_star)327 · intro a328 simp only [← UniformSpace.Completion.coe_smul, star_coe, star_smul]329330noncomputable instance limitCStarRing : CStarRing Limit where331 norm_mul_self_le x := by332 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 a337 simpa only [← UniformSpace.Completion.coe_mul, star_coe,338 UniformSpace.Completion.norm_coe] using CStarRing.norm_mul_self_le a339340noncomputable instance limitCStarAlgebra : CStarAlgebra Limit where341 toNormedRing := (inferInstance : NormedRing Limit)342 toStarRing := limitStarRing343 toCompleteSpace := (inferInstance : CompleteSpace Limit)344 toCStarRing := limitCStarRing345 toNormedAlgebra := limitNormedAlgebra346 toStarModule := limitStarModule347348noncomputable instance limitPartialOrder : PartialOrder Limit :=349 CStarAlgebra.spectralOrder Limit350351noncomputable instance limitStarOrderedRing : StarOrderedRing Limit :=352 CStarAlgebra.spectralOrderedRing Limit353354noncomputable instance limitNontrivial : Nontrivial Limit :=355 ⟨⟨((0 : PreCAR) : Limit), ((1 : PreCAR) : Limit), fun h =>356 zero_ne_one (UniformSpace.Completion.coe_injective PreCAR h)⟩⟩357358/-- The canonical dense star-algebra map into the completion. -/359noncomputable def toLimit : PreCAR →⋆ₐ[ℂ] Limit where360 toFun x := (x : Limit)361 map_one' := UniformSpace.Completion.coe_one PreCAR362 map_mul' := UniformSpace.Completion.coe_mul363 map_zero' := UniformSpace.Completion.coe_zero364 map_add' := UniformSpace.Completion.coe_add365 commutes' _ := rfl366 map_star' x := (star_coe x).symm367368/-- 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)371372@[simp]373theorem ofStage_apply (n : ℕ) (x : Stage n) :374 ofStage n x = (stageHom n x : Limit) := rfl375376@[simp]377theorem norm_ofStage (n : ℕ) (x : Stage n) : ‖ofStage n x‖ = ‖x‖ := by378 rw [ofStage_apply, UniformSpace.Completion.norm_coe, norm_stageHom]379380theorem ofStage_injective (n : ℕ) : Function.Injective (ofStage n) :=381 AddMonoidHomClass.isometry_of_norm (ofStage n) (norm_ofStage n) |>.injective382383@[simp]384theorem ofStage_step (n : ℕ) (x : Stage n) :385 ofStage (n + 1) (step n x) = ofStage n x := by386 simp only [ofStage_apply, stageHom_apply, toPreCAR_step]387388theorem dense_stageRange : Dense (⋃ n, Set.range (ofStage n)) := by389 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 := by392 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 PreCAR399 (hcont.range_subset_closure_image_dense dense_stageUnion).trans (closure_mono himage)400 exact Dense.of_closure (UniformSpace.Completion.denseRange_coe.mono hrange)401402noncomputable instance limitSeparableSpace : TopologicalSpace.SeparableSpace Limit :=403 UniformSpace.Completion.separableSpace_completion404405theorem finrank_stage (n : ℕ) :406 Module.finrank ℂ (Stage n) = (2 ^ n) * (2 ^ n) := by407 change Module.finrank ℂ (Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ) = _408 rw [Module.finrank_matrix]409 simp410411theorem not_finiteDimensional : ¬ FiniteDimensional ℂ Limit := by412 intro hfinite413 let k := Module.finrank ℂ Limit414 let n := k + 1415 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 := by418 exact (Nat.lt_succ_self k).trans n.lt_two_pow_self419 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 hle422 exact (Nat.not_lt_of_ge hle) (hkpow.trans_le hpowsq)423424@[simp]425theorem rootFunctional_embed (n : ℕ) : ∀ (m : ℕ) (h : n ≤ m) (x : Stage n),426 rootFunctional m (embed n m h x) = rootFunctional n x := by427 apply Nat.le_induction428 · intro x429 rw [embed_refl]430 rfl431 · intro m h ih x432 rw [embed_succ, StarAlgHom.comp_apply, rootFunctional_step, ih]433 exact h434435/-- 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)440441@[simp]442theorem algRootLinear_stage (n : ℕ) (x : Stage n) :443 algRootLinear (algStageHom n x) = rootFunctional n x := rfl444445/-- The root-coordinate functional on the normed stage union. -/446noncomputable def preRootLinear : PreCAR →ₗ[ℂ] ℂ :=447 algRootLinear.comp preStarAlgEquiv.toAlgEquiv.toLinearEquiv.toLinearMap448449@[simp]450theorem preRootLinear_stage (n : ℕ) (x : Stage n) :451 preRootLinear (stageHom n x) = rootFunctional n x := rfl452453theorem norm_preRootLinear_le (x : PreCAR) : ‖preRootLinear x‖ ≤ ‖x‖ := by454 obtain ⟨n, a, b, ha, _⟩ := exists_common_stage x x455 rw [← ha, preRootLinear_stage, norm_stageHom]456 simpa [rootFunctional_apply] using457 (CStarMatrix.norm_entry_le_norm (M := a) (i := (0 : Fin (2 ^ n)))458 (j := (0 : Fin (2 ^ n))))459460/-- The bounded root-coordinate functional before completion. -/461noncomputable def preRootFunctional : PreCAR →L[ℂ] ℂ :=462 preRootLinear.mkContinuous 1 fun x => by simpa using norm_preRootLinear_le x463464@[simp]465theorem preRootFunctional_stage (n : ℕ) (x : Stage n) :466 preRootFunctional (stageHom n x) = rootFunctional n x := rfl467468/-- The product-vector state candidate on the completed CAR algebra. -/469noncomputable def rootState : Limit →L[ℂ] ℂ :=470 preRootFunctional.extend (UniformSpace.Completion.toComplL : PreCAR →L[ℂ] Limit)471472@[simp]473theorem rootState_coe (x : PreCAR) : rootState (x : Limit) = preRootFunctional x := by474 exact ContinuousLinearMap.extend_eq preRootFunctional475 UniformSpace.Completion.denseRange_coe476 (UniformSpace.Completion.isUniformInducing_coe PreCAR) x477478@[simp]479theorem rootState_stage (n : ℕ) (x : Stage n) :480 rootState (ofStage n x) = rootFunctional n x := by481 rw [ofStage_apply, rootState_coe, preRootFunctional_stage]482483theorem preRootFunctional_star_mul_self_nonneg (x : PreCAR) :484 0 ≤ preRootFunctional (star x * x) := by485 obtain ⟨n, a, b, ha, _⟩ := exists_common_stage x x486 rw [← ha, ← map_star, ← map_mul, preRootFunctional_stage]487 exact rootLinear_nonneg n (star a * a) (star_mul_self_nonneg a)488489theorem rootState_star_mul_self_nonneg (x : Limit) :490 0 ≤ rootState (star x * x) := by491 refine UniformSpace.Completion.induction_on (α := PreCAR)492 (p := fun x => 0 ≤ rootState (star x * x)) x ?_ ?_493 · exact isClosed_le continuous_const494 (rootState.continuous.comp (continuous_limit_star.mul continuous_id))495 · intro a496 simpa only [← UniformSpace.Completion.coe_mul, star_coe, rootState_coe] using497 preRootFunctional_star_mul_self_nonneg a498499theorem rootState_nonneg (x : Limit) (hx : 0 ≤ x) : 0 ≤ rootState x := by500 rcases CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx with ⟨y, rfl⟩501 exact rootState_star_mul_self_nonneg y502503@[simp]504theorem rootState_one : rootState (1 : Limit) = 1 := by505 have hone : ofStage 0 (1 : Stage 0) = (1 : Limit) := map_one (ofStage 0)506 rw [← hone, rootState_stage]507 exact rootPositiveFunctional_one 0508509theorem rootState_mem_stateSpace : rootState ∈ MathlibAnnex.CStarAlgebra.stateSpace Limit :=510 ⟨rootState_nonneg, rootState_one⟩511512/-- 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 => by515 simpa using (le_of_eq (norm_ofStage n x)))516517@[simp]518theorem restrictState_apply (n : ℕ) (phi : Limit →L[ℂ] ℂ) (x : Stage n) :519 restrictState n phi x = phi (ofStage n x) := rfl520521theorem restrictState_mem_stateSpace (n : ℕ) (phi : Limit →L[ℂ] ℂ)522 (hphi : phi ∈ MathlibAnnex.CStarAlgebra.stateSpace Limit) :523 restrictState n phi ∈ MathlibAnnex.CStarAlgebra.stateSpace (Stage n) := by524 constructor525 · intro x hx526 letI : NonnegSpectrumClass ℝ (Stage n) :=527 CStarAlgebra.instNonnegSpectrumClass'528 letI : NonUnitalContinuousFunctionalCalculus ℂ (Stage n) IsStarNormal :=529 (IsStarNormal.instNonUnitalContinuousFunctionalCalculus530 (A := Stage n)).toNonUnitalContinuousFunctionalCalculus531 letI : NonUnitalContinuousFunctionalCalculus ℝ (Stage n) IsSelfAdjoint :=532 IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus533 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.1536 simpa only [map_mul, map_star] using star_mul_self_nonneg (ofStage n y)537 · rw [restrictState_apply, map_one, hphi.2]538539theorem eq_rootState_of_restrict (phi : Limit →L[ℂ] ℂ)540 (hphi : ∀ n, restrictState n phi = rootFunctional n) : phi = rootState := by541 apply ContinuousLinearMap.coeFn_injective542 exact phi.continuous.ext_on dense_stageRange rootState.continuous fun x hx => by543 rcases Set.mem_iUnion.mp hx with ⟨n, hn⟩544 rcases hn with ⟨a, rfl⟩545 calc546 phi (ofStage n a) = restrictState n phi a := rfl547 _ = rootFunctional n a := DFunLike.congr_fun (hphi n) a548 _ = rootState (ofStage n a) := (rootState_stage n a).symm549550/-- The completed product-vector state is pure, proved from its pure finite restrictions. -/551theorem isPureState_rootState : MathlibAnnex.CStarAlgebra.IsPureState Limit rootState := by552 rw [MathlibAnnex.CStarAlgebra.IsPureState, mem_extremePoints_iff_left]553 refine ⟨rootState_mem_stateSpace, ?_⟩554 intro phi₁ hphi₁ phi₂ hphi₂ hsegment555 rcases hsegment with ⟨a, b, ha, hb, hab, hcomb⟩556 apply eq_rootState_of_restrict phi₁557 intro n558 have hcomb_n : a • restrictState n phi₁ + b • restrictState n phi₂ =559 rootFunctional n := by560 apply ContinuousLinearMap.ext561 intro x562 have hx := congrArg (fun psi : Limit →L[ℂ] ℂ => psi (ofStage n x)) hcomb563 calc564 (a • restrictState n phi₁ + b • restrictState n phi₂) x =565 (a • phi₁ + b • phi₂) (ofStage n x) := rfl566 _ = rootState (ofStage n x) := hx567 _ = rootFunctional n x := rootState_stage n x568 have hpure := isPureState_rootFunctional n569 rw [MathlibAnnex.CStarAlgebra.IsPureState, mem_extremePoints_iff_left] at hpure570 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⟩574575theorem step_rootProjection_mul (n : ℕ) :576 step n (rootProjection n) * rootProjection (n + 1) = rootProjection (n + 1) := by577 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 := by582 change rootFunctional (n + 1) (step n (rootProjection n)) = 1583 rw [rootFunctional_step, rootFunctional_apply]584 simp [rootProjection]585 have hsand : p * q * p = p := by586 calc587 p * q * p = rootFunctional (n + 1) q • p := rootProjection_mul_mul (n + 1) q588 _ = p := by rw [hentry, one_smul]589 have hz : star (q * p - p) * (q * p - p) = 0 := by590 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 simp594 exact sub_eq_zero.mp ((CStarRing.star_mul_self_eq_zero_iff _).mp hz)595596/-- The common root flag in the completed CAR algebra. -/597noncomputable def rootFlag (n : ℕ) : Limit :=598 ofStage n (rootProjection n)599600@[simp]601theorem rootFlag_zero : rootFlag 0 = 1 := by602 rw [rootFlag]603 have hp : rootProjection 0 = (1 : Stage 0) := by604 apply CStarMatrix.ext605 intro i j606 fin_cases i607 fin_cases j608 simp [rootProjection]609 rw [hp, map_one]610611theorem isStarProjection_rootFlag (n : ℕ) : IsStarProjection (rootFlag n) :=612 (isStarProjection_rootProjection n).map (ofStage n)613614@[simp]615theorem rootState_rootFlag (n : ℕ) : rootState (rootFlag n) = 1 := by616 rw [rootFlag, rootState_stage, rootFunctional_apply]617 simp [rootProjection]618619theorem rootFlag_succ_le (n : ℕ) : rootFlag (n + 1) ≤ rootFlag n := by620 apply (isStarProjection_rootFlag (n + 1)).le_iff_mul_eq_right621 (isStarProjection_rootFlag n) |>.2622 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)626627theorem antitone_rootFlag : Antitone rootFlag :=628 antitone_nat_of_succ_le rootFlag_succ_le629630@[simp]631theorem ofStage_embed (n m : ℕ) (h : n ≤ m) (x : Stage n) :632 ofStage m (embed n m h x) = ofStage n x := by633 simp only [ofStage_apply, stageHom_apply, toPreCAR_embed]634635/-- 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 := by639 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 rfl646647/-- The norm-valued root-compression error. -/648noncomputable def compressionError (n : ℕ) (x : Limit) : Limit :=649 rootFlag n * x * rootFlag n - rootState x • rootFlag n650651theorem compressionError_sub (n : ℕ) (x y : Limit) :652 compressionError n x - compressionError n y = compressionError n (x - y) := by653 simp only [compressionError, map_sub, sub_smul]654 noncomm_ring655656theorem norm_compressionError_le (n : ℕ) (x : Limit) :657 ‖compressionError n x‖ ≤ (1 + ‖rootState‖) * ‖x‖ := by658 have hq := (isStarProjection_rootFlag n).norm_le659 have hleft : ‖rootFlag n * x * rootFlag n‖ ≤ ‖x‖ := by660 calc661 ‖rootFlag n * x * rootFlag n‖ ≤ ‖rootFlag n‖ * ‖x‖ * ‖rootFlag n‖ := by662 exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right (norm_mul_le _ _)663 (norm_nonneg _))664 _ ≤ 1 * ‖x‖ * 1 := by gcongr665 _ = ‖x‖ := by ring666 have hright : ‖rootState x • rootFlag n‖ ≤ ‖rootState‖ * ‖x‖ := by667 rw [norm_smul]668 calc669 ‖rootState x‖ * ‖rootFlag n‖ ≤ (‖rootState‖ * ‖x‖) * 1 := by670 gcongr671 exact rootState.le_opNorm x672 _ = ‖rootState‖ * ‖x‖ := mul_one _673 calc674 ‖compressionError n x‖ ≤675 ‖rootFlag n * x * rootFlag n‖ + ‖rootState x • rootFlag n‖ := norm_sub_le _ _676 _ ≤ ‖x‖ + ‖rootState‖ * ‖x‖ := add_le_add hleft hright677 _ = (1 + ‖rootState‖) * ‖x‖ := by ring678679theorem compressionError_ofStage (m n : ℕ) (h : m ≤ n) (x : Stage m) :680 compressionError n (ofStage m x) = 0 := by681 rw [compressionError, rootFlag_mul_ofStage_mul m n h x, sub_self]682683/-- 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) := by686 rw [Metric.tendsto_atTop]687 intro ε hε688 have hden : 0 < ‖rootState‖ + 2 := by positivity689 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 a695 have hdist : ‖x - ofStage m a‖ < ε / (‖rootState‖ + 2) := by696 simpa only [dist_eq_norm, norm_sub_rev] using hyx697 have hlarge : (‖rootState‖ + 2) * ‖x - ofStage m a‖ < ε := by698 rw [mul_comm]699 exact (lt_div_iff₀ hden).mp hdist700 have hcoeff : 1 + ‖rootState‖ ≤ ‖rootState‖ + 2 := by linarith701 have herr : ‖compressionError n x‖ < ε := by702 calc703 ‖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‖ := by708 gcongr709 _ < ε := hlarge710 simpa [Real.dist_eq, abs_of_nonneg (norm_nonneg _)] using herr711712end MathlibAnnex.CStarAlgebra.CAR