OAI/Analysis/LipschitzHilbert/Fourier/UniformLineMoments.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Expose the dimension and scale-count uniformity of the already proved short energy and line moments. The constant is chosen before the finite packet spaces, as required for the final uniform operator estimate.

  1. theorem OAI.LipschitzHilbert.LinePacketFamily.uniform_short_energy line 15
  2. theorem OAI.LipschitzHilbert.LinePacketFamily.uniform_line_moment line 52