OAI/MeasureTheory/Falconer/Fourier/UniformJetBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A fixed derivative budget for each normalized mask jet

One constant is selected before all scales and descriptor lists. Only the sum of actual derivative orders pays an amplitude cost.

  1. theorem OAI.Falconer.normalizedAmbientDescriptorJet_uniform_budget line 16
  2. theorem OAI.Falconer.rescaledAmbientDescriptorJet_budget line 55
  3. theorem OAI.Falconer.weighted_jet_product_bound line 81
  4. theorem OAI.Falconer.normalizedAmbientJetProduct_uniform_budget line 132