OAI/Analysis/LipschitzHilbert/Fourier/AnnularSquareBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The geometric annular cutoffs have a uniform finite square sum.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyLow_norm line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyOuter_norm line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifference_norm line 19
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive_norm_le line 22
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.geometric_annuli_separated line 26
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifference_square_sum line 44
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyPositive_square_sum line 88