OAI/Analysis/LipschitzHilbert/Estimates/HardyPairL4.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An elementary fourth-power bound for the difference of positive and negative frequency Schwartz functions. The proof uses only Plancherel, frequency support of products, and a scalar quadratic inequality.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProduct_positive line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProduct_negative line 24
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartz_disjoint_energy_add_sub line 35
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.hardyPair_fourth_power line 48