Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/ShellReconstruction.lean
Pinned GitHub source · Raw UTF-8 source
Back to Reconstructing a represented unitary from its shells and residual corner
1import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Basic3import MathlibAnnex.Analysis.InnerProductSpace.ProjectionLimit4import MathlibAnnex.Analysis.InnerProductSpace.ProjectionShell5import MathlibAnnex.Analysis.InnerProductSpace.UnitaryCompletion67/-!8# Rebuilding shell strong sums in an arbitrary representation910Only algebraic source identities are transported through the representation.11The strong limits are then reconstructed in the target Hilbert space by the12orthogonal-shell theorem; no representation is claimed to preserve a strong13operator limit formed elsewhere.14-/1516set_option autoImplicit false1718open Filter Topology19open scoped InnerProduct2021namespace MathlibAnnex.Analysis.CStarAlgebra2223universe u v2425variable {A : Type u} [CStarAlgebra A]26variable {H : Type v}27variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2829/-- Star projections remain star projections under a unital star-algebra30homomorphism. -/31theorem IsStarProjection.map_representation32 (pi : Representation A H) {p : A} (hp : IsStarProjection p) :33 IsStarProjection (pi p) := by34 constructor35 · rw [isIdempotentElem_iff, ← map_mul, hp.isIdempotentElem.eq]36 · rw [isSelfAdjoint_iff, ← map_star, hp.isSelfAdjoint.star_eq]3738/-- Algebraic decreasing projection flags and exact shell supports rebuild39both strong shell sums and their limiting products in every represented40Hilbert space. -/41theorem exists_represented_strongSums_of_sourceShells42 (pi : Representation A H)43 (p q w : ℕ → A)44 (hp : ∀ n, IsStarProjection (p n))45 (hq : ∀ n, IsStarProjection (q n))46 (hp0 : p 0 = 1) (hq0 : q 0 = 1)47 (hp_le : ∀ ⦃m n : ℕ⦄, m ≤ n → p m * p n = p n)48 (hq_le : ∀ ⦃m n : ℕ⦄, m ≤ n → q m * q n = q n)49 (hInitial : ∀ n, star (w n) * w n = p n - p (n + 1))50 (hFinal : ∀ n, w n * star (w n) = q n - q (n + 1)) :51 let U : ℕ → Submodule ℂ H := fun n ↦ (pi (p n)).range52 let V : ℕ → Submodule ℂ H := fun n ↦ (pi (q n)).range53 ∃ S T PU PV : H →L[ℂ] H,54 ContinuousLinearMap.StronglyConverges55 (ContinuousLinearMap.partialSum (fun n ↦ pi (w n))) atTop S ∧56 ContinuousLinearMap.StronglyConverges57 (ContinuousLinearMap.partialSum (fun n ↦ (pi (w n))†)) atTop T ∧58 T = S† ∧59 IsStarProjection PU ∧ PU.range = ⨅ n, U n ∧60 IsStarProjection PV ∧ PV.range = ⨅ n, V n ∧61 (S†).comp S = 1 - PU ∧62 S.comp (S†) = 1 - PV := by63 dsimp only64 let U : ℕ → Submodule ℂ H := fun n ↦ (pi (p n)).range65 let V : ℕ → Submodule ℂ H := fun n ↦ (pi (q n)).range66 have hpPi (n : ℕ) : IsStarProjection (pi (p n)) :=67 IsStarProjection.map_representation pi (hp n)68 have hqPi (n : ℕ) : IsStarProjection (pi (q n)) :=69 IsStarProjection.map_representation pi (hq n)70 have hUdata (n : ℕ) : ∃ (_ : (U n).HasOrthogonalProjection),71 pi (p n) = (U n).starProjection := by72 simpa [U] using73 (isStarProjection_iff_eq_starProjection_range.mp (hpPi n))74 have hVdata (n : ℕ) : ∃ (_ : (V n).HasOrthogonalProjection),75 pi (q n) = (V n).starProjection := by76 simpa [V] using77 (isStarProjection_iff_eq_starProjection_range.mp (hqPi n))78 letI hUprojection (n : ℕ) : (U n).HasOrthogonalProjection := (hUdata n).choose79 letI hVprojection (n : ℕ) : (V n).HasOrthogonalProjection := (hVdata n).choose80 have hUproj (n : ℕ) : pi (p n) = (U n).starProjection := (hUdata n).choose_spec81 have hVproj (n : ℕ) : pi (q n) = (V n).starProjection := (hVdata n).choose_spec82 have hUclosed (n : ℕ) : IsClosed (U n : Set H) := by83 exact ContinuousLinearMap.IsIdempotentElem.isClosed_range (hpPi n).isIdempotentElem84 have hVclosed (n : ℕ) : IsClosed (V n : Set H) := by85 exact ContinuousLinearMap.IsIdempotentElem.isClosed_range (hqPi n).isIdempotentElem86 letI : IsClosed ((⨅ n, U n : Submodule ℂ H) : Set H) := by87 simpa only [Submodule.coe_iInf] using isClosed_iInter hUclosed88 letI : IsClosed ((⨅ n, V n : Submodule ℂ H) : Set H) := by89 simpa only [Submodule.coe_iInf] using isClosed_iInter hVclosed90 letI : CompleteSpace (⨅ n, U n : Submodule ℂ H) := inferInstance91 letI : CompleteSpace (⨅ n, V n : Submodule ℂ H) := inferInstance92 letI : (⨅ n, U n).HasOrthogonalProjection := inferInstance93 letI : (⨅ n, V n).HasOrthogonalProjection := inferInstance94 have hUanti : Antitone U := by95 intro m n hmn96 rintro x ⟨y, rfl⟩97 refine ⟨pi (p n) y, ?_⟩98 have heq : pi (p m) * pi (p n) = pi (p n) := by99 rw [← map_mul, hp_le hmn]100 exact congrArg (fun T : H →L[ℂ] H ↦ T y) heq101 have hVanti : Antitone V := by102 intro m n hmn103 rintro x ⟨y, rfl⟩104 refine ⟨pi (q n) y, ?_⟩105 have heq : pi (q m) * pi (q n) = pi (q n) := by106 rw [← map_mul, hq_le hmn]107 exact congrArg (fun T : H →L[ℂ] H ↦ T y) heq108 have hU0 : U 0 = ⊤ := by109 rw [← Submodule.range_starProjection (U 0), ← hUproj, hp0, map_one]110 exact LinearMap.range_eq_top.mpr fun x ↦ ⟨x, rfl⟩111 have hV0 : V 0 = ⊤ := by112 rw [← Submodule.range_starProjection (V 0), ← hVproj, hq0, map_one]113 exact LinearMap.range_eq_top.mpr fun x ↦ ⟨x, rfl⟩114 have hInitialPi (n : ℕ) :115 ((pi (w n))†).comp (pi (w n)) = Submodule.projectionShell U n := by116 change star (pi (w n)) * pi (w n) = _117 rw [← map_star, ← map_mul, hInitial, map_sub, hUproj, hUproj]118 rfl119 have hFinalPi (n : ℕ) :120 (pi (w n)).comp ((pi (w n))†) = Submodule.projectionShell V n := by121 change pi (w n) * star (pi (w n)) = _122 rw [← map_star, ← map_mul, hFinal, map_sub, hVproj, hVproj]123 rfl124 obtain ⟨S, T, hS, hT, _, _, hAdj, hProdU, hProdV⟩ :=125 ContinuousLinearMap.exists_strongSums_of_projectionShells126 (fun n ↦ pi (w n)) U V hUanti hVanti hU0 hV0 hInitialPi hFinalPi127 exact ⟨S, T, (⨅ n, U n).starProjection, (⨅ n, V n).starProjection,128 hS, hT, hAdj, isStarProjection_starProjection, Submodule.range_starProjection _,129 isStarProjection_starProjection, Submodule.range_starProjection _, hProdU, hProdV⟩130131/-- A represented unitary satisfying the finite algebraic shell relations is132reconstructed from strong sums formed afresh on the target Hilbert space.133The complementary operator is supported exactly between the two represented134limiting fixed spaces. In particular, this theorem never maps a strong limit135through `pi`; only the finite source identities are mapped. -/136theorem exists_represented_unitaryCompletion_of_sourceShells137 (pi : Representation A H) (e : H ≃ₗᵢ[ℂ] H)138 (p q w : ℕ → A)139 (hp : ∀ n, IsStarProjection (p n))140 (hq : ∀ n, IsStarProjection (q n))141 (hp0 : p 0 = 1) (hq0 : q 0 = 1)142 (hp_le : ∀ ⦃m n : ℕ⦄, m ≤ n → p m * p n = p n)143 (hq_le : ∀ ⦃m n : ℕ⦄, m ≤ n → q m * q n = q n)144 (hInitial : ∀ n, star (w n) * w n = p n - p (n + 1))145 (hFinal : ∀ n, w n * star (w n) = q n - q (n + 1))146 (hUnitary : ∀ n, (e : H →L[ℂ] H).comp147 (pi (p n - p (n + 1))) = pi (w n)) :148 let U : ℕ → Submodule ℂ H := fun n ↦ (pi (p n)).range149 let V : ℕ → Submodule ℂ H := fun n ↦ (pi (q n)).range150 ∃ S T P Q R : H →L[ℂ] H,151 ContinuousLinearMap.StronglyConverges152 (ContinuousLinearMap.partialSum (fun n ↦ pi (w n))) atTop S ∧153 ContinuousLinearMap.StronglyConverges154 (ContinuousLinearMap.partialSum (fun n ↦ (pi (w n))†)) atTop T ∧155 ‖S‖ ≤ 1 ∧ ‖T‖ ≤ 1 ∧ T = S† ∧156 IsStarProjection P ∧ P.range = ⨅ n, U n ∧157 IsStarProjection Q ∧ Q.range = ⨅ n, V n ∧158 (S†).comp S = 1 - P ∧ S.comp (S†) = 1 - Q ∧159 (e : H →L[ℂ] H) = S + R ∧160 R = (e : H →L[ℂ] H).comp P ∧161 (R†).comp R = P ∧ R.comp (R†) = Q ∧162 R = (Q.comp R).comp P ∧163 (∀ x, x ∈ ⨅ n, U n ↔ e x ∈ ⨅ n, V n) := by164 dsimp only165 let U : ℕ → Submodule ℂ H := fun n ↦ (pi (p n)).range166 let V : ℕ → Submodule ℂ H := fun n ↦ (pi (q n)).range167 have hpPi (n : ℕ) : IsStarProjection (pi (p n)) :=168 IsStarProjection.map_representation pi (hp n)169 have hqPi (n : ℕ) : IsStarProjection (pi (q n)) :=170 IsStarProjection.map_representation pi (hq n)171 have hUdata (n : ℕ) : ∃ (_ : (U n).HasOrthogonalProjection),172 pi (p n) = (U n).starProjection := by173 simpa [U] using174 (isStarProjection_iff_eq_starProjection_range.mp (hpPi n))175 have hVdata (n : ℕ) : ∃ (_ : (V n).HasOrthogonalProjection),176 pi (q n) = (V n).starProjection := by177 simpa [V] using178 (isStarProjection_iff_eq_starProjection_range.mp (hqPi n))179 letI hUprojection (n : ℕ) : (U n).HasOrthogonalProjection :=180 (hUdata n).choose181 letI hVprojection (n : ℕ) : (V n).HasOrthogonalProjection :=182 (hVdata n).choose183 have hUproj (n : ℕ) : pi (p n) = (U n).starProjection :=184 (hUdata n).choose_spec185 have hVproj (n : ℕ) : pi (q n) = (V n).starProjection :=186 (hVdata n).choose_spec187 have hUclosed (n : ℕ) : IsClosed (U n : Set H) :=188 ContinuousLinearMap.IsIdempotentElem.isClosed_range189 (hpPi n).isIdempotentElem190 have hVclosed (n : ℕ) : IsClosed (V n : Set H) :=191 ContinuousLinearMap.IsIdempotentElem.isClosed_range192 (hqPi n).isIdempotentElem193 letI : IsClosed ((⨅ n, U n : Submodule ℂ H) : Set H) := by194 simpa only [Submodule.coe_iInf] using isClosed_iInter hUclosed195 letI : IsClosed ((⨅ n, V n : Submodule ℂ H) : Set H) := by196 simpa only [Submodule.coe_iInf] using isClosed_iInter hVclosed197 letI : CompleteSpace (⨅ n, U n : Submodule ℂ H) := inferInstance198 letI : CompleteSpace (⨅ n, V n : Submodule ℂ H) := inferInstance199 letI : (⨅ n, U n).HasOrthogonalProjection := inferInstance200 letI : (⨅ n, V n).HasOrthogonalProjection := inferInstance201 have hUanti : Antitone U := by202 intro m n hmn203 rintro x ⟨y, rfl⟩204 refine ⟨pi (p n) y, ?_⟩205 have heq : pi (p m) * pi (p n) = pi (p n) := by206 rw [← map_mul, hp_le hmn]207 exact congrArg (fun T : H →L[ℂ] H ↦ T y) heq208 have hVanti : Antitone V := by209 intro m n hmn210 rintro x ⟨y, rfl⟩211 refine ⟨pi (q n) y, ?_⟩212 have heq : pi (q m) * pi (q n) = pi (q n) := by213 rw [← map_mul, hq_le hmn]214 exact congrArg (fun T : H →L[ℂ] H ↦ T y) heq215 have hU0 : U 0 = ⊤ := by216 rw [← Submodule.range_starProjection (U 0), ← hUproj, hp0, map_one]217 exact LinearMap.range_eq_top.mpr fun x ↦ ⟨x, rfl⟩218 have hV0 : V 0 = ⊤ := by219 rw [← Submodule.range_starProjection (V 0), ← hVproj, hq0, map_one]220 exact LinearMap.range_eq_top.mpr fun x ↦ ⟨x, rfl⟩221 have hInitialPi (n : ℕ) :222 ((pi (w n))†).comp (pi (w n)) = Submodule.projectionShell U n := by223 change star (pi (w n)) * pi (w n) = _224 rw [← map_star, ← map_mul, hInitial, map_sub, hUproj, hUproj]225 rfl226 have hFinalPi (n : ℕ) :227 (pi (w n)).comp ((pi (w n))†) = Submodule.projectionShell V n := by228 change pi (w n) * star (pi (w n)) = _229 rw [← map_star, ← map_mul, hFinal, map_sub, hVproj, hVproj]230 rfl231 have hShell (n : ℕ) : pi (p n - p (n + 1)) =232 Submodule.projectionShell U n := by233 rw [map_sub, hUproj, hUproj]234 rfl235 obtain ⟨S, T, hS, hT, hSnorm, hTnorm, hAdj, hProdU, hProdV,236 hcompletion⟩ :=237 ContinuousLinearMap.exists_strongSums_unitaryCompletion_of_projectionShells238 e (fun n ↦ pi (w n)) U V hUanti hVanti hU0 hV0 hInitialPi hFinalPi239 fun n ↦ by240 rw [← hShell]241 exact hUnitary n242 let P : H →L[ℂ] H := (⨅ n, U n).starProjection243 let Q : H →L[ℂ] H := (⨅ n, V n).starProjection244 let R : H →L[ℂ] H := (e : H →L[ℂ] H).comp P245 change (e : H →L[ℂ] H) = S + R ∧246 R = (e : H →L[ℂ] H).comp P ∧247 (R†).comp R = P ∧ R.comp (R†) = Q ∧248 R = (Q.comp R).comp P ∧249 (∀ x, x ∈ ⨅ n, U n ↔ e x ∈ ⨅ n, V n) at hcompletion250 exact ⟨S, T, P, Q, R, hS, hT, hSnorm, hTnorm, hAdj,251 isStarProjection_starProjection, Submodule.range_starProjection _,252 isStarProjection_starProjection, Submodule.range_starProjection _,253 hProdU, hProdV, hcompletion⟩254255end MathlibAnnex.Analysis.CStarAlgebra