OAI/MeasureTheory/Falconer/Fourier/JetAdmissible.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual differentiated descriptor products as angular symbols

Multiplication by the smooth coefficient of an inverse term preserves every descriptor support. The derivative scales add under multiplication; normalization records its exact amplitude cost.

  1. theorem OAI.Falconer.iteratedDeriv_product_bound line 17
  2. theorem OAI.Falconer.ChartSymbolControl.mul line 48
  3. theorem OAI.Falconer.descriptorJetProduct_mul_admissible line 64