Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CaptureSurviving.lean, lines 176–250.
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.CaptureZero 2import Mathlib.Analysis.Normed.Module.Normalize 3 4/-! 5# Vectors carried by a surviving completed-CAR defect 6 7The target-side unitary-completion relation transports a normalized vector 8from a nonzero initial limiting fixed space to the root limiting fixed space. 9The actual completed-CAR compression estimates then identify both vector 10states. No ambient rank-one assertion is made for an arbitrary target 11representation. 12-/ 13 14set_option autoImplicit false 15set_option maxHeartbeats 1200000 16 17noncomputable section 18 19open Filter Topology 20open scoped ComplexOrder ENNReal lp InnerProduct 21 22namespace MathlibAnnex.CStarAlgebra.CAR 23 24open MathlibAnnex.Analysis.CStarAlgebra 25open MathlibAnnex.Analysis.InnerProductSpace 26 27universe v 28 29/-- A specified nonzero limiting fixed space supplies unit vectors carrying 30the selected state and the root state, joined by the represented target 31generator. -/ 32theorem exists_targetDefectVectors_of_fixedSpace_ne_bot 33 (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 ∈ unitary 38 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 39 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 40 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation 41 (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.linearIsometryEquiv 54 (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 := by 59 let sigma := restrictedRepresentation L rho 60 let U : ℕ → Submodule ℂ K := fun n ↦ 61 (sigma (transportedFlag family i n)).range 62 let V : ℕ → Submodule ℂ K := fun n ↦ (sigma (rootFlag n)).range 63 obtain ⟨S, T, P, Q, R, -, -, -, -, -, -, hPrange, -, hQrange, -, -, -, -, 64 -, -, -, htransport⟩ := 65 exists_targetShellReconstruction family L hLunit hLsource rho i 66 have hU_ne : (⨅ n, U n) ≠ ⊥ := by 67 simpa [U, sigma] using hi 68 obtain ⟨x, hxU, hxne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hU_ne 69 let eta_i : K := NormedSpace.normalize x 70 have heta_i_norm : ‖eta_i‖ = 1 := NormedSpace.norm_normalize hxne 71 have heta_i_mem : eta_i ∈ ⨅ n, U n := by 72 change NormedSpace.normalize x ∈ ⨅ n, U n 73 rw [NormedSpace.normalize] 74 exact (⨅ n, U n).smul_mem (‖x‖⁻¹ : ℝ) hxU 75 let e : K ≃ₗᵢ[ℂ] K := Unitary.linearIsometryEquiv 76 (representedGeneratorUnitary L hLunit rho i) 77 let eta_o : K := e eta_i 78 have heta_o_norm : ‖eta_o‖ = 1 := by 79 rw [show ‖eta_o‖ = ‖eta_i‖ by exact e.norm_map eta_i] 80 exact heta_i_norm 81 have heta_o_mem : eta_o ∈ ⨅ n, V n := by 82 exact (htransport eta_i).1 heta_i_mem 83 have heta_i_fixed (n : ℕ) : 84 sigma (transportedFlag family i n) eta_i = eta_i := by 85 have hn : eta_i ∈ U n := (Submodule.mem_iInf U).mp heta_i_mem n 86 exact LinearMap.IsIdempotentElem.mem_range_iff 87 (ContinuousLinearMap.IsIdempotentElem.toLinearMap 88 (IsStarProjection.map_representation sigma 89 (isStarProjection_transportedFlag family i n)).isIdempotentElem) |>.mp hn 90 have heta_o_fixed (n : ℕ) : sigma (rootFlag n) eta_o = eta_o := by 91 have hn : eta_o ∈ V n := (Submodule.mem_iInf V).mp heta_o_mem n 92 exact LinearMap.IsIdempotentElem.mem_range_iff 93 (ContinuousLinearMap.IsIdempotentElem.toLinearMap 94 (IsStarProjection.map_representation sigma 95 (isStarProjection_rootFlag n)).isIdempotentElem) |>.mp hn 96 have heta_i_state : Representation.vectorFunctional sigma eta_i = 97 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 := by 98 apply ContinuousLinearMap.ext 99 intro b 100 have hcoeff := inner_map_eq_of_compression_tendsto sigma 101 (Representation.continuousLinearMap sigma).continuous 102 (transportedFlag family i) 103 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 b eta_i eta_i 104 (fun n ↦ (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq) 105 heta_i_fixed heta_i_fixed 106 (tendsto_representative_transported_compression family i b) 107 have hself : inner ℂ eta_i eta_i = 1 := by 108 rw [inner_self_eq_norm_sq_to_K, heta_i_norm] 109 norm_num 110 change inner ℂ eta_i (sigma b eta_i) = 111 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 b 112 calc 113 inner ℂ eta_i (sigma b eta_i) = 114 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 b * 115 inner ℂ eta_i eta_i := hcoeff 116 _ = (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 b := by 117 rw [hself, mul_one] 118 have heta_o_state : Representation.vectorFunctional sigma eta_o = rootState := by 119 apply ContinuousLinearMap.ext 120 intro b 121 have hcompression : Tendsto 122 (fun n ↦ rootFlag n * b * rootFlag n - rootState b • rootFlag n) 123 atTop (nhds 0) := by 124 simpa using tendsto_transported_compressionError 125 (StarAlgEquiv.refl ℂ Limit) rootState (fun _ ↦ rfl) b 126 have hcoeff := inner_map_eq_of_compression_tendsto sigma 127 (Representation.continuousLinearMap sigma).continuous rootFlag rootState 128 b eta_o eta_o 129 (fun n ↦ (isStarProjection_rootFlag n).isSelfAdjoint.star_eq) 130 heta_o_fixed heta_o_fixed hcompression 131 have hself : inner ℂ eta_o eta_o = 1 := by 132 rw [inner_self_eq_norm_sq_to_K, heta_o_norm] 133 norm_num 134 change inner ℂ eta_o (sigma b eta_o) = rootState b 135 calc 136 inner ℂ eta_o (sigma b eta_o) = 137 rootState b * inner ℂ eta_o eta_o := hcoeff 138 _ = 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⟩ 141 142/-- Every irreducible target representation contains a transported pair of 143unit defect vectors with the exact selected and root completed-CAR states. -/ 144theorem exists_targetDefectVectors 145 (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 ∈ unitary 150 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 151 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 152 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation 153 (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.linearIsometryEquiv 164 (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 := by 169 obtain ⟨i, hi⟩ := exists_nonzero_targetFixedSpace 170 family L hLunit hLsource rho hrho 171 obtain ⟨eta_i, eta_o, h⟩ := 172 exists_targetDefectVectors_of_fixedSpace_ne_bot 173 family L hLunit hLsource rho i hi 174 exact ⟨i, eta_i, eta_o, h⟩ 175 176/-- A surviving defect yields one common root unit vector and a compatible 177unit defect vector for every selected pure-state class. Each represented 178generator sends its selected vector to the same root vector, and every vector 179state is identified from the actual completed-CAR compression theorem. -/ 180theorem exists_targetDefectVectorFamily 181 (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 ∈ unitary 186 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 187 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 188 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation 189 (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.linearIsometryEquiv 204 (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 := by 208 obtain ⟨i₀, eta₀, eta_o, -, heta_o_norm, -, heta_o_fixed, -, -, 209 heta_o_state⟩ := 210 exists_targetDefectVectors family L hLunit hLsource rho hrho 211 let sigma := restrictedRepresentation L rho 212 have heta_o_mem : eta_o ∈ 213 (⨅ n, (sigma (rootFlag n)).range) := by 214 rw [Submodule.mem_iInf] 215 intro n 216 exact ⟨eta_o, heta_o_fixed n⟩ 217 let e (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : K ≃ₗᵢ[ℂ] K := 218 Unitary.linearIsometryEquiv 219 (representedGeneratorUnitary L hLunit rho i) 220 let eta (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : K := (e i).symm eta_o 221 refine ⟨eta_o, eta, heta_o_norm, heta_o_fixed, heta_o_state, ?_⟩ 222 intro i 223 have heta_norm : ‖eta i‖ = 1 := by 224 rw [show ‖eta i‖ = ‖eta_o‖ by exact (e i).symm.norm_map eta_o] 225 exact heta_o_norm 226 obtain ⟨S, T, P, Q, R, -, -, -, -, -, -, -, -, -, -, -, -, -, -, -, -, 227 htransport⟩ := 228 exists_targetShellReconstruction family L hLunit hLsource rho i 229 have heta_mem : eta i ∈ 230 (⨅ n, (sigma (transportedFlag family i n)).range) := by 231 apply (htransport (eta i)).2 232 simpa [e, eta] using heta_o_mem 233 have heta_fixed (n : ℕ) : 234 sigma (transportedFlag family i n) (eta i) = eta i := by 235 have hn : eta i ∈ (sigma (transportedFlag family i n)).range := 236 (Submodule.mem_iInf _).mp heta_mem n 237 exact LinearMap.IsIdempotentElem.mem_range_iff 238 (ContinuousLinearMap.IsIdempotentElem.toLinearMap 239 (IsStarProjection.map_representation sigma 240 (isStarProjection_transportedFlag family i n)).isIdempotentElem) |>.mp hn 241 have heta_state : Representation.vectorFunctional sigma (eta i) = 242 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 := by 243 apply vectorFunctional_eq_of_compression_tendsto sigma 244 (transportedFlag family i) 245 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 246 (fun n ↦ (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq) 247 (tendsto_representative_transported_compression family i) 248 (eta i) heta_norm heta_fixed 249 refine ⟨heta_norm, heta_fixed, ?_, heta_state⟩ 250 simp [e, eta] 251 252end MathlibAnnex.CStarAlgebra.CAR