OAI/MeasureTheory/Falconer/Fourier/DescriptorDerivativeScale.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A uniform derivative scale for the actual descriptor family

The fixed derivative constants and polynomial list size are absorbed before choosing any cells, net points or descriptor family. The retained scale remembers the largest nominal descriptor length.

  1. def OAI.Falconer.descriptorDerivativeScale line 17
  2. theorem OAI.Falconer.descriptorDerivativeScale_ge_one line 20
  3. theorem OAI.Falconer.descriptorMaskRadius_inv_eq line 26
  4. theorem OAI.Falconer.descriptorMaskRadius_inv_le line 42
  5. theorem OAI.Falconer.uniform_descriptor_global_scale line 51