OAI/MeasureTheory/Falconer/Fourier/SymbolProduct.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite derivative budgets for products of angular masks

Products of scalar angular masks are considered in arbitrary one-coordinate charts and for arbitrary finite indexed descriptor lists, including repeated descriptors.

  1. theorem OAI.Falconer.product_derivatives_at line 17
  2. theorem OAI.Falconer.iteratedDeriv_add_order line 60
  3. theorem OAI.Falconer.iteratedDeriv_contDiff line 66
  4. def OAI.Falconer.normalizedChartFactor line 72
  5. theorem OAI.Falconer.normalizedChartFactor_contDiff line 75
  6. theorem OAI.Falconer.normalizedChartFactor_derivative_bound line 79
  7. theorem OAI.Falconer.normalized_chart_product_bound line 96