OAI/Analysis/LipschitzHilbert/Fourier/LineDyadicReconstructionEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite dyadic square bounds control the whole Schwartz function, using the already proved strong binary resolution.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicResolutionScale_eq_scale line 16
  2. def OAI.LipschitzHilbert.PacketRepresentation.dyadicResolutionWindow line 22
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicSchwartzSum_eq_window line 25
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.line_dyadic_reconstruction_energy line 38