OAI/Analysis/LipschitzHilbert/Estimates/SquareMaximalWeakL1.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A weak L1 square maximal majorant using nine fixed grid pairs.

  1. def OAI.LipschitzHilbert.DyadicLineGrid.squareSup line 11
  2. theorem OAI.LipschitzHilbert.DyadicLineGrid.squareSup_measurable line 14
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.gridSquareSup_le_squareSup line 22
  4. theorem OAI.LipschitzHilbert.DyadicLineGrid.squareSup_weak_L1 line 27
  5. def OAI.LipschitzHilbert.DyadicLineGrid.centeredSquare line 49
  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.centeredSquare_measurable line 52
  7. theorem OAI.LipschitzHilbert.DyadicLineGrid.centeredSquare_volume line 55
  8. theorem OAI.LipschitzHilbert.DyadicLineGrid.square_integral_le_squareSup line 60