OAI/Analysis/LipschitzHilbert/Fourier/VerticalSamplingDifference.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pointwise quadratic comparison of the two sampling orders.

  1. def OAI.LipschitzHilbert.PacketRepresentation.verticalSamplingDifference line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalSamplingDifference_energy_pointwise line 16