HilbertSumIsometries.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinate isometries preserve orthogonality when composing a Hilbert sum.

theorem OAI.KadisonSimilarity.orthogonalFamily_comp_isometries line 15
def OAI.KadisonSimilarity.hilbertSumTransport line 21
theorem OAI.KadisonSimilarity.hilbertSum_transport_component line 27
def OAI.KadisonSimilarity.hilbertSumTransportWithComponents line 40

theorem OAI.KadisonSimilarity.intertwines_of_dense_summands line 48

Source documentation

Equality of bounded maps can be checked on the dense cyclic summands.

theorem intertwines_of_dense_summands
    {K : Type*} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    (V : ∀ i, E i →ₗᵢ[ℂ] H)
    (hdense : Dense (Submodule.span ℂ (⋃ i, Set.range (V i)) : Set H))
    (I : H →ₗᵢ[ℂ] K) (W : ∀ i, E i →ₗᵢ[ℂ] K)
    (hI : ∀ i x, I (V i x) = W i x)
    (Q : ∀ i, E i →L[ℂ] E i) (S : H →L[ℂ] H) (T : K →L[ℂ] K)
    (hS : ∀ i x, S (V i x) = V i (Q i x))
    (hT : ∀ i x, W i (Q i x) = T (W i x)) :
    I.toContinuousLinearMap.comp S = T.comp I.toContinuousLinearMap := by
…

theorem OAI.KadisonSimilarity.intertwines_apply_of_dense_summands line 64