OAI/Analysis/KadisonKastler/PartialIsometryCorner.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A partial isometry between two isometrically embedded Hilbert spaces

  1. theorem OAI.KadisonKastler.corner_adjoint_comp line 15
  2. def OAI.KadisonKastler.partialIsometryCornerEquiv line 38

    Source documentation

    Compress a partial isometry whose initial and final projections are the two range projections.

    def partialIsometryCornerEquiv (U : H →ₗᵢ[ℂ] E) (V : K →ₗᵢ[ℂ] E) (W : E →L[ℂ] E)
    (hU : W.adjoint.comp W = U.toContinuousLinearMap.comp U.toContinuousLinearMap.adjoint)
    (hV : W.comp W.adjoint = V.toContinuousLinearMap.comp V.toContinuousLinearMap.adjoint) :
    H ≃ₗᵢ[ℂ] K := by
…
  3. theorem OAI.KadisonKastler.partialIsometryCornerEquiv_apply line 54