OAI/Analysis/KadisonKastler/CoreTraceReciprocal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A bounded reciprocal for the core trace packet

The reciprocal is cut off outside the unit frequency window. Its spectral multiplier recovers the unweighted unit packet exactly.

  1. def OAI.KadisonKastler.coreTraceReciprocal line 18
  2. theorem OAI.KadisonKastler.coreTraceReciprocal_measurable line 21
  3. theorem OAI.KadisonKastler.coreTraceReciprocal_bound line 25
  4. theorem OAI.KadisonKastler.coreTraceReciprocal_scalar line 35
  5. theorem OAI.KadisonKastler.coreTraceReciprocal_packet line 57