Exact source: MathlibAnnex/Analysis/InnerProductSpace/RankOneCompletion.lean
Pinned GitHub source · Raw UTF-8 source
Back to An irreducible operator algebra constructed from projection shells
1import MathlibAnnex.Analysis.InnerProductSpace.RankOne2import MathlibAnnex.Analysis.InnerProductSpace.ProjectionShell3import MathlibAnnex.Analysis.InnerProductSpace.UnitaryCompletion45/-!6# Rank-one completion of a one-dimensional defect78The input operator has initial and final defects equal to the projections onto9two displayed unit vectors. The missing rank-one link completes it to a10unitary. In particular, no cross-term vanishing is assumed: it is derived11from the two defect-product identities.12-/1314set_option autoImplicit false1516open Filter Topology17open scoped InnerProduct1819namespace ContinuousLinearMap2021variable {H : Type*}22variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2324/-- The initial defect identity forces the partial isometry to vanish on its25displayed initial defect vector. -/26theorem apply_eq_zero_of_adjoint_comp_eq_one_sub_rankOne27 (S : H →L[ℂ] H) (b : H) (hb : ‖b‖ = 1)28 (hS : (S†).comp S = 1 - InnerProductSpace.rankOne ℂ b b) :29 S b = 0 := by30 have hnorm : ‖S b‖ ^ 2 = 0 := by31 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)3435/-- The final defect identity forces the adjoint partial isometry to vanish on36its displayed final defect vector. -/37theorem adjoint_apply_eq_zero_of_comp_adjoint_eq_one_sub_rankOne38 (S : H →L[ℂ] H) (a : H) (ha : ‖a‖ = 1)39 (hS : S.comp (S†) = 1 - InnerProductSpace.rankOne ℂ a a) :40 (S†) a = 0 := by41 have hnorm : ‖(S†) a‖ ^ 2 = 0 := by42 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)4546/-- A partial isometry with displayed one-dimensional initial and final47defects 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_unitary50 (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 := by55 let V : H →L[ℂ] H := InnerProductSpace.rankOne ℂ a b56 let P : H →L[ℂ] H := InnerProductSpace.rankOne ℂ b b57 let Q : H →L[ℂ] H := InnerProductSpace.rankOne ℂ a a58 have hSb : S b = 0 :=59 apply_eq_zero_of_adjoint_comp_eq_one_sub_rankOne S b hb hInitial60 have hSa : (S†) a = 0 :=61 adjoint_apply_eq_zero_of_comp_adjoint_eq_one_sub_rankOne S a ha hFinal62 have hVstar : V† = InnerProductSpace.rankOne ℂ b a := by63 simpa [V] using InnerProductSpace.adjoint_rankOne a b64 have hSVstar : S.comp (V†) = 0 := by65 rw [hVstar, InnerProductSpace.comp_rankOne, hSb]66 simp67 have hVstarS : (V†).comp S = 0 := by68 rw [hVstar, InnerProductSpace.rankOne_comp, hSa]69 simp70 have hSstarV : (S†).comp V = 0 := by71 dsimp [V]72 rw [InnerProductSpace.comp_rankOne, hSa]73 simp74 have hVSstar : V.comp (S†) = 0 := by75 dsimp [V]76 rw [InnerProductSpace.rankOne_comp, adjoint_adjoint, hSb]77 simp78 have hVstarV : (V†).comp V = P := by79 ext x80 simp [V, P, InnerProductSpace.rankOne_apply,81 InnerProductSpace.adjoint_rankOne, ha]82 have hVVstar : V.comp (V†) = Q := by83 ext x84 simp [V, Q, InnerProductSpace.rankOne_apply,85 InnerProductSpace.adjoint_rankOne, hb]86 constructor87 · rw [Unitary.mem_iff]88 constructor89 · change (S + V)† * (S + V) = 190 rw [map_add]91 calc92 (S† + V†) * (S + V) =93 ((S†).comp S + (S†).comp V) +94 ((V†).comp S + (V†).comp V) := by95 ext x96 simp [ContinuousLinearMap.mul_apply]97 _ = 1 := by98 rw [hInitial, hSstarV, hVstarS, hVstarV]99 simp [P]100 · change (S + V) * (S + V)† = 1101 rw [map_add]102 calc103 (S + V) * (S† + V†) =104 (S.comp (S†) + S.comp (V†)) +105 (V.comp (S†) + V.comp (V†)) := by106 ext x107 simp [ContinuousLinearMap.mul_apply]108 _ = 1 := by109 rw [hFinal, hSVstar, hVSstar, hVVstar]110 simp [Q]111 · change S b + V b = a112 rw [hSb]113 simp [V, InnerProductSpace.rankOne_apply,114 inner_self_eq_norm_sq_to_K, hb]115116/-- A strong sum of supported projection shells restricts to the original117shell map on every shell. -/118theorem StronglyConverges.comp_projectionShell_eq119 (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 := by126 have horth := pairwiseInitialOrthogonal_of_projectionShells W U hU hInitial127 have hsupport : (W n).comp (Submodule.projectionShell U n) = W n :=128 comp_projection_eq_self_of_adjoint_comp_self_eq129 (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 := by134 rw [partialSum, finsetSum_comp, Finset.sum_eq_single n]135 · exact hsupport136 · intro m hm hmn137 calc138 (W m).comp (Submodule.projectionShell U n) =139 ((W m).comp ((W n)†)).comp (W n) := by140 rw [← hInitial n]141 rfl142 _ = 0 := by rw [horth hmn]; simp143 · intro hnmem144 exact (hnmem (Finset.mem_range.mpr hN)).elim145 apply ContinuousLinearMap.ext146 intro x147 apply tendsto_nhds_unique ((hS.comp_right (Submodule.projectionShell U n)) x)148 refine Filter.Tendsto.congr' ?_ tendsto_const_nhds149 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⟩152153/-- A bounded operator which fixes every shell of a normalized decreasing154projection flag and fixes the unit vector spanning the limiting defect is the155identity. This is the root-normalization argument: fixing the defect vector156alone is not used as a substitute for fixing the complementary shell sum. -/157theorem eq_one_of_comp_projectionShell_eq_self_of_rankOne_iInf158 (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 := by169 let P : H →L[ℂ] H := (⨅ n, U n).starProjection170 have hComplement : StronglyConverges171 (fun n ↦ 1 - (U n).starProjection) atTop (1 - P) :=172 (StronglyConverges.const (ι := ℕ) (l := atTop) (1 : H →L[ℂ] H)).sub173 (Submodule.stronglyConverges_starProjection_iInf U hU)174 have hFinite (N : ℕ) :175 L.comp (1 - (U N).starProjection) = 1 - (U N).starProjection := by176 rw [← Submodule.partialSum_projectionShell U hU0]177 exact comp_partialSum_eq_of_comp_eq L178 (Submodule.projectionShell U) (Submodule.projectionShell U) hShell N179 apply ContinuousLinearMap.ext180 intro x181 have hComplementFixed : L ((1 - P) x) = (1 - P) x := by182 apply tendsto_nhds_unique ((hComplement.comp_left L) x)183 refine (hComplement x).congr' ?_184 filter_upwards [] with N185 exact congrArg (fun T : H →L[ℂ] H ↦ T x) (hFinite N).symm186 have hDefectFixed : L (P x) = P x := by187 change L ((⨅ n, U n).starProjection x) =188 (⨅ n, U n).starProjection x189 rw [hUinf]190 simp [InnerProductSpace.rankOne_apply, hLb]191 calc192 L x = L ((1 - P) x + P x) := by simp193 _ = L ((1 - P) x) + L (P x) := map_add L _ _194 _ = (1 - P) x + P x := by rw [hComplementFixed, hDefectFixed]195 _ = x := by simp196197/-- Raw decreasing projection-shell data whose limiting defects are two198displayed unit-vector lines yields an actual unitary rank-one completion.199Both strong sums and the completed unitary are conclusions. -/200theorem exists_rankOneCompletion_of_projectionShells201 (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).comp219 (Submodule.projectionShell U n) = W n := by220 obtain ⟨S, _, hS, _, _, _, _, hProdU, hProdV⟩ :=221 exists_strongSums_of_projectionShells222 W U V hU hV hU0 hV0 hInitial hFinal223 have hInitialS : (S†).comp S =224 1 - InnerProductSpace.rankOne ℂ b b := by225 simpa [hUinf] using hProdU226 have hFinalS : S.comp (S†) =227 1 - InnerProductSpace.rankOne ℂ a a := by228 simpa [hVinf] using hProdV229 obtain ⟨hunitary, hmap⟩ :=230 add_rankOne_mem_unitary S a b ha hb hInitialS hFinalS231 refine ⟨S, hS, hunitary, hmap, ?_⟩232 intro n233 have hSshell := StronglyConverges.comp_projectionShell_eq234 W U hU hInitial S hS n235 have hbmem : b ∈ ⨅ k, U k := by236 apply (⨅ k, U k).starProjection_eq_self_iff.mp237 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 := by241 have hball : ∀ k, b ∈ U k := (Submodule.mem_iInf U).mp hbmem242 have hbn : b ∈ U n := hball n243 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).comp248 (Submodule.projectionShell U n) = 0 := by249 rw [InnerProductSpace.rankOne_comp,250 Submodule.projectionShell_adjoint, hbshell]251 simp252 rw [add_comp, hSshell, hrank, add_zero]253254end ContinuousLinearMap