Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TargetReconstruction.lean, lines 28–33.
Back to Reconstructing a represented unitary from its shells and residual corner
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicModel 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.ShellReconstruction 3 4/-! 5# Reconstructing completed-CAR shells in an arbitrary target representation 6 7The strong sums in this file are formed on the target Hilbert space. The 8source representation contributes only finite algebraic projection and 9support identities. Thus no continuity of an arbitrary representation for 10the strong-operator topology is used. 11-/ 12 13set_option autoImplicit false 14set_option maxHeartbeats 1200000 15 16noncomputable section 17 18open Filter Topology 19open scoped ComplexOrder ENNReal lp InnerProduct 20 21namespace MathlibAnnex.CStarAlgebra.CAR 22 23open MathlibAnnex.Analysis.CStarAlgebra 24open MathlibAnnex.Analysis.InnerProductSpace 25 26universe v 27 28/-- The actual concrete target associated with a completed-CAR atomic family. -/ 29abbrev AtomicTarget 30 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → 31 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 32 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) := 33 MathlibAnnex.CStarAlgebra.AtomicConstruction.concreteTarget selectedAtomicRepresentation L 34 35/-- Restriction of an arbitrary target representation to the actual completed 36CAR source. -/ 37noncomputable def restrictedRepresentation 38 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → 39 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 40 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) 41 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 42 [CompleteSpace K] (rho : Representation (AtomicTarget L) K) : 43 Representation Limit K := 44 rho.comp (MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L) 45 46/-- A target generator is unitary in every represented Hilbert space. -/ 47noncomputable def representedGeneratorUnitary 48 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → 49 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 50 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) 51 (hLunit : ∀ i, L i ∈ unitary 52 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 53 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 54 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 55 [CompleteSpace K] (rho : Representation (AtomicTarget L) K) 56 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : unitary (K →L[ℂ] K) := by 57 have htarget : MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i ∈ 58 unitary (AtomicTarget L) := by 59 rw [Unitary.mem_iff] 60 constructor 61 · apply Subtype.ext 62 exact (hLunit i).1 63 · apply Subtype.ext 64 exact (hLunit i).2 65 exact ⟨rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i), 66 Unitary.map_mem rho htarget⟩ 67 68@[simp] 69theorem representedGeneratorUnitary_coe 70 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → 71 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 72 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) 73 (hLunit : ∀ i, L i ∈ unitary 74 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 75 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 76 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 77 [CompleteSpace K] (rho : Representation (AtomicTarget L) K) 78 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 79 ((representedGeneratorUnitary L hLunit rho i : unitary (K →L[ℂ] K)) : 80 K →L[ℂ] K) = 81 rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i) := rfl 82 83/-- The source shell relation becomes a finite relation in every target 84representation. -/ 85theorem representedGenerator_comp_sourceShell 86 (family : RepresentativeShellFamily) 87 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → 88 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 89 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) 90 (hLunit : ∀ i, L i ∈ unitary 91 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 92 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 93 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation 94 (transportedFlag family i n - transportedFlag family i (n + 1))) = 95 representedShellLink family i n) 96 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 97 [CompleteSpace K] (rho : Representation (AtomicTarget L) K) 98 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 99 ((Unitary.linearIsometryEquiv 100 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) : 101 K →L[ℂ] K).comp 102 (restrictedRepresentation L rho 103 (transportedFlag family i n - transportedFlag family i (n + 1))) = 104 restrictedRepresentation L rho 105 ((representativeShellData family i).link n) := by 106 have htarget : 107 MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i * 108 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L 109 (transportedFlag family i n - transportedFlag family i (n + 1)) = 110 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L 111 ((representativeShellData family i).link n) := by 112 apply Subtype.ext 113 exact hLsource i n 114 change rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i) * 115 rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L 116 (transportedFlag family i n - transportedFlag family i (n + 1))) = 117 rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L 118 ((representativeShellData family i).link n)) 119 rw [← map_mul, htarget] 120 121/-- In every target Hilbert universe, the represented generator is rebuilt as 122the strong sum of the represented completed-CAR shell links plus a precisely 123supported limiting defect. -/ 124theorem exists_targetShellReconstruction 125 (family : RepresentativeShellFamily) 126 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → 127 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 128 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) 129 (hLunit : ∀ i, L i ∈ unitary 130 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 131 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 132 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation 133 (transportedFlag family i n - transportedFlag family i (n + 1))) = 134 representedShellLink family i n) 135 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 136 [CompleteSpace K] (rho : Representation (AtomicTarget L) K) 137 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 138 let sigma := restrictedRepresentation L rho 139 let p := transportedFlag family i 140 let q := rootFlag 141 let w := (representativeShellData family i).link 142 let U : ℕ → Submodule ℂ K := fun n ↦ (sigma (p n)).range 143 let V : ℕ → Submodule ℂ K := fun n ↦ (sigma (q n)).range 144 ∃ S T P Q R : K →L[ℂ] K, 145 ContinuousLinearMap.StronglyConverges 146 (ContinuousLinearMap.partialSum (fun n ↦ sigma (w n))) atTop S ∧ 147 ContinuousLinearMap.StronglyConverges 148 (ContinuousLinearMap.partialSum (fun n ↦ (sigma (w n))†)) atTop T ∧ 149 ‖S‖ ≤ 1 ∧ ‖T‖ ≤ 1 ∧ T = S† ∧ 150 IsStarProjection P ∧ P.range = ⨅ n, U n ∧ 151 IsStarProjection Q ∧ Q.range = ⨅ n, V n ∧ 152 (S†).comp S = 1 - P ∧ S.comp (S†) = 1 - Q ∧ 153 (Unitary.linearIsometryEquiv 154 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) = 155 S + R ∧ 156 R = ((Unitary.linearIsometryEquiv 157 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) : 158 K →L[ℂ] K).comp P ∧ 159 (R†).comp R = P ∧ R.comp (R†) = Q ∧ 160 R = (Q.comp R).comp P ∧ 161 (∀ x, x ∈ ⨅ n, U n ↔ 162 (Unitary.linearIsometryEquiv 163 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) x ∈ 164 ⨅ n, V n) := by 165 dsimp only 166 apply exists_represented_unitaryCompletion_of_sourceShells 167 (restrictedRepresentation L rho) 168 (Unitary.linearIsometryEquiv 169 (representedGeneratorUnitary L hLunit rho i)) 170 (transportedFlag family i) rootFlag 171 (representativeShellData family i).link 172 (isStarProjection_transportedFlag family i) isStarProjection_rootFlag 173 (transportedFlag_zero family i) rootFlag_zero 174 (fun _ _ hmn ↦ transportedFlag_mul_of_le family i hmn) 175 (fun _ _ hmn ↦ rootFlag_mul_of_le hmn) 176 (representativeLink_initial family i) 177 (representativeLink_final family i) 178 (representedGenerator_comp_sourceShell family L hLunit hLsource rho i) 179 180end MathlibAnnex.CStarAlgebra.CAR