OAI/Analysis/LipschitzHilbert/Estimates/DyadicWeakL1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Weak L1 bounds for actual finite dyadic line averages. The constants are independent of the root, depth, and cell length. These supply the one-dimensional part of the auxiliary covering maximal operator.

  1. theorem OAI.LipschitzHilbert.DyadicLineGrid.lineAverage_maximal_weak_L1 line 13
  2. theorem OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal_root_weak_L1 line 27
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal_weak_L1 line 40