OAI/MeasureTheory/Falconer/Fourier/ComplexMaskJets.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Scale-normalized jets of the complex angular multiplier

The multiplier is treated as an additional label. Its new derivative order is charged to the inverse, and its available smoothness budget is reduced by exactly that order.

  1. theorem OAI.Falconer.MaskJetIndex.value_const_mul line 17
  2. theorem OAI.Falconer.MaskJetIndex.value_real_smul line 24
  3. def OAI.Falconer.MaskJetIndex.scaledValue line 30
  4. theorem OAI.Falconer.MaskJetIndex.scaledValue_contDiff line 34
  5. theorem OAI.Falconer.MaskJetIndex.scaledValue_ofReal line 40
  6. theorem OAI.Falconer.MaskJetIndex.value_eq_inv_radius_scaled line 46
  7. theorem OAI.Falconer.MaskJetIndex.norm_iteratedFDeriv_nested line 52
  8. def OAI.Falconer.MaskJetIndex.jetEvaluation line 63
  9. theorem OAI.Falconer.MaskJetIndex.jetEvaluation_norm_le line 70
  10. theorem OAI.Falconer.MaskJetIndex.norm_iteratedFDeriv_value_le line 79
  11. theorem OAI.Falconer.MaskJetIndex.norm_iteratedFDeriv_scaledValue_le line 93
  12. theorem OAI.Falconer.MaskJetIndex.angular_budget_shift line 102