OAI/Analysis/KadisonKastler/TracialDixmierConclusion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.FiniteInnerAverage.trace_algebraApply line 18
2. theorem OAI.KadisonKastler.FiniteInnerAverage.trace_error_le line 35
3. theorem OAI.KadisonKastler.trace_scalar_mem_norm_orbitHull line 48

   Source documentation

   The scalar of the norm-closed orbit hull is exactly the represented trace.

   theorem trace_scalar_mem_norm_orbitHull (τ : 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) :
       τ.trace x • (1 : H →L[ℂ] H) ∈ closure (convexHull ℝ (innerUnitaryOrbit M x.val)) := by
   …

   Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.innerUnitaryOrbit

4. theorem OAI.KadisonKastler.publishedDixmierOfTracialFactor line 70

   Source documentation

   Finite inner averages of a represented diffuse finite factor approximate scalars, using its faithful tracial vector.

   theorem publishedDixmierOfTracialFactor (τ : 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) :
       PublishedDixmierAveraging M := by
   …

   Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.PublishedDixmierAveraging