OAI/MeasureTheory/Falconer/Fourier/DescriptorJetProduct.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Indexed products of actual normalized descriptor derivatives

The index set distinguishes repeated descriptors. Its total derivative order controls the norm independently of the number of undifferentiated masks. Reached factors split off as one angular function on each cell.

  1. def OAI.Falconer.descriptorJetProduct line 16
  2. theorem OAI.Falconer.descriptorJetProduct_reached_split line 24
  3. theorem OAI.Falconer.descriptorJetProduct_support line 51
  4. theorem OAI.Falconer.normalizedDescriptorJet_order_bound line 62
  5. theorem OAI.Falconer.descriptorJetProduct_total_order_bound line 93