OAI/Analysis/LipschitzHilbert/Packets/AnnularLowerFrame.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The concrete annular resolution also supplies the lower square-frame bound: at each frequency only three of its summands can be nonzero.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.natural_annular_nonzero_count line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.natural_annular_square_sum line 43
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyScale_square_sum line 68
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.annular_upper_frame line 75
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.natural_annular_sum_square line 82
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblySymbol_square_le line 117
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.annularL2Sum_lower_frame_schwartz line 125
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.annularL2Sum_lower_frame line 157