OAI/Analysis/LipschitzHilbert/Estimates/AllDyadicWeakL1.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weak L1 control at all integer scales, using the extended supremum so that the pointwise domination has no exceptional-set convention.

  1. def OAI.LipschitzHilbert.DyadicLineGrid.allDyadicSup line 13
  2. theorem OAI.LipschitzHilbert.DyadicLineGrid.allDyadicSup_measurable line 16
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.cellMean_le_allDyadicSup line 19
  4. theorem OAI.LipschitzHilbert.DyadicLineGrid.allDyadicSup_weak_L1 line 23