OAI/MeasureTheory/Falconer/Shells/MaskedDistanceBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the original masked distance measure

Here m is the unit-interval regularized profile. Descriptor predicates receive its depth parametrization u ↦ m (u/N).

  1. theorem OAI.Falconer.descriptorPairWeight_bounds line 17
  2. theorem OAI.Falconer.maskedCellDistance_finite line 40
  3. theorem OAI.Falconer.uniform_maskedCellDistance_dominates line 61