OAI/Analysis/KadisonKastler/TracialProjectionInterpolation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_tracial_projection_interpolation line 20

   Source documentation

   If the trace of p lies between that of q and q+d, cut just the orthogonal slot d. The resulting projection has exactly the trace of p and hence is unitarily conjugate to p in the original finite factor.

   theorem exists_tracial_projection_interpolation (τ : TracialRepresentation M)
       (hfactor : ∀ c : Algebra M, (∀ a : Algebra M, a * c = c * a) →
         ∃ z : ℂ, c = z • (1 : Algebra M))
       (hdiff : ∀ p : Algebra M, IsStarProjection p → p ≠ 0 →
         ∃ q : Algebra M, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
       (p q d : AlgebraProjection M) (hqd : q.val * d.val = 0)
       (hlo : (τ.trace q.val).re ≤ (τ.trace p.val).re)
       (hhi : (τ.trace p.val).re ≤ (τ.trace q.val).re + (τ.trace d.val).re) :
       ∃ (s : AlgebraProjection M) (u : unitary (Algebra M)),
         q ≤ s ∧ s ≤ (⟨q.val + d.val, q.property.add d.property hqd⟩ : AlgebraProjection M) ∧
         (u : Algebra M) * s.val * star (u : Algebra M) = p.val := by
   …

   Mentions: OAI.KadisonKastler.Algebra