ContinuousLinearMap.unitaryCompletion_of_finite_relations

Exact source: MathlibAnnex/Analysis/InnerProductSpace/UnitaryCompletion.lean, lines 121–234.

Raw UTF-8 source

Back to Reconstructing a represented unitary from its shells and residual corner

1import MathlibAnnex.Analysis.InnerProductSpace.ProjectionShell
2
3/-!
4# Exact unitary completion from finite defect relations
5
6A fixed unitary conjugating every finite defect projection conjugates the
7limiting defect projections.  If its complementary finite pieces converge
8strongly to `S`, the remaining corner `V = U P` completes `S` exactly.
9-/
10
11set_option autoImplicit false
12
13open Filter Topology
14open scoped InnerProduct
15
16namespace ContinuousLinearMap
17
18variable {𝕜 E F : Type*}
19variable [RCLike 𝕜]
20variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]
21variable [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F]
22
23/-- Termwise shell relations sum to the corresponding finite relation. -/
24theorem comp_partialSum_eq_of_comp_eq
25    (e : E →L[𝕜] F) (D : ℕ → E →L[𝕜] E) (W : ℕ → E →L[𝕜] F)
26    (h : ∀ n, e.comp (D n) = W n) (N : ℕ) :
27    e.comp (partialSum D N) = partialSum W N := by
28  ext x
29  simp only [partialSum, map_sum, sum_apply,
30    ContinuousLinearMap.comp_apply]
31  apply Finset.sum_congr rfl
32  intro n hn
33  exact congrArg (fun T : E →L[𝕜] F ↦ T x) (h n)
34
35/-- Termwise shells plus a finite telescoping identity give the finite
36complement relation consumed by `unitaryCompletion_of_finite_relations`. -/
37theorem comp_complement_eq_partialSum_of_shells
38    (e : E →L[𝕜] F) (D : ℕ → E →L[𝕜] E) (W : ℕ → E →L[𝕜] F)
39    (U : ℕ → Submodule 𝕜 E) [∀ N, (U N).HasOrthogonalProjection]
40    (hshell : ∀ n, e.comp (D n) = W n)
41    (htelescope : ∀ N, partialSum D N = 1 - (U N).starProjection) :
42    ∀ N, e.comp (1 - (U N).starProjection) = partialSum W N := by
43  intro N
44  rw [← htelescope]
45  exact comp_partialSum_eq_of_comp_eq e D W hshell N
46
47/-- If a unitary's complementary corner has the prescribed final defect product,
48then it conjugates the remaining projection onto the remaining final projection. -/
49theorem unitary_conjugacy_of_complement_product
50    (e : E ≃ₗᵢ[𝕜] F) (P : E →L[𝕜] E) (Q : F →L[𝕜] F)
51    (A : E →L[𝕜] F)
52    (hPadj : P† = P) (hPidem : P.comp P = P)
53    (hA : (e : E →L[𝕜] F).comp (1 - P) = A)
54    (hprod : A.comp (A†) = 1 - Q) :
55    ((e : E →L[𝕜] F).comp P).comp ((e : E →L[𝕜] F)†) = Q := by
56  have hAadj : A† = (1 - P).comp ((e : E →L[𝕜] F)†) := by
57    have h := congrArg (fun T : E →L[𝕜] F ↦ T†) hA
58    simpa [adjoint_comp, map_sub, hPadj] using h.symm
59  have hPapply : ∀ x, P (P x) = P x := by
60    intro x
61    exact congrArg (fun T : E →L[𝕜] E ↦ T x) hPidem
62  have hcompApply : ∀ x, (1 - P) ((1 - P) x) = (1 - P) x := by
63    intro x
64    simp [hPapply]
65  ext y
66  have hprodApply := congrArg (fun T : F →L[𝕜] F ↦ T y) hprod
67  change A ((A†) y) = y - Q y at hprodApply
68  rw [hAadj] at hprodApply
69  change A ((1 - P) (((e : E →L[𝕜] F)†) y)) = y - Q y at hprodApply
70  have hAApply : ∀ x, A x = e ((1 - P) x) := by
71    intro x
72    exact (congrArg (fun T : E →L[𝕜] F ↦ T x) hA).symm
73  rw [hAApply, hcompApply] at hprodApply
74  change e (P (((e : E →L[𝕜] F)†) y)) = Q y
75  have heApply : e (((e : E →L[𝕜] F)†) y) = y := by
76    rw [e.adjoint_eq_symm]
77    exact e.apply_symm_apply y
78  have hdecomp : e ((1 - P) (((e : E →L[𝕜] F)†) y)) =
79      e (((e : E →L[𝕜] F)†) y) - e (P (((e : E →L[𝕜] F)†) y)) := by
80    simp
81  rw [hdecomp, heApply] at hprodApply
82  exact sub_right_inj.mp hprodApply
83
84/-- The raw termwise unitary shell relation and the two shell support identities
85imply every finite unitary conjugacy relation. -/
86theorem unitary_starProjection_conjugacy_of_projectionShells
87    (e : E ≃ₗᵢ[𝕜] F) (W : ℕ → E →L[𝕜] F)
88    (U : ℕ → Submodule 𝕜 E) (V : ℕ → Submodule 𝕜 F)
89    [∀ n, (U n).HasOrthogonalProjection]
90    [∀ n, (V n).HasOrthogonalProjection]
91    (hU : Antitone U) (hV : Antitone V)
92    (hU0 : U 0 = ⊤) (hV0 : V 0 = ⊤)
93    (hInitial : ∀ n, ((W n)†).comp (W n) = Submodule.projectionShell U n)
94    (hFinal : ∀ n, (W n).comp ((W n)†) = Submodule.projectionShell V n)
95    (hUnitary : ∀ n, (e : E →L[𝕜] F).comp (Submodule.projectionShell U n) = W n) :
96    ∀ N, ((e : E →L[𝕜] F).comp (U N).starProjection).comp
97      ((e : E →L[𝕜] F)†) = (V N).starProjection := by
98  intro N
99  have hi := pairwiseInitialOrthogonal_of_projectionShells W U hU hInitial
100  have hfiniteComplement : (e : E →L[𝕜] F).comp (1 - (U N).starProjection) =
101      partialSum W N :=
102    comp_complement_eq_partialSum_of_shells (e : E →L[𝕜] F)
103      (Submodule.projectionShell U) W U hUnitary
104      (Submodule.partialSum_projectionShell U hU0) N
105  have hfiniteProduct : (partialSum W N).comp
106      (partialSum (fun n ↦ (W n)†) N) = 1 - (V N).starProjection := by
107    rw [partialSum_comp_adjoint_partialSum_eq W (Submodule.projectionShell V) hi hFinal,
108      Submodule.partialSum_projectionShell V hV0]
109  have hpartialAdjoint : (partialSum W N)† = partialSum (fun n ↦ (W n)†) N := by
110    exact (partialSum_adjoint W N).symm
111  apply unitary_conjugacy_of_complement_product e (U N).starProjection
112    (V N).starProjection (partialSum W N)
113  · exact (U N).starProjection_isSymmetric.clm_adjoint_eq
114  · exact (U N).isIdempotentElem_starProjection
115  · exact hfiniteComplement
116  · rwa [hpartialAdjoint]
117
118/-- Exact completion of a strong shell limit by the limiting defect corner.
119The two finite hypotheses are precisely the finite complement and finite
120conjugacy relations; all asserted limiting and corner identities are proved. -/
121theorem unitaryCompletion_of_finite_relations
122    (e : E ≃ₗᵢ[𝕜] F) (A : ℕ → E →L[𝕜] F) (S : E →L[𝕜] F)
123    (U : ℕ → Submodule 𝕜 E) (V : ℕ → Submodule 𝕜 F)
124    [∀ N, (U N).HasOrthogonalProjection]
125    [∀ N, (V N).HasOrthogonalProjection]
126    [(⨅ N, U N).HasOrthogonalProjection]
127    [(⨅ N, V N).HasOrthogonalProjection]
128    (hU : Antitone U) (hV : Antitone V)
129    (hA : StronglyConverges A atTop S)
130    (hfiniteComplement : ∀ N,
131      (e : E →L[𝕜] F).comp (1 - (U N).starProjection) = A N)
132    (hfiniteConjugacy : ∀ N,
133      ((e : E →L[𝕜] F).comp (U N).starProjection).comp
134        ((e : E →L[𝕜] F)†) = (V N).starProjection) :
135    let P := (⨅ N, U N).starProjection
136    let Q := (⨅ N, V N).starProjection
137    let R := (e : E →L[𝕜] F).comp P
138    (e : E →L[𝕜] F) = S + R ∧
139      R = (e : E →L[𝕜] F).comp P ∧
140      (R†).comp R = P ∧ R.comp (R†) = Q ∧
141      R = (Q.comp R).comp P ∧
142      (∀ x, x ∈ ⨅ N, U N ↔ e x ∈ ⨅ N, V N) := by
143  dsimp only
144  let P : E →L[𝕜] E := (⨅ N, U N).starProjection
145  let Q : F →L[𝕜] F := (⨅ N, V N).starProjection
146  let R : E →L[𝕜] F := (e : E →L[𝕜] F).comp P
147  have hPlim := Submodule.stronglyConverges_starProjection_iInf U hU
148  have hQlim := Submodule.stronglyConverges_starProjection_iInf V hV
149  have hcompLimit : (e : E →L[𝕜] F).comp (1 - P) = S := by
150    apply ext
151    intro x
152    apply tendsto_nhds_unique (l := (atTop : Filter ℕ))
153    · exact ((StronglyConverges.const (ι := ℕ) (l := atTop)
154        (1 : E →L[𝕜] E)).sub hPlim |>.comp_left (e : E →L[𝕜] F)) x
155    · simpa [hfiniteComplement] using hA x
156  have hconjLimit :
157      ((e : E →L[𝕜] F).comp P).comp ((e : E →L[𝕜] F)†) = Q := by
158    apply ext
159    intro y
160    apply tendsto_nhds_unique (l := (atTop : Filter ℕ))
161    · exact (hPlim.comp_left (e : E →L[𝕜] F) |>.comp_right
162        ((e : E →L[𝕜] F)†)) y
163    · apply Filter.Tendsto.congr'
164        (h := by simpa [Q] using hQlim y)
165      filter_upwards [] with N
166      exact (congrArg (fun T : F →L[𝕜] F ↦ T y)
167        (hfiniteConjugacy N)).symm
168  have hPadj : P† = P := by
169    exact (⨅ N, U N).starProjection_isSymmetric.clm_adjoint_eq
170  have hQadj : Q† = Q := by
171    exact (⨅ N, V N).starProjection_isSymmetric.clm_adjoint_eq
172  have hPidem : P.comp P = P := (⨅ N, U N).isIdempotentElem_starProjection
173  have hQidem : Q.comp Q = Q := (⨅ N, V N).isIdempotentElem_starProjection
174  have hleft : (e : E →L[𝕜] F) = S + R := by
175    apply ext
176    intro x
177    have hx := congrArg (fun T : E →L[𝕜] F ↦ T x) hcompLimit
178    change e ((1 - P) x) = S x at hx
179    calc
180      e x = e ((1 - P) x + P x) := by simp
181      _ = e ((1 - P) x) + e (P x) := map_add e _ _
182      _ = S x + R x := by rw [hx]; rfl
183      _ = (S + R) x := rfl
184  have hPapply : ∀ x, P (P x) = P x := by
185    intro x
186    exact congrArg (fun T : E →L[𝕜] E ↦ T x) hPidem
187  have hRadj : R† = P.comp ((e : E →L[𝕜] F)†) := by
188    simp [R, adjoint_comp, hPadj]
189  have hinitial : (R†).comp R = P := by
190    ext x
191    rw [hRadj]
192    change P (((e : E →L[𝕜] F)†) (e (P x))) = P x
193    rw [LinearIsometryEquiv.adjoint_eq_symm]
194    have he : (e.symm : F →L[𝕜] E) (e (P x)) = P x := by
195      exact e.symm_apply_apply (P x)
196    rw [he]
197    exact hPapply x
198  have hfinal : R.comp (R†) = Q := by
199    ext y
200    have hc := congrArg (fun T : F →L[𝕜] F ↦ T y) hconjLimit
201    change e (P (((e : E →L[𝕜] F)†) y)) = Q y at hc
202    rw [hRadj]
203    change e (P (P (((e : E →L[𝕜] F)†) y))) = Q y
204    rw [hPapply]
205    exact hc
206  have hsupport : R = (Q.comp R).comp P := by
207    have hi : ∀ x, (R†) (R x) = P x := by
208      intro x
209      exact congrArg (fun T : E →L[𝕜] E ↦ T x) hinitial
210    have hf : ∀ y, R ((R†) y) = Q y := by
211      intro y
212      exact congrArg (fun T : F →L[𝕜] F ↦ T y) hfinal
213    ext x
214    calc
215      R x = R (P x) := by
216        dsimp [R]
217        rw [hPapply]
218      _ = R ((R†) (R (P x))) := by rw [hi, hPapply]
219      _ = Q (R (P x)) := hf _
220      _ = ((Q.comp R).comp P) x := rfl
221  have hmem : ∀ x, x ∈ ⨅ N, U N ↔ e x ∈ ⨅ N, V N := by
222    intro x
223    rw [← Submodule.starProjection_eq_self_iff, ← Submodule.starProjection_eq_self_iff]
224    change P x = x ↔ Q (e x) = e x
225    constructor
226    · intro hx
227      have hc := congrArg (fun T : F →L[𝕜] F ↦ T (e x)) hconjLimit
228      simpa [P, Q, ContinuousLinearMap.comp_apply, hx] using hc.symm
229    · intro hx
230      have hc := congrArg (fun T : F →L[𝕜] F ↦ T (e x)) hconjLimit
231      have : e (P x) = e x := by
232        simpa [P, Q, ContinuousLinearMap.comp_apply, hx] using hc
233      exact e.injective this
234  exact ⟨hleft, rfl, hinitial, hfinal, hsupport, hmem⟩
235
236/-- Complete raw-shell entry theorem.  Decreasing normalized projection families,
237the two termwise support products, and the termwise unitary relation suffice to
238construct the strong shell sum and its adjoint and to identify the complementary
239unitary corner.  Finite products, finite conjugacy, and strong convergence are all
240conclusions or internal derived facts, not hypotheses. -/
241theorem exists_strongSums_unitaryCompletion_of_projectionShells
242    (e : E ≃ₗᵢ[𝕜] F) (W : ℕ → E →L[𝕜] F)
243    (U : ℕ → Submodule 𝕜 E) (V : ℕ → Submodule 𝕜 F)
244    [∀ n, (U n).HasOrthogonalProjection]
245    [∀ n, (V n).HasOrthogonalProjection]
246    [(⨅ n, U n).HasOrthogonalProjection]
247    [(⨅ n, V n).HasOrthogonalProjection]
248    (hU : Antitone U) (hV : Antitone V)
249    (hU0 : U 0 = ⊤) (hV0 : V 0 = ⊤)
250    (hInitial : ∀ n, ((W n)†).comp (W n) = Submodule.projectionShell U n)
251    (hFinal : ∀ n, (W n).comp ((W n)†) = Submodule.projectionShell V n)
252    (hUnitary : ∀ n, (e : E →L[𝕜] F).comp (Submodule.projectionShell U n) = W n) :
253    ∃ S : E →L[𝕜] F, ∃ T : F →L[𝕜] E,
254      StronglyConverges (partialSum W) atTop S ∧
255      StronglyConverges (partialSum fun n ↦ (W n)†) atTop T ∧
256      ‖S‖ ≤ 1 ∧ ‖T‖ ≤ 1 ∧ T = S† ∧
257      (S†).comp S = 1 - (⨅ n, U n).starProjection ∧
258      S.comp (S†) = 1 - (⨅ n, V n).starProjection ∧
259      (let P := (⨅ n, U n).starProjection
260       let Q := (⨅ n, V n).starProjection
261       let R := (e : E →L[𝕜] F).comp P
262       (e : E →L[𝕜] F) = S + R ∧
263         R = (e : E →L[𝕜] F).comp P ∧
264         (R†).comp R = P ∧ R.comp (R†) = Q ∧
265         R = (Q.comp R).comp P ∧
266         (∀ x, x ∈ ⨅ n, U n ↔ e x ∈ ⨅ n, V n)) := by
267  obtain ⟨S, T, hS, hT, hSnorm, hTnorm, hAdj, hProdU, hProdV⟩ :=
268    exists_strongSums_of_projectionShells W U V hU hV hU0 hV0 hInitial hFinal
269  have hfiniteComplement : ∀ N,
270      (e : E →L[𝕜] F).comp (1 - (U N).starProjection) = partialSum W N :=
271    comp_complement_eq_partialSum_of_shells (e : E →L[𝕜] F)
272      (Submodule.projectionShell U) W U hUnitary
273      (Submodule.partialSum_projectionShell U hU0)
274  have hfiniteConjugacy : ∀ N,
275      ((e : E →L[𝕜] F).comp (U N).starProjection).comp
276        ((e : E →L[𝕜] F)†) = (V N).starProjection :=
277    unitary_starProjection_conjugacy_of_projectionShells e W U V hU hV hU0 hV0
278      hInitial hFinal hUnitary
279  have hcompletion := unitaryCompletion_of_finite_relations e (partialSum W) S U V
280    hU hV hS hfiniteComplement hfiniteConjugacy
281  exact ⟨S, T, hS, hT, hSnorm, hTnorm, hAdj, hProdU, hProdV, hcompletion⟩
282
283end ContinuousLinearMap