OAI/Analysis/KadisonKastler/PreservationMatrix.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.missing_word_label_exists line 17
2. def OAI.KadisonKastler.missingWordLabel line 25
3. theorem OAI.KadisonKastler.missingWordLabel_spec line 30
4. theorem OAI.KadisonKastler.missingWordLabel_right_injective line 36
5. theorem OAI.KadisonKastler.missingWordLabel_left_injective line 58
6. def OAI.KadisonKastler.preservationProjectionMatrix line 88
7. theorem OAI.KadisonKastler.norm_preservationProjectionMatrix_le line 96

   Source documentation

   Distinct missing labels in a row and column give orthogonal ranges and domains, so the projection part has norm at most one.

   theorem norm_preservationProjectionMatrix_le (W : Finset α) {p q : ℕ}
       (hW : W.card = p + q + 1) (e : α → H →L[ℂ] H)
       (he : ∀ a, IsStarProjection (e a)) (horth : ∀ a b, a ≠ b → e a * e b = 0) :
       ‖preservationProjectionMatrix W hW e‖ ≤ 1 := by
   …

   Mentions: OAI.KadisonKastler.preservationProjectionMatrix

8. theorem OAI.KadisonKastler.rectangularOperator_norm_mul_le line 120
9. def OAI.KadisonKastler.preservationAdjacency line 128
10. def OAI.KadisonKastler.preservationSubsetMatrix line 133

    Source documentation

    Compression onto the centered GNS leg, including its scalar correction.

    def preservationSubsetMatrix (W : Finset α) {p q : ℕ}
        (hW : W.card = p + q + 1) (e : α → H →L[ℂ] H) (P : H →L[ℂ] H) (d : ℝ) :
        CStarMatrix (WordSubset W q) (WordSubset W p) (H →L[ℂ] H) :=
    …

    Mentions: OAI.KadisonKastler.WordSubset

11. theorem OAI.KadisonKastler.norm_preservationSubsetMatrix_le line 140