OAI/MeasureTheory/Falconer/Fourier/JetStateAmbient.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Ambient representatives of the exact recursive symbols

The bound is uniform in the descriptor list and scale. It retains the ambient representative needed for the full-sphere far expansion.

  1. theorem OAI.Falconer.iteratedFDeriv_mul_bound line 18
  2. def OAI.Falconer.DescriptorJetSymbol.ambient line 53
  3. theorem OAI.Falconer.DescriptorJetSymbol.ambient_sphere line 61
  4. theorem OAI.Falconer.DescriptorJetSymbol.ambient_smooth line 70
  5. theorem OAI.Falconer.exists_descriptorJetSymbol_ambient_budget line 82