OAI/Analysis/KadisonKastler/CentralProjectionComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_partialIsometry_separated_remainders line 18

   Source documentation

   A maximal partial isometry leaves no algebraic link between its two remainder projections. This statement does not require scalar center.

   theorem exists_partialIsometry_separated_remainders (p q : AlgebraProjection M) :
       ∃ (v : PartialIsometry M) (hp : v.support ≤ p) (hq : v.target ≤ q),
         ∀ a : Algebra M,
           (AlgebraProjection.remainder v.target q hq).val * a *
             (AlgebraProjection.remainder v.support p hp).val = 0 := by
   …

   Mentions: OAI.KadisonKastler.Algebra

2. theorem OAI.KadisonKastler.exists_centrally_separated_comparison line 56

   Source documentation

   One central projection separates the two unmatched remainders.

   theorem exists_centrally_separated_comparison (p q : AlgebraProjection M) :
       ∃ (v : PartialIsometry M) (hp : v.support ≤ p) (hq : v.target ≤ q)
         (z : AlgebraProjection M),
         (∀ a : Algebra M, a * z.val = z.val * a) ∧
         AlgebraProjection.remainder v.support p hp ≤ z ∧
         AlgebraProjection.remainder v.target q hq ≤
           (⟨1 - z.val, z.property.one_sub⟩ : AlgebraProjection M) := by
   …

   Mentions: OAI.KadisonKastler.Algebra