Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/StagePurification.lean, lines 115–128.
Back to Purifying a vector state on a finite CAR stage
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CornerLift 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.NoCompacts 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.VectorFunctional 4import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension 5import MathlibAnnex.Analysis.InnerProductSpace.FiniteEmbedding 6import MathlibAnnex.Analysis.InnerProductSpace.ProjectionLimit 7 8/-! 9# Finite-stage vector-state reconstruction 10 11This file formalizes the algebraic core of finite-stage purification. A 12family in the represented root corner is assembled with the stage matrix 13units. Its vector state has precisely the prescribed Gram matrix on the 14whole finite stage. The remaining existence problem is isolated to finding 15such a corner family with the target Gram matrix. 16-/ 17 18set_option autoImplicit false 19 20open MathlibAnnex.Analysis.CStarAlgebra 21open MathlibAnnex.Analysis.InnerProductSpace 22 23namespace MathlibAnnex.CStarAlgebra.CAR 24 25/-- Assemble a vector from a family in the represented root corner. -/ 26noncomputable def reconstructedStageVector 27 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 28 [CompleteSpace H] (ρ : Representation Limit H) (n : ℕ) 29 (w : Fin (2 ^ n) → H) : H := 30 ∑ i, ρ (limitMatrixUnit n i 0) (w i) 31 32theorem representation_matrixUnit_reconstructedStageVector 33 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 34 [CompleteSpace H] (ρ : Representation Limit H) (n : ℕ) 35 (w : Fin (2 ^ n) → H) 36 (p q : Fin (2 ^ n)) : 37 ρ (limitMatrixUnit n p q) (reconstructedStageVector ρ n w) = 38 ρ (limitMatrixUnit n p 0) (w q) := by 39 classical 40 simp only [reconstructedStageVector, map_sum] 41 rw [Finset.sum_eq_single q] 42 · rw [← ContinuousLinearMap.mul_apply, ← map_mul] 43 simp 44 · intro i _ hiq 45 rw [← ContinuousLinearMap.mul_apply, ← map_mul, limitMatrixUnit_mul] 46 simp [Ne.symm hiq] 47 · simp 48 49private theorem inner_matrixUnit_columns 50 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 51 [CompleteSpace H] (ρ : Representation Limit H) (n : ℕ) 52 (w : Fin (2 ^ n) → H) 53 (hw : ∀ i, ρ (limitMatrixUnit n 0 0) (w i) = w i) 54 (i p q : Fin (2 ^ n)) : 55 inner ℂ (ρ (limitMatrixUnit n i 0) (w i)) 56 (ρ (limitMatrixUnit n p 0) (w q)) = 57 if i = p then inner ℂ (w i) (w q) else 0 := by 58 classical 59 have hadj : ContinuousLinearMap.adjoint (ρ (limitMatrixUnit n i 0)) = 60 ρ (limitMatrixUnit n 0 i) := by 61 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star, 62 star_limitMatrixUnit] 63 calc 64 inner ℂ (ρ (limitMatrixUnit n i 0) (w i)) 65 (ρ (limitMatrixUnit n p 0) (w q)) = 66 inner ℂ (w i) 67 (ContinuousLinearMap.adjoint (ρ (limitMatrixUnit n i 0)) 68 (ρ (limitMatrixUnit n p 0) (w q))) := 69 (ContinuousLinearMap.adjoint_inner_right 70 (ρ (limitMatrixUnit n i 0)) (w i) 71 (ρ (limitMatrixUnit n p 0) (w q))).symm 72 _ = inner ℂ (w i) 73 (ρ (limitMatrixUnit n 0 i * limitMatrixUnit n p 0) (w q)) := by 74 rw [hadj, map_mul] 75 rfl 76 _ = if i = p then inner ℂ (w i) (w q) else 0 := by 77 by_cases hip : i = p 78 · subst p 79 simp [hw] 80 · rw [limitMatrixUnit_mul] 81 simp [hip] 82 83/-- The reconstructed vector has the requested Gram coefficient on every 84matrix unit. -/ 85theorem vectorFunctional_reconstructedStageVector_matrixUnit 86 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 87 [CompleteSpace H] (ρ : Representation Limit H) (n : ℕ) 88 (w : Fin (2 ^ n) → H) 89 (hw : ∀ i, ρ (limitMatrixUnit n 0 0) (w i) = w i) 90 (p q : Fin (2 ^ n)) : 91 Representation.vectorFunctional ρ (reconstructedStageVector ρ n w) 92 (limitMatrixUnit n p q) = inner ℂ (w p) (w q) := by 93 classical 94 rw [Representation.vectorFunctional_apply, 95 representation_matrixUnit_reconstructedStageVector] 96 simp only [reconstructedStageVector, sum_inner] 97 rw [Finset.sum_eq_single p] 98 · rw [inner_matrixUnit_columns ρ n w hw p p q] 99 simp 100 · intro i _ hip 101 rw [inner_matrixUnit_columns ρ n w hw i p q] 102 simp [hip] 103 · simp 104 105private theorem vectorFunctional_matrixUnit_eq_cornerGram 106 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 107 [CompleteSpace H] (σ : Representation Limit H) (n : ℕ) 108 (η : H) (p q : Fin (2 ^ n)) : 109 Representation.vectorFunctional σ η (limitMatrixUnit n p q) = 110 inner ℂ (σ (limitMatrixUnit n 0 p) η) 111 (σ (limitMatrixUnit n 0 q) η) := by 112 simpa using Representation.vectorFunctional_star_mul σ η 113 (limitMatrixUnit n 0 p) (limitMatrixUnit n 0 q) 114 115/-- Equality on the matrix-unit basis gives equality on the entire embedded 116finite stage. -/ 117theorem continuousLinearMap_eq_on_ofStage_of_eq_matrixUnit 118 (φ ψ : Limit →L[ℂ] ℂ) (n : ℕ) 119 (h : ∀ i j : Fin (2 ^ n), 120 φ (limitMatrixUnit n i j) = ψ (limitMatrixUnit n i j)) 121 (c : Stage n) : φ (ofStage n c) = ψ (ofStage n c) := by 122 rw [ofStage_eq_sum_smul_limitMatrixUnit] 123 simp only [map_sum, map_smul] 124 apply Finset.sum_congr rfl 125 intro i _ 126 apply Finset.sum_congr rfl 127 intro j _ 128 rw [h i j] 129 130/-- Proof-bearing finite-stage purification core. Any root-corner family 131with the GNS Gram matrix reconstructs a vector state agreeing with the target 132vector state on the whole chosen matrix stage; no rank-one restriction on the 133target state is used. -/ 134theorem reconstructedStageVector_vectorFunctional_eq_on_stage 135 {H K : Type*} 136 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 137 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 138 (ρ : Representation Limit H) (σ : Representation Limit K) 139 (n : ℕ) (η : K) (w : Fin (2 ^ n) → H) 140 (hw : ∀ i, ρ (limitMatrixUnit n 0 0) (w i) = w i) 141 (hgram : ∀ i j, 142 inner ℂ (w i) (w j) = 143 inner ℂ (σ (limitMatrixUnit n 0 i) η) 144 (σ (limitMatrixUnit n 0 j) η)) 145 (c : Stage n) : 146 Representation.vectorFunctional ρ (reconstructedStageVector ρ n w) 147 (ofStage n c) = Representation.vectorFunctional σ η (ofStage n c) := by 148 apply continuousLinearMap_eq_on_ofStage_of_eq_matrixUnit _ _ n _ c 149 intro i j 150 rw [vectorFunctional_reconstructedStageVector_matrixUnit ρ n w hw i j, 151 hgram i j] 152 exact (vectorFunctional_matrixUnit_eq_cornerGram σ n η i j).symm 153 154/-- The reconstruction preserves normalization. -/ 155theorem norm_reconstructedStageVector_eq_one 156 {H K : Type*} 157 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 158 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 159 (ρ : Representation Limit H) (σ : Representation Limit K) 160 (n : ℕ) (η : K) (hη : ‖η‖ = 1) 161 (w : Fin (2 ^ n) → H) 162 (hw : ∀ i, ρ (limitMatrixUnit n 0 0) (w i) = w i) 163 (hgram : ∀ i j, 164 inner ℂ (w i) (w j) = 165 inner ℂ (σ (limitMatrixUnit n 0 i) η) 166 (σ (limitMatrixUnit n 0 j) η)) : 167 ‖reconstructedStageVector ρ n w‖ = 1 := by 168 have hstate := reconstructedStageVector_vectorFunctional_eq_on_stage 169 ρ σ n η w hw hgram (1 : Stage n) 170 have hofone : ofStage n (1 : Stage n) = 1 := map_one (ofStage n) 171 rw [hofone] at hstate 172 have hinner : 173 inner ℂ (reconstructedStageVector ρ n w) 174 (reconstructedStageVector ρ n w) = inner ℂ η η := by 175 simpa [Representation.vectorFunctional_apply] using hstate 176 rw [inner_self_eq_norm_sq_to_K, inner_self_eq_norm_sq_to_K] at hinner 177 have hre : ‖reconstructedStageVector ρ n w‖ ^ 2 = ‖η‖ ^ 2 := by 178 exact_mod_cast hinner 179 rw [hη, one_pow] at hre 180 nlinarith [norm_nonneg (reconstructedStageVector ρ n w)] 181 182/-- In every nonzero irreducible CAR representation, the represented root 183corner has infinite Hilbert dimension. Otherwise the corner projection 184would be a nonzero compact operator in the represented CAR image. -/ 185theorem not_finiteDimensional_range_rootCorner 186 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 187 [CompleteSpace H] (ρ : Representation Limit H) 188 (hρ : ρ.IsIrreducible) (n : ℕ) : 189 ¬ FiniteDimensional ℂ 190 (LinearMap.range (ρ (limitMatrixUnit n 0 0)).toLinearMap) := by 191 intro hfinite 192 let P : H →L[ℂ] H := ρ (limitMatrixUnit n 0 0) 193 let R : Submodule ℂ H := LinearMap.range P.toLinearMap 194 let Q : H →L[ℂ] R := P.codRestrict R (fun x => ⟨x, rfl⟩) 195 letI : FiniteDimensional ℂ R := hfinite 196 letI : LocallyCompactSpace R := 197 LocallyCompactSpace.of_finiteDimensional_of_complete ℂ R 198 have hQ : IsCompactOperator Q := 199 isCompactOperator_of_locallyCompactSpace_dom Q 200 have hcompact : IsCompactOperator P := by 201 have hc := hQ.clm_comp R.subtypeL 202 simpa [P, Q, R, Function.comp_def] using hc 203 have hezero : limitMatrixUnit n 0 0 = 0 := 204 eq_zero_of_isCompactOperator_image ρ hρ hcompact 205 have hstage : matrixUnit n 0 0 = 0 := by 206 apply ofStage_injective n 207 change ofStage n (matrixUnit n 0 0) = 0 at hezero 208 rw [map_zero] 209 exact hezero 210 have hentry := congrFun (congrFun hstage (0 : Fin (2 ^ n))) 211 (0 : Fin (2 ^ n)) 212 simp at hentry 213 214/-- Any finite Gram matrix occurring in a Hilbert space can be realized by 215vectors in the represented root corner of an irreducible CAR 216representation. Infinite-dimensionality of the corner supplies an 217isometric copy of the finite-dimensional span of the input family. -/ 218theorem exists_rootCornerFamily_with_gram 219 {H K : Type*} 220 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 221 [NormedAddCommGroup K] [InnerProductSpace ℂ K] 222 (ρ : Representation Limit H) (hρ : ρ.IsIrreducible) 223 (n : ℕ) {I : Type*} [Fintype I] (v : I → K) : 224 ∃ w : I → H, 225 (∀ i, ρ (limitMatrixUnit n 0 0) (w i) = w i) ∧ 226 ∀ i j, inner ℂ (w i) (w j) = inner ℂ (v i) (v j) := by 227 classical 228 let P : H →L[ℂ] H := ρ (limitMatrixUnit n 0 0) 229 have hP : IsStarProjection P := 230 (isStarProjection_limitMatrixUnit_zero_zero n).map ρ 231 let R : Submodule ℂ H := LinearMap.range P.toLinearMap 232 letI : CompleteSpace R := IsComplete.completeSpace_coe 233 (ContinuousLinearMap.IsIdempotentElem.isClosed_range hP.isIdempotentElem).isComplete 234 let S : Submodule ℂ K := Submodule.span ℂ (Set.range v) 235 letI : FiniteDimensional ℂ S := 236 FiniteDimensional.span_of_finite ℂ (Set.finite_range v) 237 have hR : ¬ FiniteDimensional ℂ R := by 238 simpa [P, R] using 239 not_finiteDimensional_range_rootCorner ρ hρ n 240 obtain ⟨L⟩ := 241 nonempty_linearIsometry_of_finiteDimensional_of_not_finiteDimensional 242 (E := S) (F := R) hR 243 let vS : I → S := fun i => 244 ⟨v i, Submodule.subset_span (Set.mem_range_self i)⟩ 245 let w : I → H := fun i => (L (vS i) : R) 246 refine ⟨w, ?_, ?_⟩ 247 · intro i 248 have hmem : w i ∈ LinearMap.range P.toLinearMap := (L (vS i)).property 249 exact (LinearMap.IsIdempotentElem.mem_range_iff 250 (ContinuousLinearMap.IsIdempotentElem.toLinearMap 251 hP.isIdempotentElem)).mp hmem 252 · intro i j 253 change inner ℂ (L (vS i)) (L (vS j)) = inner ℂ (vS i) (vS j) 254 exact L.inner_map_map (vS i) (vS j) 255 256/-- Every unit vector state has an exact unit-vector realization on an 257arbitrary finite CAR stage inside any irreducible CAR representation. This 258is the finite-stage purification step, with the root-corner Gram family now 259constructed rather than assumed. -/ 260theorem exists_unitVector_vectorFunctional_eq_on_stage 261 {H K : Type*} 262 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 263 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 264 (ρ : Representation Limit H) (hρ : ρ.IsIrreducible) 265 (σ : Representation Limit K) (n : ℕ) (η : K) (hη : ‖η‖ = 1) : 266 ∃ ξ : H, ‖ξ‖ = 1 ∧ ∀ c : Stage n, 267 Representation.vectorFunctional ρ ξ (ofStage n c) = 268 Representation.vectorFunctional σ η (ofStage n c) := by 269 let v : Fin (2 ^ n) → K := fun i => σ (limitMatrixUnit n 0 i) η 270 obtain ⟨w, hw, hgram⟩ := 271 exists_rootCornerFamily_with_gram ρ hρ n v 272 refine ⟨reconstructedStageVector ρ n w, 273 norm_reconstructedStageVector_eq_one ρ σ n η hη w hw ?_, ?_⟩ 274 · intro i j 275 exact hgram i j 276 · intro c 277 exact reconstructedStageVector_vectorFunctional_eq_on_stage 278 ρ σ n η w hw hgram c 279 280end MathlibAnnex.CStarAlgebra.CAR