Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CaptureSurviving.lean
Pinned GitHub source · Raw UTF-8 source
Back to The cyclic sum fills every irreducible target representation · Back to A common root vector realizes every selected state through the generators
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CaptureZero2import Mathlib.Analysis.Normed.Module.Normalize34/-!5# Vectors carried by a surviving completed-CAR defect67The target-side unitary-completion relation transports a normalized vector8from a nonzero initial limiting fixed space to the root limiting fixed space.9The actual completed-CAR compression estimates then identify both vector10states. No ambient rank-one assertion is made for an arbitrary target11representation.12-/1314set_option autoImplicit false15set_option maxHeartbeats 12000001617noncomputable section1819open Filter Topology20open scoped ComplexOrder ENNReal lp InnerProduct2122namespace MathlibAnnex.CStarAlgebra.CAR2324open MathlibAnnex.Analysis.CStarAlgebra25open MathlibAnnex.Analysis.InnerProductSpace2627universe v2829/-- A specified nonzero limiting fixed space supplies unit vectors carrying30the selected state and the root state, joined by the represented target31generator. -/32theorem exists_targetDefectVectors_of_fixedSpace_ne_bot33 (family : RepresentativeShellFamily)34 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →35 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]36 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)37 (hLunit : ∀ i, L i ∈ unitary38 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]39 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))40 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation41 (transportedFlag family i n - transportedFlag family i (n + 1))) =42 representedShellLink family i n)43 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]44 [CompleteSpace K] (rho : Representation (AtomicTarget L) K)45 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit)46 (hi : (⨅ n, ((restrictedRepresentation L rho)47 (transportedFlag family i n)).range) ≠ ⊥) :48 ∃ eta_i eta_o : K,49 ‖eta_i‖ = 1 ∧ ‖eta_o‖ = 1 ∧50 (∀ n, (restrictedRepresentation L rho)51 (transportedFlag family i n) eta_i = eta_i) ∧52 (∀ n, (restrictedRepresentation L rho) (rootFlag n) eta_o = eta_o) ∧53 (Unitary.linearIsometryEquiv54 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) eta_i = eta_o ∧55 Representation.vectorFunctional (restrictedRepresentation L rho) eta_i =56 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 ∧57 Representation.vectorFunctional (restrictedRepresentation L rho) eta_o =58 rootState := by59 let sigma := restrictedRepresentation L rho60 let U : ℕ → Submodule ℂ K := fun n ↦61 (sigma (transportedFlag family i n)).range62 let V : ℕ → Submodule ℂ K := fun n ↦ (sigma (rootFlag n)).range63 obtain ⟨S, T, P, Q, R, -, -, -, -, -, -, hPrange, -, hQrange, -, -, -, -,64 -, -, -, htransport⟩ :=65 exists_targetShellReconstruction family L hLunit hLsource rho i66 have hU_ne : (⨅ n, U n) ≠ ⊥ := by67 simpa [U, sigma] using hi68 obtain ⟨x, hxU, hxne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hU_ne69 let eta_i : K := NormedSpace.normalize x70 have heta_i_norm : ‖eta_i‖ = 1 := NormedSpace.norm_normalize hxne71 have heta_i_mem : eta_i ∈ ⨅ n, U n := by72 change NormedSpace.normalize x ∈ ⨅ n, U n73 rw [NormedSpace.normalize]74 exact (⨅ n, U n).smul_mem (‖x‖⁻¹ : ℝ) hxU75 let e : K ≃ₗᵢ[ℂ] K := Unitary.linearIsometryEquiv76 (representedGeneratorUnitary L hLunit rho i)77 let eta_o : K := e eta_i78 have heta_o_norm : ‖eta_o‖ = 1 := by79 rw [show ‖eta_o‖ = ‖eta_i‖ by exact e.norm_map eta_i]80 exact heta_i_norm81 have heta_o_mem : eta_o ∈ ⨅ n, V n := by82 exact (htransport eta_i).1 heta_i_mem83 have heta_i_fixed (n : ℕ) :84 sigma (transportedFlag family i n) eta_i = eta_i := by85 have hn : eta_i ∈ U n := (Submodule.mem_iInf U).mp heta_i_mem n86 exact LinearMap.IsIdempotentElem.mem_range_iff87 (ContinuousLinearMap.IsIdempotentElem.toLinearMap88 (IsStarProjection.map_representation sigma89 (isStarProjection_transportedFlag family i n)).isIdempotentElem) |>.mp hn90 have heta_o_fixed (n : ℕ) : sigma (rootFlag n) eta_o = eta_o := by91 have hn : eta_o ∈ V n := (Submodule.mem_iInf V).mp heta_o_mem n92 exact LinearMap.IsIdempotentElem.mem_range_iff93 (ContinuousLinearMap.IsIdempotentElem.toLinearMap94 (IsStarProjection.map_representation sigma95 (isStarProjection_rootFlag n)).isIdempotentElem) |>.mp hn96 have heta_i_state : Representation.vectorFunctional sigma eta_i =97 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 := by98 apply ContinuousLinearMap.ext99 intro b100 have hcoeff := inner_map_eq_of_compression_tendsto sigma101 (Representation.continuousLinearMap sigma).continuous102 (transportedFlag family i)103 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 b eta_i eta_i104 (fun n ↦ (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq)105 heta_i_fixed heta_i_fixed106 (tendsto_representative_transported_compression family i b)107 have hself : inner ℂ eta_i eta_i = 1 := by108 rw [inner_self_eq_norm_sq_to_K, heta_i_norm]109 norm_num110 change inner ℂ eta_i (sigma b eta_i) =111 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 b112 calc113 inner ℂ eta_i (sigma b eta_i) =114 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 b *115 inner ℂ eta_i eta_i := hcoeff116 _ = (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 b := by117 rw [hself, mul_one]118 have heta_o_state : Representation.vectorFunctional sigma eta_o = rootState := by119 apply ContinuousLinearMap.ext120 intro b121 have hcompression : Tendsto122 (fun n ↦ rootFlag n * b * rootFlag n - rootState b • rootFlag n)123 atTop (nhds 0) := by124 simpa using tendsto_transported_compressionError125 (StarAlgEquiv.refl ℂ Limit) rootState (fun _ ↦ rfl) b126 have hcoeff := inner_map_eq_of_compression_tendsto sigma127 (Representation.continuousLinearMap sigma).continuous rootFlag rootState128 b eta_o eta_o129 (fun n ↦ (isStarProjection_rootFlag n).isSelfAdjoint.star_eq)130 heta_o_fixed heta_o_fixed hcompression131 have hself : inner ℂ eta_o eta_o = 1 := by132 rw [inner_self_eq_norm_sq_to_K, heta_o_norm]133 norm_num134 change inner ℂ eta_o (sigma b eta_o) = rootState b135 calc136 inner ℂ eta_o (sigma b eta_o) =137 rootState b * inner ℂ eta_o eta_o := hcoeff138 _ = rootState b := by rw [hself, mul_one]139 exact ⟨eta_i, eta_o, heta_i_norm, heta_o_norm,140 heta_i_fixed, heta_o_fixed, rfl, heta_i_state, heta_o_state⟩141142/-- Every irreducible target representation contains a transported pair of143unit defect vectors with the exact selected and root completed-CAR states. -/144theorem exists_targetDefectVectors145 (family : RepresentativeShellFamily)146 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →147 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]148 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)149 (hLunit : ∀ i, L i ∈ unitary150 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]151 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))152 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation153 (transportedFlag family i n - transportedFlag family i (n + 1))) =154 representedShellLink family i n)155 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]156 [CompleteSpace K] (rho : Representation (AtomicTarget L) K)157 (hrho : rho.IsIrreducible) :158 ∃ (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (eta_i eta_o : K),159 ‖eta_i‖ = 1 ∧ ‖eta_o‖ = 1 ∧160 (∀ n, (restrictedRepresentation L rho)161 (transportedFlag family i n) eta_i = eta_i) ∧162 (∀ n, (restrictedRepresentation L rho) (rootFlag n) eta_o = eta_o) ∧163 (Unitary.linearIsometryEquiv164 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) eta_i = eta_o ∧165 Representation.vectorFunctional (restrictedRepresentation L rho) eta_i =166 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 ∧167 Representation.vectorFunctional (restrictedRepresentation L rho) eta_o =168 rootState := by169 obtain ⟨i, hi⟩ := exists_nonzero_targetFixedSpace170 family L hLunit hLsource rho hrho171 obtain ⟨eta_i, eta_o, h⟩ :=172 exists_targetDefectVectors_of_fixedSpace_ne_bot173 family L hLunit hLsource rho i hi174 exact ⟨i, eta_i, eta_o, h⟩175176/-- A surviving defect yields one common root unit vector and a compatible177unit defect vector for every selected pure-state class. Each represented178generator sends its selected vector to the same root vector, and every vector179state is identified from the actual completed-CAR compression theorem. -/180theorem exists_targetDefectVectorFamily181 (family : RepresentativeShellFamily)182 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →183 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]184 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)185 (hLunit : ∀ i, L i ∈ unitary186 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]187 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))188 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation189 (transportedFlag family i n - transportedFlag family i (n + 1))) =190 representedShellLink family i n)191 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]192 [CompleteSpace K] (rho : Representation (AtomicTarget L) K)193 (hrho : rho.IsIrreducible) :194 ∃ (eta_o : K) (eta : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → K),195 ‖eta_o‖ = 1 ∧196 (∀ n, (restrictedRepresentation L rho) (rootFlag n) eta_o = eta_o) ∧197 Representation.vectorFunctional (restrictedRepresentation L rho) eta_o =198 rootState ∧199 ∀ i,200 ‖eta i‖ = 1 ∧201 (∀ n, (restrictedRepresentation L rho)202 (transportedFlag family i n) (eta i) = eta i) ∧203 (Unitary.linearIsometryEquiv204 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) (eta i) =205 eta_o ∧206 Representation.vectorFunctional (restrictedRepresentation L rho) (eta i) =207 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 := by208 obtain ⟨i₀, eta₀, eta_o, -, heta_o_norm, -, heta_o_fixed, -, -,209 heta_o_state⟩ :=210 exists_targetDefectVectors family L hLunit hLsource rho hrho211 let sigma := restrictedRepresentation L rho212 have heta_o_mem : eta_o ∈213 (⨅ n, (sigma (rootFlag n)).range) := by214 rw [Submodule.mem_iInf]215 intro n216 exact ⟨eta_o, heta_o_fixed n⟩217 let e (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : K ≃ₗᵢ[ℂ] K :=218 Unitary.linearIsometryEquiv219 (representedGeneratorUnitary L hLunit rho i)220 let eta (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : K := (e i).symm eta_o221 refine ⟨eta_o, eta, heta_o_norm, heta_o_fixed, heta_o_state, ?_⟩222 intro i223 have heta_norm : ‖eta i‖ = 1 := by224 rw [show ‖eta i‖ = ‖eta_o‖ by exact (e i).symm.norm_map eta_o]225 exact heta_o_norm226 obtain ⟨S, T, P, Q, R, -, -, -, -, -, -, -, -, -, -, -, -, -, -, -, -,227 htransport⟩ :=228 exists_targetShellReconstruction family L hLunit hLsource rho i229 have heta_mem : eta i ∈230 (⨅ n, (sigma (transportedFlag family i n)).range) := by231 apply (htransport (eta i)).2232 simpa [e, eta] using heta_o_mem233 have heta_fixed (n : ℕ) :234 sigma (transportedFlag family i n) (eta i) = eta i := by235 have hn : eta i ∈ (sigma (transportedFlag family i n)).range :=236 (Submodule.mem_iInf _).mp heta_mem n237 exact LinearMap.IsIdempotentElem.mem_range_iff238 (ContinuousLinearMap.IsIdempotentElem.toLinearMap239 (IsStarProjection.map_representation sigma240 (isStarProjection_transportedFlag family i n)).isIdempotentElem) |>.mp hn241 have heta_state : Representation.vectorFunctional sigma (eta i) =242 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 := by243 apply vectorFunctional_eq_of_compression_tendsto sigma244 (transportedFlag family i)245 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1246 (fun n ↦ (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq)247 (tendsto_representative_transported_compression family i)248 (eta i) heta_norm heta_fixed249 refine ⟨heta_norm, heta_fixed, ?_, heta_state⟩250 simp [e, eta]251252end MathlibAnnex.CStarAlgebra.CAR