OAI/Analysis/LipschitzHilbert/Fourier/LocalizedSymbolOperator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The localized symbol is a weighted average of genuine planar frequency multipliers, with two powers of the weight assigned to the waves.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.planarInverse_const_mul line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.localized_symbol_operator line 21