ReducingRestriction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Restriction to a reducing subspace and finite coefficients

The restriction of a star algebra to a closed invariant subspace is an actual star homomorphism. Extending a corner unitary by the identity preserves the coefficients of its conjugation on that subspace.

theorem OAI.KadisonKastler.cornerCompression_coe_of_invariant line 20
theorem OAI.KadisonKastler.cornerCompression_mul_of_invariant line 27
theorem OAI.KadisonKastler.cornerCompression_star line 36

def OAI.KadisonKastler.reducingRestriction line 44

Source documentation

Restriction to a closed subspace invariant under the given star algebra.

def reducingRestriction (A : StarSubalgebra ℂ (H →L[ℂ] H))
    (hA : ∀ a : A, ∀ x ∈ K, (a : H →L[ℂ] H) x ∈ K) :
    A →⋆ₐ[ℂ] (K →L[ℂ] K) where
…

theorem OAI.KadisonKastler.reducingRestriction_coe_apply line 63
theorem OAI.KadisonKastler.star_cornerUnitary_coe line 69

theorem OAI.KadisonKastler.unitaryConj_cornerUnitary_apply line 80

Source documentation

On the reducing subspace, the extended unitary gives exactly the conjugation of the restricted operator.

theorem unitaryConj_cornerUnitary_apply (A : StarSubalgebra ℂ (H →L[ℂ] H))
    (hA : ∀ a : A, ∀ x ∈ K, (a : H →L[ℂ] H) x ∈ K)
    (v : unitary (K →L[ℂ] K)) (a : A) (x : K) :
    unitaryConj (cornerUnitary K v) a.val (x : H) =
      (unitaryConj v (reducingRestriction K A hA a) x : H) := by
…

Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.cornerUnitary, OAI.KadisonKastler.reducingRestriction

theorem OAI.KadisonKastler.inner_unitaryConj_cornerUnitary line 92

Source documentation

Coefficients on the reducing space are unchanged when its unitary is extended by the identity on the orthogonal complement.

theorem inner_unitaryConj_cornerUnitary (A : StarSubalgebra ℂ (H →L[ℂ] H))
    (hA : ∀ a : A, ∀ x ∈ K, (a : H →L[ℂ] H) x ∈ K)
    (v : unitary (K →L[ℂ] K)) (a : A) (x y : K) :
    inner ℂ (y : H) (unitaryConj (cornerUnitary K v) a.val (x : H)) =
      inner ℂ y (unitaryConj v (reducingRestriction K A hA a) x) := by
…

Mentions: OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.cornerUnitary, OAI.KadisonKastler.reducingRestriction