OAI/Analysis/KadisonKastler/CoreTraceSymmetry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The weakly closed vector symmetry used for the core trace

Its scalar formulation is linear in the operator and passes to weak operator limits. An involutive antiunitary then turns it into the exact tracial norm identity needed by the finite-window criterion.

  1. def OAI.KadisonKastler.coreTraceSymmetrySpace line 21
  2. theorem OAI.KadisonKastler.coreTraceSymmetry_norm line 32
  3. theorem OAI.KadisonKastler.coreTraceSymmetry_of_weak_limit line 49