OAI/MeasureTheory/Falconer/Estimates/AnchoredBufferedMasks.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Buffered masks on the original spatial anchor cells

These masks are jointly measurable, bounded between zero and one, smooth in every adapted angular chart, and constant in the spatial variable on all descendants of a reached anchor. Their angular derivative constants are independent of the number of anchor cells.

  1. def OAI.Falconer.anchoredBufferedMask line 18
  2. theorem OAI.Falconer.anchoredBufferedMask_measurable line 23
  3. theorem OAI.Falconer.anchoredBufferedMask_bounds line 31
  4. theorem OAI.Falconer.anchoredBufferedMask_support line 39
  5. theorem OAI.Falconer.anchoredBufferedMask_core line 49
  6. theorem OAI.Falconer.anchoredBufferedMask_chart_derivatives line 60