OAI/Analysis/LipschitzHilbert/Fourier/SymbolWeights.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Integrable fixed polynomial weights for the separated symbol. The same weight is allocated to the two waves and to the selector, leaving an integrable outside coefficient. Only a fixed seminorm is used.

  1. def OAI.LipschitzHilbert.PacketRepresentation.symbolWeight line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolWeight_pos line 16
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolWeight_integrable line 19
  4. def OAI.LipschitzHilbert.PacketRepresentation.symbolCoefficientBound line 27
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolCoefficientBound_pos line 31
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.symbol_coefficient_decay line 34
  7. def OAI.LipschitzHilbert.PacketRepresentation.weightedSelector line 48
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.weightedSelector_bound line 51
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolWeight_coordinate line 61
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.weighted_symbol_identity line 73