OAI/Analysis/LipschitzHilbert/Fourier/AnnularResolutionSymbols.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The concrete symmetric finite annular partition converges to one away from the zero vertical frequency.

  1. def OAI.LipschitzHilbert.PacketRepresentation.reassemblyScale line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyScale_pos line 15
  3. def OAI.LipschitzHilbert.PacketRepresentation.reassemblySymbol line 19
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyScale_last line 22
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblySymbol_eq line 32
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblySymbol_norm line 50
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyLow_small_tendsto line 54
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyLow_large_eventually line 62
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblySymbol_tendsto line 74