OAI/Analysis/LipschitzHilbert/Fourier/LineSchwartzPairing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Self-adjoint low-pass projections and the product pairing used in the actual smooth Carleson synthesis estimate.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProjection_inner line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyLow_conj line 32
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.lineLowpass_absorb line 35
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProduct_inner_bound line 46