OAI/Analysis/LipschitzHilbert/Fourier/PositiveLineMaximal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Positive line maximal functions. Extended integrals give pointwise monotonicity, including on exceptional lines, which is needed by the finite rectangle removal algorithm.

  1. abbrev OAI.LipschitzHilbert.DyadicLineGrid.LineCellIndex line 15
  2. def OAI.LipschitzHilbert.DyadicLineGrid.positiveGridLine line 17
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.positiveGridLine_weak_L1 line 20
  4. def OAI.LipschitzHilbert.DyadicLineGrid.positiveGridHorizontal line 30
  5. theorem OAI.LipschitzHilbert.DyadicLineGrid.positiveGridHorizontal_measurable line 33
  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.positiveGridHorizontal_weak_L1 line 47
  7. def OAI.LipschitzHilbert.DyadicLineGrid.positiveHorizontal line 57
  8. theorem OAI.LipschitzHilbert.DyadicLineGrid.positiveHorizontal_measurable line 60
  9. theorem OAI.LipschitzHilbert.DyadicLineGrid.positiveHorizontal_mono line 68
  10. theorem OAI.LipschitzHilbert.DyadicLineGrid.positiveHorizontal_weak_L1 line 75