OAI/Analysis/LipschitzHilbert/Fourier/SeparatedSymbolFourier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Separation of the normalized (X,Y,U) symbol by Fourier inversion. The two frequency coordinates and the selector coordinate are separated inside an absolutely convergent integral.

  1. abbrev OAI.LipschitzHilbert.PacketRepresentation.SymbolSpace line 14
  2. def OAI.LipschitzHilbert.PacketRepresentation.symbolPoint line 16
  3. def OAI.LipschitzHilbert.PacketRepresentation.frequencyCharacter line 18
  4. def OAI.LipschitzHilbert.PacketRepresentation.selectorCharacter line 21
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolPoint_inner line 24
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.norm_frequencyCharacter line 29
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.norm_selectorCharacter line 33
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.separated_symbol_integrable line 36
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.separated_symbol_fourier line 48