OAI/Analysis/KadisonKastler/FourierTranslation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Fourier transformation of the actual regular translations

The identity is first proved on Schwartz vectors and extended by their norm density. Its normalization is explicit: translating by s becomes multiplication by exp(2*pi*i*s*ΞΎ).

  1. def OAI.KadisonKastler.translatedSchwartz line 21
  2. theorem OAI.KadisonKastler.translatedSchwartz_toLp line 26
  3. theorem OAI.KadisonKastler.fourier_translate_function line 36
  4. theorem OAI.KadisonKastler.fourier_translate_schwartz line 46

    Distinct definitions of this name: OAI/Analysis/KadisonKastler/RegularFourierTransport.lean:71 (same statement text; different proof or body). Qualify references as OAI.KadisonKastler.fourier_translate_schwartz@path.

  5. theorem OAI.KadisonKastler.fourier_regularTranslateApply line 62

    Source documentation

    Plancherel's transform intertwines the two concrete unitary actions.

    Distinct definitions of this name: OAI/Analysis/KadisonKastler/RegularFourierTransport.lean:94 (same statement text; different proof or body). Qualify references as OAI.KadisonKastler.fourier_regularTranslateApply@path.

    theorem fourier_regularTranslateApply (s : ℝ) (f : RegularCoreHilbert H) :
    (𝓕 (regularTranslateApply s f) : RegularCoreHilbert H) =
      (regularCharacterUnitary (H := H) (2 * Real.pi * s) :
…

    Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularTranslateApply, OAI.KadisonKastler.regularCharacterUnitary