Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/StagePurification.lean
Pinned GitHub source · Raw UTF-8 source
Back to Realizing a finite Gram matrix in a represented CAR corner · Back to Purifying a vector state on a finite CAR stage
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CornerLift2import MathlibAnnex.Analysis.CStarAlgebra.CAR.NoCompacts3import MathlibAnnex.Analysis.CStarAlgebra.Representation.VectorFunctional4import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension5import MathlibAnnex.Analysis.InnerProductSpace.FiniteEmbedding6import MathlibAnnex.Analysis.InnerProductSpace.ProjectionLimit78/-!9# Finite-stage vector-state reconstruction1011This file formalizes the algebraic core of finite-stage purification. A12family in the represented root corner is assembled with the stage matrix13units. Its vector state has precisely the prescribed Gram matrix on the14whole finite stage. The remaining existence problem is isolated to finding15such a corner family with the target Gram matrix.16-/1718set_option autoImplicit false1920open MathlibAnnex.Analysis.CStarAlgebra21open MathlibAnnex.Analysis.InnerProductSpace2223namespace MathlibAnnex.CStarAlgebra.CAR2425/-- Assemble a vector from a family in the represented root corner. -/26noncomputable def reconstructedStageVector27 {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)3132theorem representation_matrixUnit_reconstructedStageVector33 {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) := by39 classical40 simp only [reconstructedStageVector, map_sum]41 rw [Finset.sum_eq_single q]42 · rw [← ContinuousLinearMap.mul_apply, ← map_mul]43 simp44 · intro i _ hiq45 rw [← ContinuousLinearMap.mul_apply, ← map_mul, limitMatrixUnit_mul]46 simp [Ne.symm hiq]47 · simp4849private theorem inner_matrixUnit_columns50 {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 := by58 classical59 have hadj : ContinuousLinearMap.adjoint (ρ (limitMatrixUnit n i 0)) =60 ρ (limitMatrixUnit n 0 i) := by61 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star,62 star_limitMatrixUnit]63 calc64 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_right70 (ρ (limitMatrixUnit n i 0)) (w i)71 (ρ (limitMatrixUnit n p 0) (w q))).symm72 _ = inner ℂ (w i)73 (ρ (limitMatrixUnit n 0 i * limitMatrixUnit n p 0) (w q)) := by74 rw [hadj, map_mul]75 rfl76 _ = if i = p then inner ℂ (w i) (w q) else 0 := by77 by_cases hip : i = p78 · subst p79 simp [hw]80 · rw [limitMatrixUnit_mul]81 simp [hip]8283/-- The reconstructed vector has the requested Gram coefficient on every84matrix unit. -/85theorem vectorFunctional_reconstructedStageVector_matrixUnit86 {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) := by93 classical94 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 simp100 · intro i _ hip101 rw [inner_matrixUnit_columns ρ n w hw i p q]102 simp [hip]103 · simp104105private theorem vectorFunctional_matrixUnit_eq_cornerGram106 {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) η) := by112 simpa using Representation.vectorFunctional_star_mul σ η113 (limitMatrixUnit n 0 p) (limitMatrixUnit n 0 q)114115/-- Equality on the matrix-unit basis gives equality on the entire embedded116finite stage. -/117theorem continuousLinearMap_eq_on_ofStage_of_eq_matrixUnit118 (φ ψ : 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) := by122 rw [ofStage_eq_sum_smul_limitMatrixUnit]123 simp only [map_sum, map_smul]124 apply Finset.sum_congr rfl125 intro i _126 apply Finset.sum_congr rfl127 intro j _128 rw [h i j]129130/-- Proof-bearing finite-stage purification core. Any root-corner family131with the GNS Gram matrix reconstructs a vector state agreeing with the target132vector state on the whole chosen matrix stage; no rank-one restriction on the133target state is used. -/134theorem reconstructedStageVector_vectorFunctional_eq_on_stage135 {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) := by148 apply continuousLinearMap_eq_on_ofStage_of_eq_matrixUnit _ _ n _ c149 intro i j150 rw [vectorFunctional_reconstructedStageVector_matrixUnit ρ n w hw i j,151 hgram i j]152 exact (vectorFunctional_matrixUnit_eq_cornerGram σ n η i j).symm153154/-- The reconstruction preserves normalization. -/155theorem norm_reconstructedStageVector_eq_one156 {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 := by168 have hstate := reconstructedStageVector_vectorFunctional_eq_on_stage169 ρ σ n η w hw hgram (1 : Stage n)170 have hofone : ofStage n (1 : Stage n) = 1 := map_one (ofStage n)171 rw [hofone] at hstate172 have hinner :173 inner ℂ (reconstructedStageVector ρ n w)174 (reconstructedStageVector ρ n w) = inner ℂ η η := by175 simpa [Representation.vectorFunctional_apply] using hstate176 rw [inner_self_eq_norm_sq_to_K, inner_self_eq_norm_sq_to_K] at hinner177 have hre : ‖reconstructedStageVector ρ n w‖ ^ 2 = ‖η‖ ^ 2 := by178 exact_mod_cast hinner179 rw [hη, one_pow] at hre180 nlinarith [norm_nonneg (reconstructedStageVector ρ n w)]181182/-- In every nonzero irreducible CAR representation, the represented root183corner has infinite Hilbert dimension. Otherwise the corner projection184would be a nonzero compact operator in the represented CAR image. -/185theorem not_finiteDimensional_range_rootCorner186 {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) := by191 intro hfinite192 let P : H →L[ℂ] H := ρ (limitMatrixUnit n 0 0)193 let R : Submodule ℂ H := LinearMap.range P.toLinearMap194 let Q : H →L[ℂ] R := P.codRestrict R (fun x => ⟨x, rfl⟩)195 letI : FiniteDimensional ℂ R := hfinite196 letI : LocallyCompactSpace R :=197 LocallyCompactSpace.of_finiteDimensional_of_complete ℂ R198 have hQ : IsCompactOperator Q :=199 isCompactOperator_of_locallyCompactSpace_dom Q200 have hcompact : IsCompactOperator P := by201 have hc := hQ.clm_comp R.subtypeL202 simpa [P, Q, R, Function.comp_def] using hc203 have hezero : limitMatrixUnit n 0 0 = 0 :=204 eq_zero_of_isCompactOperator_image ρ hρ hcompact205 have hstage : matrixUnit n 0 0 = 0 := by206 apply ofStage_injective n207 change ofStage n (matrixUnit n 0 0) = 0 at hezero208 rw [map_zero]209 exact hezero210 have hentry := congrFun (congrFun hstage (0 : Fin (2 ^ n)))211 (0 : Fin (2 ^ n))212 simp at hentry213214/-- Any finite Gram matrix occurring in a Hilbert space can be realized by215vectors in the represented root corner of an irreducible CAR216representation. Infinite-dimensionality of the corner supplies an217isometric copy of the finite-dimensional span of the input family. -/218theorem exists_rootCornerFamily_with_gram219 {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) := by227 classical228 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.toLinearMap232 letI : CompleteSpace R := IsComplete.completeSpace_coe233 (ContinuousLinearMap.IsIdempotentElem.isClosed_range hP.isIdempotentElem).isComplete234 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 := by238 simpa [P, R] using239 not_finiteDimensional_range_rootCorner ρ hρ n240 obtain ⟨L⟩ :=241 nonempty_linearIsometry_of_finiteDimensional_of_not_finiteDimensional242 (E := S) (F := R) hR243 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 i248 have hmem : w i ∈ LinearMap.range P.toLinearMap := (L (vS i)).property249 exact (LinearMap.IsIdempotentElem.mem_range_iff250 (ContinuousLinearMap.IsIdempotentElem.toLinearMap251 hP.isIdempotentElem)).mp hmem252 · intro i j253 change inner ℂ (L (vS i)) (L (vS j)) = inner ℂ (vS i) (vS j)254 exact L.inner_map_map (vS i) (vS j)255256/-- Every unit vector state has an exact unit-vector realization on an257arbitrary finite CAR stage inside any irreducible CAR representation. This258is the finite-stage purification step, with the root-corner Gram family now259constructed rather than assumed. -/260theorem exists_unitVector_vectorFunctional_eq_on_stage261 {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) := by269 let v : Fin (2 ^ n) → K := fun i => σ (limitMatrixUnit n 0 i) η270 obtain ⟨w, hw, hgram⟩ :=271 exists_rootCornerFamily_with_gram ρ hρ n v272 refine ⟨reconstructedStageVector ρ n w,273 norm_reconstructedStageVector_eq_one ρ σ n η hη w hw ?_, ?_⟩274 · intro i j275 exact hgram i j276 · intro c277 exact reconstructedStageVector_vectorFunctional_eq_on_stage278 ρ σ n η w hw hgram c279280end MathlibAnnex.CStarAlgebra.CAR