OAI/Analysis/LipschitzHilbert/Fourier/LocalAnnularVariation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Local annular variation from Lépingle's inequality, with the smooth/dyadic comparison supplied by packet estimates.

  1. theorem OAI.LipschitzHilbert.fullBandSum_coe line 17
  2. theorem OAI.LipschitzHilbert.partialBandSum_coe line 22
  3. theorem OAI.LipschitzHilbert.fullBandSum_memLp line 30
  4. theorem OAI.LipschitzHilbert.partialBandSum_memLp line 35
  5. theorem OAI.LipschitzHilbert.geometric_annular_variation line 46
  6. theorem OAI.LipschitzHilbert.local_annular_variation line 101