OAI/Analysis/LipschitzHilbert/Estimates/LaminarWeakL1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The weak L1 covering estimate for a ranked laminar family. Applied below only to squares in the product of two fixed dyadic grids.

  1. theorem OAI.LipschitzHilbert.ranked_disjoint_cover line 17
  2. theorem OAI.LipschitzHilbert.ranked_finite_weak_bound line 64
  3. theorem OAI.LipschitzHilbert.ranked_countable_weak_bound line 78