OAI/Analysis/LipschitzHilbert/Estimates/AveragedSquareMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Even moments of the vertical Sobolev majorant. The constants are independent of the number of packet sums and of their Hilbert dimension.

  1. theorem OAI.LipschitzHilbert.average_natPow_le line 16
  2. theorem OAI.LipschitzHilbert.averaged_square_moment line 24