OAI/Analysis/KadisonKastler/FourierModulation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Fourier transforms of scalar character multipliers

The identity is established on Schwartz functions by the integral formula, then on the actual LĀ² space by density.

  1. theorem OAI.KadisonKastler.character_eq_fourierChar line 22
  2. theorem OAI.KadisonKastler.character_temperate line 26
  3. def OAI.KadisonKastler.modulatedSchwartz line 32
  4. theorem OAI.KadisonKastler.modulatedSchwartz_apply line 36
  5. theorem OAI.KadisonKastler.modulatedSchwartz_toLp line 40
  6. theorem OAI.KadisonKastler.fourier_modulate_function line 50
  7. theorem OAI.KadisonKastler.fourier_modulate_schwartz line 64
  8. theorem OAI.KadisonKastler.fourier_regularCharacterUnitary line 85

    Source documentation

    Multiplication by the scalar character translates Fourier frequency.

    theorem fourier_regularCharacterUnitary (s : ā„) (f : RegularCoreHilbert H) :
    (š“• ((regularCharacterUnitary (H := H) (2 * Real.pi * s) :
ā€¦

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