OAI/Analysis/LipschitzHilbert/Fourier/LineAnnularSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed annular Fourier overlap controls sums of the actual line Schwartz functions appearing in the commutator proof.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.line_annular_nonzero_count line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.line_annular_pointwise_square line 46
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.line_annular_sum_energy line 78