OAI/MeasureTheory/Falconer/Fourier/InverseJetState.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual inverse step on factorized descriptor symbols

An endpoint is labelled by one angular multiplier and its original finite set of descriptors. The seed retains every old jet order. A new inverse adds at most 2*j to each endpoint's descriptor budget.

  1. abbrev OAI.Falconer.DescriptorInverseLabel line 19
  2. def OAI.Falconer.descriptorInverseSeed line 21
  3. theorem OAI.Falconer.MaskJetExpansion.seed_inverse_single_order line 31
  4. theorem OAI.Falconer.MaskJetExpansion.seed_inverse_left_order line 43
  5. def OAI.Falconer.DescriptorJetSymbol.inverseLeftJets line 67
  6. theorem OAI.Falconer.DescriptorJetSymbol.inverseLeftJets_order line 75