OAI/Analysis/FiniteFactor/Diffuse/SmallPartitions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nonhyperlinear.Diffuseness.no_minimal_projection_of_small_partitions line 13

   Source documentation

   A faithful tracial concrete algebra with finite identity partitions of arbitrarily small projection trace has no minimal projection.

   theorem no_minimal_projection_of_small_partitions (M:VonNeumannAlgebra H) (v:H)
       (hcyclic:∀a b:M.toStarSubalgebra,
         inner ℂ v (((a*b:M.toStarSubalgebra):H→L[ℂ]H) v)=
         inner ℂ v (((b*a:M.toStarSubalgebra):H→L[ℂ]H) v))
       (hfaithful:∀T:M.toStarSubalgebra,(T:H→L[ℂ]H) v=0→T=0)
       (hpart:∀ε:ℝ,0<ε→∃n:ℕ,∃e:Fin n→M.toStarSubalgebra,
         (∀j,IsStarProjection (e j:H→L[ℂ]H)) ∧ (∑j,e j)=1 ∧
         ∀j,(inner ℂ v ((e j:H→L[ℂ]H) v)).re<ε)
       (p:M.toStarSubalgebra) (hps:star p=p) (hpi:p*p=p) (hp0:p≠0) :
       ∃q:M.toStarSubalgebra,star q=q ∧ q*q=q ∧ q≠0 ∧ q≠p ∧ q*p=q := by
   …