OAI/MeasureTheory/Falconer/Fourier/BaseJetAmplitude.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual masked amplitude is the zero-jet root state

  1. theorem OAI.Falconer.DescriptorJetSymbol.base_ambient line 14
  2. theorem OAI.Falconer.DescriptorJetSymbol.base_pair_amplitude line 31
  3. def OAI.Falconer.descriptorRootSymbol line 44
  4. theorem OAI.Falconer.descriptorRootSymbol_pair line 48