OAI/MeasureTheory/Falconer/Estimates/DescriptorScaledKernel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual masked distance law as a cell-scaled stationary target

The unit profile is evaluated at depth divided by N in the descriptor amplitude. Both masks and the original pair law remain in this identity.

  1. def OAI.Falconer.descriptorPairAmplitude line 16
  2. theorem OAI.Falconer.descriptorPairAmplitude_measurable line 24
  3. theorem OAI.Falconer.maskedCellDistance_fourier_scaled_kernel line 34