OAI/MeasureTheory/Falconer/Fourier/SymbolOrder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Derivative order of the separated angular factors

A fixed smooth multiplier or chart substitution preserves the order charged to the original symbol. A directional derivative charges one order. Constants are uniform in the symbol and its scale, on each fixed compact angular set.

  1. structure OAI.Falconer.SymbolOrder line 23
  2. theorem OAI.Falconer.SymbolOrder.base line 32
  3. theorem OAI.Falconer.SymbolOrder.mono line 40
  4. theorem OAI.Falconer.SymbolOrder.derivative line 51
  5. theorem OAI.Falconer.SymbolOrder.mul_fixed line 67
  6. theorem OAI.Falconer.SymbolOrder.pullback line 93