OAI/Analysis/LipschitzHilbert/Fourier/SignedAnnularSymbol.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

All signed finite annular multipliers have the same Mihlin bounds. The proof uses only the fixed support annulus and its finite overlap.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.iteratedDeriv_tsupport_subset line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifference_tsupport line 22
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifference_derivative_support line 31
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.natural_closed_annulus_count line 36
  5. def OAI.LipschitzHilbert.PacketRepresentation.signedAnnularSymbol line 68
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.signedAnnularSymbol_derivative line 75
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.signedAnnularSymbol_mihlin line 105
  8. def OAI.LipschitzHilbert.PacketRepresentation.signedAnnularMihlinConstant line 163
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.signedAnnularMihlinConstant_nonneg line 167
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.signedAnnularSymbol_mihlin_four line 170
  11. theorem OAI.LipschitzHilbert.PacketRepresentation.signedAnnularSymbol_norm line 179