OAI/MeasureTheory/Falconer/Fourier/JetChartControl.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Rotated chart control for the actual finite products of mask jets

The total derivative order pays the amplitude cost. The number of mask occurrences enters the derivative scale, and no occurrence is discarded. All constants are selected before the scale, descriptors, and index type.

  1. theorem OAI.Falconer.descriptorJetProduct_chartControl line 19