OAI/Analysis/OperatorAlgebra/ScalarLpLocalizedFunctions.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A bounded spectral chart on each interval [-n,n]. This gives the localized continuous multipliers needed to test the modular weight, using only commutation with the actual character group.

  1. def OAI.WeakPureInfiniteness.scalarPhaseCosine line 17
  2. lemma OAI.WeakPureInfiniteness.scalarPhaseCosine_apply line 23
  3. lemma OAI.WeakPureInfiniteness.scalarPhaseCosine_selfAdjoint line 26
  4. lemma OAI.WeakPureInfiniteness.scalarPhaseCosine_character line 32
  5. lemma OAI.WeakPureInfiniteness.scalarLp_commute_phaseCosine line 48
  6. lemma OAI.WeakPureInfiniteness.scalarPhaseCosine_cfc_apply line 62
  7. lemma OAI.WeakPureInfiniteness.scalarLp_commute_phaseCosine_cfc line 72
  8. def OAI.WeakPureInfiniteness.intervalChartRate line 88
  9. lemma OAI.WeakPureInfiniteness.intervalChartRate_pos line 90
  10. lemma OAI.WeakPureInfiniteness.intervalChart_inverse line 94
  11. def OAI.WeakPureInfiniteness.intervalChartFunction line 108
  12. lemma OAI.WeakPureInfiniteness.intervalChartFunction_apply line 113
  13. lemma OAI.WeakPureInfiniteness.scalarLp_commute_intervalChart line 120
  14. lemma OAI.WeakPureInfiniteness.intervalChartFunction_localized line 130
  15. theorem OAI.WeakPureInfiniteness.scalarLp_commute_continuousMultiplier line 156

    Source documentation

    Every continuous scalar multiplier commutes with the Fourier compression of a core element. The proof uses bounded spectral charts and interval exhaustion, so it imposes no global uniform approximation premise.

    theorem scalarLp_commute_continuousMultiplier
    (T : Lp ℂ 2 (volume : Measure ℝ) →L[ℂ] Lp ℂ 2 (volume : Measure ℝ))
    (hc : ∀ s, Commute T
      (modularDualUnitary (H := ℂ) volume s : Lp ℂ 2 volume →L[ℂ] Lp ℂ 2 volume))
…

    Mentions: OAI.WeakPureInfiniteness.modularDualUnitary