OAI/MeasureTheory/Falconer/Estimates/AnchoredMasks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Angular masks attached to actual dyadic anchor cells

The spatial dependence is a finite Borel choice of the anchor cell. On every descendant of an anchor cell, its angular mask is exactly constant in the spatial variable.

  1. def OAI.Falconer.anchoredMask line 19
  2. theorem OAI.Falconer.anchoredMask_measurable line 23
  3. theorem OAI.Falconer.anchoredMask_on_cell line 31
  4. theorem OAI.Falconer.anchoredMask_off_parent line 44
  5. theorem OAI.Falconer.anchoredMask_bounds line 52
  6. theorem OAI.Falconer.anchoredMask_reached line 64
  7. theorem OAI.Falconer.anchoredMask_chart_smooth line 72
  8. theorem OAI.Falconer.anchoredMask_chart_derivatives line 93