OAI/MeasureTheory/Falconer/Estimates/DescriptorAmbient.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Smooth ambient extensions of the actual spatially anchored masks

At each spatial point there is at most one active anchor cell. Consequently the ambient derivative bound has no factor counting anchor cells.

  1. def OAI.Falconer.descriptorAmbientMask line 20
  2. theorem OAI.Falconer.descriptorAmbientMask_sphere line 29
  3. theorem OAI.Falconer.descriptorAmbientMask_on_cell line 34
  4. theorem OAI.Falconer.descriptorAmbientMask_off_parent line 49
  5. theorem OAI.Falconer.descriptorAmbientMask_contDiff line 58
  6. theorem OAI.Falconer.descriptorAmbientMask_measurable line 70
  7. theorem OAI.Falconer.descriptorAmbientMask_derivatives line 79
  8. theorem OAI.Falconer.descriptorAmbientMask_tsupport_good line 100