OAI/Analysis/OperatorAlgebra/ScalarLpIntervalCommutant.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Interval projections are strong limits of cosine superlevel projections. Thus commuting with the real character group implies commuting with the concrete exhausting spectral cutoffs used for modular weights.

  1. lemma OAI.WeakPureInfiniteness.cosineSuperlevel_eventually_interval line 15
  2. lemma OAI.WeakPureInfiniteness.scalarCosineSuperlevel_interval_strong line 44
  3. theorem OAI.WeakPureInfiniteness.scalarLp_commute_intervalProjection line 89