MatrixCornerFrames.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A finite family of partial isometries with common initial projection constructs the actual Hilbert coordinate frame of a corner.

theorem OAI.KadisonSimilarity.mul_initial_projection line 14
Source documentation
An algebraic partial isometry is unchanged by its initial projection.
```
theorem mul_initial_projection (e v : P) (he : IsStarProjection e) (hv : star v * v = e) :
    v * e = v := by
…
```

def OAI.KadisonSimilarity.partialIsometryColumns line 31

Source documentation

The columns are multiplication by the partial isometries after the isometric inclusion of the initial corner.

def partialIsometryColumns (L : P →⋆ₐ[ℂ] (H →L[ℂ] H))
    (e : P) (he : IsStarProjection e) {n : ℕ} (v : Fin n → P)
    (hv : ∀ i j, star (v i) * v j = if i = j then e else 0)
    (hsum : ∑ i, v i * star (v i) = 1)
    (I : F →ₗᵢ[ℂ] H)
    (hI : I.toContinuousLinearMap.comp I.toContinuousLinearMap.adjoint = L e) :
    FiniteOrthogonalColumns F H n where
…

Mentions: OAI.KadisonSimilarity.FiniteOrthogonalColumns

theorem OAI.KadisonSimilarity.partialIsometryColumns_entry line 68

Source documentation

The matrix entries of the represented algebra are the algebraic corner compressions by the same partial isometries.

theorem partialIsometryColumns_entry
    (L : P →⋆ₐ[ℂ] (H →L[ℂ] H)) (e : P) (he : IsStarProjection e)
    {n : ℕ} (v : Fin n → P)
    (hv : ∀ i j, star (v i) * v j = if i = j then e else 0)
    (hsum : ∑ i, v i * star (v i) = 1) (I : F →ₗᵢ[ℂ] H)
    (hI : I.toContinuousLinearMap.comp I.toContinuousLinearMap.adjoint = L e)
    (a : P) (i j : Fin n) :
    ((partialIsometryColumns L e he v hv hsum I hI).inclusion i).adjoint.comp
      ((L a).comp ((partialIsometryColumns L e he v hv hsum I hI).inclusion j)) =
      I.toContinuousLinearMap.adjoint.comp
        ((L (star (v i) * a * v j)).comp I.toContinuousLinearMap) := by
…

Mentions: OAI.KadisonSimilarity.partialIsometryColumns