OAI/Analysis/KadisonKastler/L2Intertwining.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Transport of regular operators through a bounded intertwiner

  1. theorem OAI.KadisonKastler.compLp_regularFieldOperator line 19
  2. theorem OAI.KadisonKastler.compLp_regularGauge line 34
  3. theorem OAI.KadisonKastler.compLp_regularIndicatorProjection line 50
  4. theorem OAI.KadisonKastler.compLp_fourierInv line 62
  5. theorem OAI.KadisonKastler.compLp_regularFrequencyProjection line 72