OAI/Analysis/KadisonKastler/RegularActionSpectral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded spectral multipliers of the common regular action

These operators lie in the core commutant. They are used to recover frequency packets from the bounded-frequency trace vector.

  1. def OAI.KadisonKastler.regularActionMultiplier line 22
  2. theorem OAI.KadisonKastler.commute_regularActionMultiplier_of_fixed line 29
  3. theorem OAI.KadisonKastler.regularActionMultiplier_mem_commutant line 58