OAI/Analysis/LipschitzHilbert/Trees/SourceMaximalBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform boundedness of the actual maximal representatives on a bounded source, including on their null-set representatives.

  1. theorem OAI.LipschitzHilbert.monotoneMaximal_le_of_bound line 13
  2. theorem OAI.LipschitzHilbert.DyadicLineGrid.cellMean_bound line 28
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal_bound line 38
  4. theorem OAI.LipschitzHilbert.DyadicLineGrid.allDyadicMaximal_bound line 46
  5. theorem OAI.LipschitzHilbert.DyadicLineGrid.threeGridMaximal_bound line 53
  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.allHorizontalMaximal_bound line 59
  7. theorem OAI.LipschitzHilbert.DyadicLineGrid.allVerticalMaximal_bound line 63