OAI/Analysis/LipschitzHilbert/Fourier/VerticalBinEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cardinality-independent square-function energy for the finite vertical bins.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.binSquareStep_nonneg line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.binSquareStep_le_one line 14
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinProfile_sum_norm_sq_le line 17
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinWindow_sum_norm_sq_le line 25
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.planar_integral_norm_sq_fourier line 35
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBin_schwartz_energy_le line 44