FourierTranslation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Fourier diagonalization of the regular translations in the concrete modular representation. The normalization is the Mathlib convention with the factor 2π. No spectral or trace property of the core is assumed.

lemma OAI.WeakPureInfiniteness.fourier_schwartz_translation line 19
lemma OAI.WeakPureInfiniteness.modularLpTranslate_schwartz line 42
lemma OAI.WeakPureInfiniteness.fourier_modularLpTranslate_schwartz line 52
theorem OAI.WeakPureInfiniteness.fourier_modularLpTranslate line 64
Source documentation
The actual L² Fourier unitary diagonalizes every regular translation.
```
theorem fourier_modularLpTranslate (s : ℝ) (f : Lp H 2 (volume : Measure ℝ)) :
    𝓕 (modularLpTranslate (volume : Measure ℝ) s f) =
      modularDual (volume : Measure ℝ) (-2 * Real.pi * s) (𝓕 f) := by
…
```
Mentions: OAI.WeakPureInfiniteness.modularLpTranslate, OAI.WeakPureInfiniteness.modularDual