OAI/Analysis/LipschitzHilbert/Fourier/LocalizedSymbolIdentity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact separated symbol with compact annular selectors.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.localized_symbol_identity line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.localized_annular_multiplier line 22