OAI/Analysis/KadisonKastler/FiniteTracialAveraging.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_tracial_scalar_average line 18

   Source documentation

   Every operator in the diffuse finite factor admits scalar finite averages.

   theorem exists_tracial_scalar_average (τ : 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)
       (x : Algebra M) (ε : ℝ) (hε : 0 < ε) :
       ∃ (C : FiniteInnerAverage M) (z : ℂ),
         ‖C.apply x.val - z • (1 : H →L[ℂ] H)‖ < ε := by
   …

   Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage