Exact source: MathlibAnnex/Analysis/InnerProductSpace/RankOneCompletion.lean, lines 200–200.
Back to An irreducible operator algebra constructed from projection shells
1import MathlibAnnex.Analysis.InnerProductSpace.RankOne 2import MathlibAnnex.Analysis.InnerProductSpace.ProjectionShell 3import MathlibAnnex.Analysis.InnerProductSpace.UnitaryCompletion 4 5/-! 6# Rank-one completion of a one-dimensional defect 7 8The input operator has initial and final defects equal to the projections onto 9two displayed unit vectors. The missing rank-one link completes it to a 10unitary. In particular, no cross-term vanishing is assumed: it is derived 11from the two defect-product identities. 12-/ 13 14set_option autoImplicit false 15 16open Filter Topology 17open scoped InnerProduct 18 19namespace ContinuousLinearMap 20 21variable {H : Type*} 22variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 23 24/-- The initial defect identity forces the partial isometry to vanish on its 25displayed initial defect vector. -/ 26theorem apply_eq_zero_of_adjoint_comp_eq_one_sub_rankOne 27 (S : H →L[ℂ] H) (b : H) (hb : ‖b‖ = 1) 28 (hS : (S†).comp S = 1 - InnerProductSpace.rankOne ℂ b b) : 29 S b = 0 := by 30 have hnorm : ‖S b‖ ^ 2 = 0 := by 31 rw [apply_norm_sq_eq_inner_adjoint_left, hS] 32 simp [InnerProductSpace.rankOne_apply, inner_self_eq_norm_sq_to_K, hb] 33 exact norm_eq_zero.mp (sq_eq_zero_iff.mp hnorm) 34 35/-- The final defect identity forces the adjoint partial isometry to vanish on 36its displayed final defect vector. -/ 37theorem adjoint_apply_eq_zero_of_comp_adjoint_eq_one_sub_rankOne 38 (S : H →L[ℂ] H) (a : H) (ha : ‖a‖ = 1) 39 (hS : S.comp (S†) = 1 - InnerProductSpace.rankOne ℂ a a) : 40 (S†) a = 0 := by 41 have hnorm : ‖(S†) a‖ ^ 2 = 0 := by 42 rw [apply_norm_sq_eq_inner_adjoint_left, adjoint_adjoint, hS] 43 simp [InnerProductSpace.rankOne_apply, inner_self_eq_norm_sq_to_K, ha] 44 exact norm_eq_zero.mp (sq_eq_zero_iff.mp hnorm) 45 46/-- A partial isometry with displayed one-dimensional initial and final 47defects becomes a unitary after adding the rank-one link from `b` to `a`. 48The conclusion also records its action on the source defect vector. -/ 49theorem add_rankOne_mem_unitary 50 (S : H →L[ℂ] H) (a b : H) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) 51 (hInitial : (S†).comp S = 1 - InnerProductSpace.rankOne ℂ b b) 52 (hFinal : S.comp (S†) = 1 - InnerProductSpace.rankOne ℂ a a) : 53 S + InnerProductSpace.rankOne ℂ a b ∈ unitary (H →L[ℂ] H) ∧ 54 (S + InnerProductSpace.rankOne ℂ a b) b = a := by 55 let V : H →L[ℂ] H := InnerProductSpace.rankOne ℂ a b 56 let P : H →L[ℂ] H := InnerProductSpace.rankOne ℂ b b 57 let Q : H →L[ℂ] H := InnerProductSpace.rankOne ℂ a a 58 have hSb : S b = 0 := 59 apply_eq_zero_of_adjoint_comp_eq_one_sub_rankOne S b hb hInitial 60 have hSa : (S†) a = 0 := 61 adjoint_apply_eq_zero_of_comp_adjoint_eq_one_sub_rankOne S a ha hFinal 62 have hVstar : V† = InnerProductSpace.rankOne ℂ b a := by 63 simpa [V] using InnerProductSpace.adjoint_rankOne a b 64 have hSVstar : S.comp (V†) = 0 := by 65 rw [hVstar, InnerProductSpace.comp_rankOne, hSb] 66 simp 67 have hVstarS : (V†).comp S = 0 := by 68 rw [hVstar, InnerProductSpace.rankOne_comp, hSa] 69 simp 70 have hSstarV : (S†).comp V = 0 := by 71 dsimp [V] 72 rw [InnerProductSpace.comp_rankOne, hSa] 73 simp 74 have hVSstar : V.comp (S†) = 0 := by 75 dsimp [V] 76 rw [InnerProductSpace.rankOne_comp, adjoint_adjoint, hSb] 77 simp 78 have hVstarV : (V†).comp V = P := by 79 ext x 80 simp [V, P, InnerProductSpace.rankOne_apply, 81 InnerProductSpace.adjoint_rankOne, ha] 82 have hVVstar : V.comp (V†) = Q := by 83 ext x 84 simp [V, Q, InnerProductSpace.rankOne_apply, 85 InnerProductSpace.adjoint_rankOne, hb] 86 constructor 87 · rw [Unitary.mem_iff] 88 constructor 89 · change (S + V)† * (S + V) = 1 90 rw [map_add] 91 calc 92 (S† + V†) * (S + V) = 93 ((S†).comp S + (S†).comp V) + 94 ((V†).comp S + (V†).comp V) := by 95 ext x 96 simp [ContinuousLinearMap.mul_apply] 97 _ = 1 := by 98 rw [hInitial, hSstarV, hVstarS, hVstarV] 99 simp [P] 100 · change (S + V) * (S + V)† = 1 101 rw [map_add] 102 calc 103 (S + V) * (S† + V†) = 104 (S.comp (S†) + S.comp (V†)) + 105 (V.comp (S†) + V.comp (V†)) := by 106 ext x 107 simp [ContinuousLinearMap.mul_apply] 108 _ = 1 := by 109 rw [hFinal, hSVstar, hVSstar, hVVstar] 110 simp [Q] 111 · change S b + V b = a 112 rw [hSb] 113 simp [V, InnerProductSpace.rankOne_apply, 114 inner_self_eq_norm_sq_to_K, hb] 115 116/-- A strong sum of supported projection shells restricts to the original 117shell map on every shell. -/ 118theorem StronglyConverges.comp_projectionShell_eq 119 (W : ℕ → H →L[ℂ] H) (U : ℕ → Submodule ℂ H) 120 [∀ n, (U n).HasOrthogonalProjection] 121 (hU : Antitone U) 122 (hInitial : ∀ n, ((W n)†).comp (W n) = Submodule.projectionShell U n) 123 (S : H →L[ℂ] H) (hS : StronglyConverges (partialSum W) atTop S) 124 (n : ℕ) : 125 S.comp (Submodule.projectionShell U n) = W n := by 126 have horth := pairwiseInitialOrthogonal_of_projectionShells W U hU hInitial 127 have hsupport : (W n).comp (Submodule.projectionShell U n) = W n := 128 comp_projection_eq_self_of_adjoint_comp_self_eq 129 (W n) (Submodule.projectionShell U n) 130 (Submodule.projectionShell_adjoint U n) 131 (Submodule.projectionShell_idempotent U hU n) (hInitial n) 132 have hpartial {N : ℕ} (hN : n < N) : 133 (partialSum W N).comp (Submodule.projectionShell U n) = W n := by 134 rw [partialSum, finsetSum_comp, Finset.sum_eq_single n] 135 · exact hsupport 136 · intro m hm hmn 137 calc 138 (W m).comp (Submodule.projectionShell U n) = 139 ((W m).comp ((W n)†)).comp (W n) := by 140 rw [← hInitial n] 141 rfl 142 _ = 0 := by rw [horth hmn]; simp 143 · intro hnmem 144 exact (hnmem (Finset.mem_range.mpr hN)).elim 145 apply ContinuousLinearMap.ext 146 intro x 147 apply tendsto_nhds_unique ((hS.comp_right (Submodule.projectionShell U n)) x) 148 refine Filter.Tendsto.congr' ?_ tendsto_const_nhds 149 exact Filter.eventually_atTop.2 ⟨n + 1, fun N hN ↦ 150 congrArg (fun T : H →L[ℂ] H ↦ T x) 151 (hpartial (Nat.lt_of_succ_le hN)).symm⟩ 152 153/-- A bounded operator which fixes every shell of a normalized decreasing 154projection flag and fixes the unit vector spanning the limiting defect is the 155identity. This is the root-normalization argument: fixing the defect vector 156alone is not used as a substitute for fixing the complementary shell sum. -/ 157theorem eq_one_of_comp_projectionShell_eq_self_of_rankOne_iInf 158 (L : H →L[ℂ] H) (U : ℕ → Submodule ℂ H) 159 [∀ n, (U n).HasOrthogonalProjection] 160 [(⨅ n, U n).HasOrthogonalProjection] 161 (hU : Antitone U) (hU0 : U 0 = ⊤) 162 (b : H) (hb : ‖b‖ = 1) 163 (hUinf : (⨅ n, U n).starProjection = 164 InnerProductSpace.rankOne ℂ b b) 165 (hShell : ∀ n, L.comp (Submodule.projectionShell U n) = 166 Submodule.projectionShell U n) 167 (hLb : L b = b) : 168 L = 1 := by 169 let P : H →L[ℂ] H := (⨅ n, U n).starProjection 170 have hComplement : StronglyConverges 171 (fun n ↦ 1 - (U n).starProjection) atTop (1 - P) := 172 (StronglyConverges.const (ι := ℕ) (l := atTop) (1 : H →L[ℂ] H)).sub 173 (Submodule.stronglyConverges_starProjection_iInf U hU) 174 have hFinite (N : ℕ) : 175 L.comp (1 - (U N).starProjection) = 1 - (U N).starProjection := by 176 rw [← Submodule.partialSum_projectionShell U hU0] 177 exact comp_partialSum_eq_of_comp_eq L 178 (Submodule.projectionShell U) (Submodule.projectionShell U) hShell N 179 apply ContinuousLinearMap.ext 180 intro x 181 have hComplementFixed : L ((1 - P) x) = (1 - P) x := by 182 apply tendsto_nhds_unique ((hComplement.comp_left L) x) 183 refine (hComplement x).congr' ?_ 184 filter_upwards [] with N 185 exact congrArg (fun T : H →L[ℂ] H ↦ T x) (hFinite N).symm 186 have hDefectFixed : L (P x) = P x := by 187 change L ((⨅ n, U n).starProjection x) = 188 (⨅ n, U n).starProjection x 189 rw [hUinf] 190 simp [InnerProductSpace.rankOne_apply, hLb] 191 calc 192 L x = L ((1 - P) x + P x) := by simp 193 _ = L ((1 - P) x) + L (P x) := map_add L _ _ 194 _ = (1 - P) x + P x := by rw [hComplementFixed, hDefectFixed] 195 _ = x := by simp 196 197/-- Raw decreasing projection-shell data whose limiting defects are two 198displayed unit-vector lines yields an actual unitary rank-one completion. 199Both strong sums and the completed unitary are conclusions. -/ 200theorem exists_rankOneCompletion_of_projectionShells 201 (W : ℕ → H →L[ℂ] H) 202 (U V : ℕ → Submodule ℂ H) 203 [∀ n, (U n).HasOrthogonalProjection] 204 [∀ n, (V n).HasOrthogonalProjection] 205 [(⨅ n, U n).HasOrthogonalProjection] 206 [(⨅ n, V n).HasOrthogonalProjection] 207 (hU : Antitone U) (hV : Antitone V) 208 (hU0 : U 0 = ⊤) (hV0 : V 0 = ⊤) 209 (hInitial : ∀ n, ((W n)†).comp (W n) = Submodule.projectionShell U n) 210 (hFinal : ∀ n, (W n).comp ((W n)†) = Submodule.projectionShell V n) 211 (a b : H) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) 212 (hUinf : (⨅ n, U n).starProjection = InnerProductSpace.rankOne ℂ b b) 213 (hVinf : (⨅ n, V n).starProjection = InnerProductSpace.rankOne ℂ a a) : 214 ∃ S : H →L[ℂ] H, 215 StronglyConverges (partialSum W) atTop S ∧ 216 (S + InnerProductSpace.rankOne ℂ a b) ∈ unitary (H →L[ℂ] H) ∧ 217 (S + InnerProductSpace.rankOne ℂ a b) b = a ∧ 218 ∀ n, (S + InnerProductSpace.rankOne ℂ a b).comp 219 (Submodule.projectionShell U n) = W n := by 220 obtain ⟨S, _, hS, _, _, _, _, hProdU, hProdV⟩ := 221 exists_strongSums_of_projectionShells 222 W U V hU hV hU0 hV0 hInitial hFinal 223 have hInitialS : (S†).comp S = 224 1 - InnerProductSpace.rankOne ℂ b b := by 225 simpa [hUinf] using hProdU 226 have hFinalS : S.comp (S†) = 227 1 - InnerProductSpace.rankOne ℂ a a := by 228 simpa [hVinf] using hProdV 229 obtain ⟨hunitary, hmap⟩ := 230 add_rankOne_mem_unitary S a b ha hb hInitialS hFinalS 231 refine ⟨S, hS, hunitary, hmap, ?_⟩ 232 intro n 233 have hSshell := StronglyConverges.comp_projectionShell_eq 234 W U hU hInitial S hS n 235 have hbmem : b ∈ ⨅ k, U k := by 236 apply (⨅ k, U k).starProjection_eq_self_iff.mp 237 rw [hUinf] 238 simp [InnerProductSpace.rankOne_apply, 239 inner_self_eq_norm_sq_to_K, hb] 240 have hbshell : Submodule.projectionShell U n b = 0 := by 241 have hball : ∀ k, b ∈ U k := (Submodule.mem_iInf U).mp hbmem 242 have hbn : b ∈ U n := hball n 243 have hbnext : b ∈ U (n + 1) := hball (n + 1) 244 simp [Submodule.projectionShell, 245 Submodule.starProjection_eq_self_iff.mpr hbn, 246 Submodule.starProjection_eq_self_iff.mpr hbnext] 247 have hrank : (InnerProductSpace.rankOne ℂ a b).comp 248 (Submodule.projectionShell U n) = 0 := by 249 rw [InnerProductSpace.rankOne_comp, 250 Submodule.projectionShell_adjoint, hbshell] 251 simp 252 rw [add_comp, hSshell, hrank, add_zero] 253 254end ContinuousLinearMap