OAI/Analysis/LipschitzHilbert/Fourier/PlaneLineWeakL1.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Weak L1 bounds for actual line averages on the plane, by Fubini.

  1. def OAI.LipschitzHilbert.DyadicLineGrid.horizontalSup line 12
  2. theorem OAI.LipschitzHilbert.DyadicLineGrid.horizontalSup_measurable line 15
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.horizontalSup_weak_L1 line 27
  4. def OAI.LipschitzHilbert.DyadicLineGrid.verticalSup line 46
  5. theorem OAI.LipschitzHilbert.DyadicLineGrid.verticalSup_measurable line 49
  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.verticalSup_weak_L1 line 53