Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TargetReconstruction.lean
Pinned GitHub source · Raw UTF-8 source
Back to Reconstructing a represented unitary from its shells and residual corner
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicModel2import MathlibAnnex.Analysis.CStarAlgebra.Representation.ShellReconstruction34/-!5# Reconstructing completed-CAR shells in an arbitrary target representation67The strong sums in this file are formed on the target Hilbert space. The8source representation contributes only finite algebraic projection and9support identities. Thus no continuity of an arbitrary representation for10the strong-operator topology is used.11-/1213set_option autoImplicit false14set_option maxHeartbeats 12000001516noncomputable section1718open Filter Topology19open scoped ComplexOrder ENNReal lp InnerProduct2021namespace MathlibAnnex.CStarAlgebra.CAR2223open MathlibAnnex.Analysis.CStarAlgebra24open MathlibAnnex.Analysis.InnerProductSpace2526universe v2728/-- The actual concrete target associated with a completed-CAR atomic family. -/29abbrev AtomicTarget30 (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 L3435/-- Restriction of an arbitrary target representation to the actual completed36CAR source. -/37noncomputable def restrictedRepresentation38 (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)4546/-- A target generator is unitary in every represented Hilbert space. -/47noncomputable def representedGeneratorUnitary48 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →49 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]50 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)51 (hLunit : ∀ i, L i ∈ unitary52 (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) := by57 have htarget : MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i ∈58 unitary (AtomicTarget L) := by59 rw [Unitary.mem_iff]60 constructor61 · apply Subtype.ext62 exact (hLunit i).163 · apply Subtype.ext64 exact (hLunit i).265 exact ⟨rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i),66 Unitary.map_mem rho htarget⟩6768@[simp]69theorem representedGeneratorUnitary_coe70 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →71 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]72 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)73 (hLunit : ∀ i, L i ∈ unitary74 (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) := rfl8283/-- The source shell relation becomes a finite relation in every target84representation. -/85theorem representedGenerator_comp_sourceShell86 (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 ∈ unitary91 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]92 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))93 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation94 (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.linearIsometryEquiv100 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) :101 K →L[ℂ] K).comp102 (restrictedRepresentation L rho103 (transportedFlag family i n - transportedFlag family i (n + 1))) =104 restrictedRepresentation L rho105 ((representativeShellData family i).link n) := by106 have htarget :107 MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i *108 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L109 (transportedFlag family i n - transportedFlag family i (n + 1)) =110 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L111 ((representativeShellData family i).link n) := by112 apply Subtype.ext113 exact hLsource i n114 change rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i) *115 rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L116 (transportedFlag family i n - transportedFlag family i (n + 1))) =117 rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L118 ((representativeShellData family i).link n))119 rw [← map_mul, htarget]120121/-- In every target Hilbert universe, the represented generator is rebuilt as122the strong sum of the represented completed-CAR shell links plus a precisely123supported limiting defect. -/124theorem exists_targetShellReconstruction125 (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 ∈ unitary130 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]131 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))132 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation133 (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 rho139 let p := transportedFlag family i140 let q := rootFlag141 let w := (representativeShellData family i).link142 let U : ℕ → Submodule ℂ K := fun n ↦ (sigma (p n)).range143 let V : ℕ → Submodule ℂ K := fun n ↦ (sigma (q n)).range144 ∃ S T P Q R : K →L[ℂ] K,145 ContinuousLinearMap.StronglyConverges146 (ContinuousLinearMap.partialSum (fun n ↦ sigma (w n))) atTop S ∧147 ContinuousLinearMap.StronglyConverges148 (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.linearIsometryEquiv154 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) =155 S + R ∧156 R = ((Unitary.linearIsometryEquiv157 (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.linearIsometryEquiv163 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) x ∈164 ⨅ n, V n) := by165 dsimp only166 apply exists_represented_unitaryCompletion_of_sourceShells167 (restrictedRepresentation L rho)168 (Unitary.linearIsometryEquiv169 (representedGeneratorUnitary L hLunit rho i))170 (transportedFlag family i) rootFlag171 (representativeShellData family i).link172 (isStarProjection_transportedFlag family i) isStarProjection_rootFlag173 (transportedFlag_zero family i) rootFlag_zero174 (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)179180end MathlibAnnex.CStarAlgebra.CAR