OAI/MeasureTheory/Falconer/Estimates/DescriptorMasks.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Actual anchored masks and retained pair tests in every dimension

The angular set at an anchor is tested against the full conditional law. Masks use finite spherical nets at one eighth of the manuscript's buffer radius. Their construction is independent of the number of anchor cells.

  1. def OAI.Falconer.descriptorMaskRadius line 20
  2. theorem OAI.Falconer.descriptorMaskRadius_pos line 23
  3. def OAI.Falconer.descriptorMask line 27
  4. def OAI.Falconer.descriptorEndpointGood line 34
  5. theorem OAI.Falconer.descriptorEndpointGood_measurable line 40
  6. theorem OAI.Falconer.descriptorEndpointGood_on_cell line 58
  7. theorem OAI.Falconer.descriptorMask_measurable line 73
  8. theorem OAI.Falconer.descriptorMask_bounds line 78
  9. theorem OAI.Falconer.descriptorMask_support line 87
  10. theorem OAI.Falconer.uniform_descriptorMask_core line 98
  11. theorem OAI.Falconer.uniform_descriptorEndpointGood_buffer line 120
  12. def OAI.Falconer.descriptorPairTests line 136
  13. theorem OAI.Falconer.descriptorPairTests_measurable line 143
  14. theorem OAI.Falconer.descriptorPairTests_mono line 162