OAI/Analysis/KadisonKastler/RelativeTracialFixedPoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed points of relative unitary averaging in a finite algebra

The trace may be realized on a different Hilbert space. A bounded weakly compact convex family invariant under the subalgebra's unitaries has a fixed element, by the constructed compact Hilbert-center theorem.

  1. theorem OAI.KadisonKastler.mem_commutant_of_unitaryConj_fixed line 22
  2. theorem OAI.KadisonKastler.exists_relative_tracial_fixed_point line 30