OAI/MeasureTheory/Falconer/Fourier/InverseJetShell.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A common recursive budget for the complete finite inverse

Both descriptor lists and original endpoint laws stay fixed. The frequency coefficient absorbs the added jet orders before the finite sum is bounded.

  1. abbrev OAI.Falconer.DescriptorInverseFamilyIndex line 17
  2. def OAI.Falconer.descriptorInverseShellCost line 22
  3. def OAI.Falconer.descriptorInverseNormalizedSum line 33
  4. theorem OAI.Falconer.descriptor_inverse_family_shell_integrable line 52
  5. theorem OAI.Falconer.descriptor_inverse_family_shell_le line 116