OAI/Analysis/LipschitzHilbert/Geometry/PositiveRectangleAuxiliary.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Pointwise monotone positive-integral auxiliary maximal functions for finite rectangle selection.

  1. theorem OAI.LipschitzHilbert.gridSquareSup_mono line 14
  2. theorem OAI.LipschitzHilbert.squareSup_mono line 18
  3. def OAI.LipschitzHilbert.positiveChartLine line 24
  4. def OAI.LipschitzHilbert.positivePlaneSquare line 27
  5. theorem OAI.LipschitzHilbert.positiveChartLine_measurable line 30
  6. theorem OAI.LipschitzHilbert.positivePlaneSquare_measurable line 34
  7. theorem OAI.LipschitzHilbert.positiveChartLine_weak_L1 line 37
  8. theorem OAI.LipschitzHilbert.positivePlaneSquare_weak_L1 line 50
  9. def OAI.LipschitzHilbert.positiveAuxiliary line 63
  10. theorem OAI.LipschitzHilbert.positiveAuxiliary_measurable line 66
  11. theorem OAI.LipschitzHilbert.positiveAuxiliary_mono line 75
  12. theorem OAI.LipschitzHilbert.positiveAuxiliary_zero line 84
  13. theorem OAI.LipschitzHilbert.positiveAuxiliary_weak_L1 line 89