OAI/Analysis/OperatorAlgebra/ScalarLpSuperlevel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Superlevel spectral projections of cosine multipliers belong to the strong commutant of every operator commuting with the character group. The projections here are the actual indicator multipliers on scalar L².

  1. def OAI.WeakPureInfiniteness.realUpperCutoff line 15
  2. lemma OAI.WeakPureInfiniteness.realUpperCutoff_continuous line 18
  3. lemma OAI.WeakPureInfiniteness.realUpperCutoff_nonneg line 21
  4. lemma OAI.WeakPureInfiniteness.realUpperCutoff_le_one line 24
  5. lemma OAI.WeakPureInfiniteness.realUpperCutoff_eventually line 28
  6. def OAI.WeakPureInfiniteness.scalarCosineSuperlevel line 45
  7. lemma OAI.WeakPureInfiniteness.scalarCosineSuperlevel_measurable line 47
  8. def OAI.WeakPureInfiniteness.scalarCosineSuperlevelProjection line 51
  9. lemma OAI.WeakPureInfiniteness.scalarCosineSuperlevel_strong line 56
  10. lemma OAI.WeakPureInfiniteness.scalarLp_commute_cosine_superlevel line 94