MathlibAnnex/Analysis/InnerProductSpace/UnitaryCompletion.lean

Exact source: MathlibAnnex/Analysis/InnerProductSpace/UnitaryCompletion.lean

Pinned GitHub source · Raw UTF-8 source

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

1import MathlibAnnex.Analysis.InnerProductSpace.ProjectionShell23/-!4# Exact unitary completion from finite defect relations56A fixed unitary conjugating every finite defect projection conjugates the7limiting defect projections.  If its complementary finite pieces converge8strongly to `S`, the remaining corner `V = U P` completes `S` exactly.9-/1011set_option autoImplicit false1213open Filter Topology14open scoped InnerProduct1516namespace ContinuousLinearMap1718variable {𝕜 E F : Type*}19variable [RCLike 𝕜]20variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]21variable [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F]2223/-- Termwise shell relations sum to the corresponding finite relation. -/24theorem comp_partialSum_eq_of_comp_eq25    (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 := by28  ext x29  simp only [partialSum, map_sum, sum_apply,30    ContinuousLinearMap.comp_apply]31  apply Finset.sum_congr rfl32  intro n hn33  exact congrArg (fun T : E →L[𝕜] F ↦ T x) (h n)3435/-- Termwise shells plus a finite telescoping identity give the finite36complement relation consumed by `unitaryCompletion_of_finite_relations`. -/37theorem comp_complement_eq_partialSum_of_shells38    (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 := by43  intro N44  rw [← htelescope]45  exact comp_partialSum_eq_of_comp_eq e D W hshell N4647/-- 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_product50    (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 := by56  have hAadj : A† = (1 - P).comp ((e : E →L[𝕜] F)†) := by57    have h := congrArg (fun T : E →L[𝕜] F ↦ T†) hA58    simpa [adjoint_comp, map_sub, hPadj] using h.symm59  have hPapply : ∀ x, P (P x) = P x := by60    intro x61    exact congrArg (fun T : E →L[𝕜] E ↦ T x) hPidem62  have hcompApply : ∀ x, (1 - P) ((1 - P) x) = (1 - P) x := by63    intro x64    simp [hPapply]65  ext y66  have hprodApply := congrArg (fun T : F →L[𝕜] F ↦ T y) hprod67  change A ((A†) y) = y - Q y at hprodApply68  rw [hAadj] at hprodApply69  change A ((1 - P) (((e : E →L[𝕜] F)†) y)) = y - Q y at hprodApply70  have hAApply : ∀ x, A x = e ((1 - P) x) := by71    intro x72    exact (congrArg (fun T : E →L[𝕜] F ↦ T x) hA).symm73  rw [hAApply, hcompApply] at hprodApply74  change e (P (((e : E →L[𝕜] F)†) y)) = Q y75  have heApply : e (((e : E →L[𝕜] F)†) y) = y := by76    rw [e.adjoint_eq_symm]77    exact e.apply_symm_apply y78  have hdecomp : e ((1 - P) (((e : E →L[𝕜] F)†) y)) =79      e (((e : E →L[𝕜] F)†) y) - e (P (((e : E →L[𝕜] F)†) y)) := by80    simp81  rw [hdecomp, heApply] at hprodApply82  exact sub_right_inj.mp hprodApply8384/-- The raw termwise unitary shell relation and the two shell support identities85imply every finite unitary conjugacy relation. -/86theorem unitary_starProjection_conjugacy_of_projectionShells87    (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).comp97      ((e : E →L[𝕜] F)†) = (V N).starProjection := by98  intro N99  have hi := pairwiseInitialOrthogonal_of_projectionShells W U hU hInitial100  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 hUnitary104      (Submodule.partialSum_projectionShell U hU0) N105  have hfiniteProduct : (partialSum W N).comp106      (partialSum (fun n ↦ (W n)†) N) = 1 - (V N).starProjection := by107    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 := by110    exact (partialSum_adjoint W N).symm111  apply unitary_conjugacy_of_complement_product e (U N).starProjection112    (V N).starProjection (partialSum W N)113  · exact (U N).starProjection_isSymmetric.clm_adjoint_eq114  · exact (U N).isIdempotentElem_starProjection115  · exact hfiniteComplement116  · rwa [hpartialAdjoint]117118/-- Exact completion of a strong shell limit by the limiting defect corner.119The two finite hypotheses are precisely the finite complement and finite120conjugacy relations; all asserted limiting and corner identities are proved. -/121theorem unitaryCompletion_of_finite_relations122    (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).comp134        ((e : E →L[𝕜] F)†) = (V N).starProjection) :135    let P := (⨅ N, U N).starProjection136    let Q := (⨅ N, V N).starProjection137    let R := (e : E →L[𝕜] F).comp P138    (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) := by143  dsimp only144  let P : E →L[𝕜] E := (⨅ N, U N).starProjection145  let Q : F →L[𝕜] F := (⨅ N, V N).starProjection146  let R : E →L[𝕜] F := (e : E →L[𝕜] F).comp P147  have hPlim := Submodule.stronglyConverges_starProjection_iInf U hU148  have hQlim := Submodule.stronglyConverges_starProjection_iInf V hV149  have hcompLimit : (e : E →L[𝕜] F).comp (1 - P) = S := by150    apply ext151    intro x152    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)) x155    · simpa [hfiniteComplement] using hA x156  have hconjLimit :157      ((e : E →L[𝕜] F).comp P).comp ((e : E →L[𝕜] F)†) = Q := by158    apply ext159    intro y160    apply tendsto_nhds_unique (l := (atTop : Filter ℕ))161    · exact (hPlim.comp_left (e : E →L[𝕜] F) |>.comp_right162        ((e : E →L[𝕜] F)†)) y163    · apply Filter.Tendsto.congr'164        (h := by simpa [Q] using hQlim y)165      filter_upwards [] with N166      exact (congrArg (fun T : F →L[𝕜] F ↦ T y)167        (hfiniteConjugacy N)).symm168  have hPadj : P† = P := by169    exact (⨅ N, U N).starProjection_isSymmetric.clm_adjoint_eq170  have hQadj : Q† = Q := by171    exact (⨅ N, V N).starProjection_isSymmetric.clm_adjoint_eq172  have hPidem : P.comp P = P := (⨅ N, U N).isIdempotentElem_starProjection173  have hQidem : Q.comp Q = Q := (⨅ N, V N).isIdempotentElem_starProjection174  have hleft : (e : E →L[𝕜] F) = S + R := by175    apply ext176    intro x177    have hx := congrArg (fun T : E →L[𝕜] F ↦ T x) hcompLimit178    change e ((1 - P) x) = S x at hx179    calc180      e x = e ((1 - P) x + P x) := by simp181      _ = e ((1 - P) x) + e (P x) := map_add e _ _182      _ = S x + R x := by rw [hx]; rfl183      _ = (S + R) x := rfl184  have hPapply : ∀ x, P (P x) = P x := by185    intro x186    exact congrArg (fun T : E →L[𝕜] E ↦ T x) hPidem187  have hRadj : R† = P.comp ((e : E →L[𝕜] F)†) := by188    simp [R, adjoint_comp, hPadj]189  have hinitial : (R†).comp R = P := by190    ext x191    rw [hRadj]192    change P (((e : E →L[𝕜] F)†) (e (P x))) = P x193    rw [LinearIsometryEquiv.adjoint_eq_symm]194    have he : (e.symm : F →L[𝕜] E) (e (P x)) = P x := by195      exact e.symm_apply_apply (P x)196    rw [he]197    exact hPapply x198  have hfinal : R.comp (R†) = Q := by199    ext y200    have hc := congrArg (fun T : F →L[𝕜] F ↦ T y) hconjLimit201    change e (P (((e : E →L[𝕜] F)†) y)) = Q y at hc202    rw [hRadj]203    change e (P (P (((e : E →L[𝕜] F)†) y))) = Q y204    rw [hPapply]205    exact hc206  have hsupport : R = (Q.comp R).comp P := by207    have hi : ∀ x, (R†) (R x) = P x := by208      intro x209      exact congrArg (fun T : E →L[𝕜] E ↦ T x) hinitial210    have hf : ∀ y, R ((R†) y) = Q y := by211      intro y212      exact congrArg (fun T : F →L[𝕜] F ↦ T y) hfinal213    ext x214    calc215      R x = R (P x) := by216        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 := rfl221  have hmem : ∀ x, x ∈ ⨅ N, U N ↔ e x ∈ ⨅ N, V N := by222    intro x223    rw [← Submodule.starProjection_eq_self_iff, ← Submodule.starProjection_eq_self_iff]224    change P x = x ↔ Q (e x) = e x225    constructor226    · intro hx227      have hc := congrArg (fun T : F →L[𝕜] F ↦ T (e x)) hconjLimit228      simpa [P, Q, ContinuousLinearMap.comp_apply, hx] using hc.symm229    · intro hx230      have hc := congrArg (fun T : F →L[𝕜] F ↦ T (e x)) hconjLimit231      have : e (P x) = e x := by232        simpa [P, Q, ContinuousLinearMap.comp_apply, hx] using hc233      exact e.injective this234  exact ⟨hleft, rfl, hinitial, hfinal, hsupport, hmem⟩235236/-- Complete raw-shell entry theorem.  Decreasing normalized projection families,237the two termwise support products, and the termwise unitary relation suffice to238construct the strong shell sum and its adjoint and to identify the complementary239unitary corner.  Finite products, finite conjugacy, and strong convergence are all240conclusions or internal derived facts, not hypotheses. -/241theorem exists_strongSums_unitaryCompletion_of_projectionShells242    (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).starProjection260       let Q := (⨅ n, V n).starProjection261       let R := (e : E →L[𝕜] F).comp P262       (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)) := by267  obtain ⟨S, T, hS, hT, hSnorm, hTnorm, hAdj, hProdU, hProdV⟩ :=268    exists_strongSums_of_projectionShells W U V hU hV hU0 hV0 hInitial hFinal269  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 hUnitary273      (Submodule.partialSum_projectionShell U hU0)274  have hfiniteConjugacy : ∀ N,275      ((e : E →L[𝕜] F).comp (U N).starProjection).comp276        ((e : E →L[𝕜] F)†) = (V N).starProjection :=277    unitary_starProjection_conjugacy_of_projectionShells e W U V hU hV hU0 hV0278      hInitial hFinal hUnitary279  have hcompletion := unitaryCompletion_of_finite_relations e (partialSum W) S U V280    hU hV hS hfiniteComplement hfiniteConjugacy281  exact ⟨S, T, hS, hT, hSnorm, hTnorm, hAdj, hProdU, hProdV, hcompletion⟩282283end ContinuousLinearMap