OAI/Analysis/ModularTheory/TranslationCalculus.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Bounded continuous functions of regular translation belong to the actual modular core. Bounded spectral charts reduce the statement to its character generators; no spectral projection is postulated.

  1. def OAI.WeakPureInfiniteness.modularTranslationCalculus line 21

    Source documentation

    Functional calculus for regular translation, in the Fourier convention fixed by fourier_modularLpTranslate.

    def modularTranslationCalculus : BoundedContinuousFunction ℝ ℂ →⋆ₐ[ℂ]
    (Lp H 2 (volume : Measure ℝ) →L[ℂ] Lp H 2 (volume : Measure ℝ)) :=
…
  2. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_apply line 26
  3. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_character line 30
  4. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_phaseCosine_mem line 46
  5. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_chart_mem line 58
  6. lemma OAI.WeakPureInfiniteness.intervalChartFunction_norm_le line 82
  7. lemma OAI.WeakPureInfiniteness.intervalChartFunction_tendsto line 89
  8. lemma OAI.WeakPureInfiniteness.modularTranslationCalculus_chart_strong line 97
  9. theorem OAI.WeakPureInfiniteness.modularTranslationCalculus_mem line 108

    Source documentation

    Every bounded continuous regular-translation multiplier lies in the core.

    theorem modularTranslationCalculus_mem (g : BoundedContinuousFunction ℝ ℂ) :
    modularTranslationCalculus (H := H) g ∈ modularCrossedProduct (volume : Measure ℝ) S := by
…

    Mentions: OAI.WeakPureInfiniteness.modularTranslationCalculus, OAI.WeakPureInfiniteness.modularCrossedProduct