OAI/Analysis/KadisonKastler/CoreFrequencyFaithfulness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Faithfulness of the bounded-frequency vector on its corner

Spectral multipliers of the regular action give localized scalar packets. The original commutant fills their vector coordinates, proving that an operator in the core which kills the trace packet vanishes on its window. No traciality or finiteness assertion is made here.

  1. theorem OAI.KadisonKastler.core_kills_unit_packet_of_kills_trace_packet line 30
  2. theorem OAI.KadisonKastler.core_kills_window_of_kills_unit_packet line 46
  3. theorem OAI.KadisonKastler.core_kills_window_of_kills_trace_packet line 115