OAI/MeasureTheory/Falconer/Fourier/JetStateStationary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual stationary amplitudes retain every old descriptor

The far expansion uses these internal endpoint pairs before any reached mask is removed. Locality of the stationary operator preserves the old support tests, also for already differentiated masks.

  1. theorem OAI.Falconer.DescriptorJetSymbol.ambient_eventually_zero line 21
  2. def OAI.Falconer.DescriptorJetSymbol.pairAmbient line 39
  3. theorem OAI.Falconer.DescriptorJetSymbol.pairAmbient_smooth line 45
  4. theorem OAI.Falconer.DescriptorJetSymbol.pairAmbient_sphere line 53
  5. theorem OAI.Falconer.DescriptorJetSymbol.pair_stationary_support line 61