OAI/MeasureTheory/Falconer/Fourier/SmoothMaskDerivatives.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform derivative bounds for buffered angular masks

Selecting any subcollection of the partition preserves the same derivative scale. The bound uses local overlap; it does not grow with the number of selected caps or depend on the geometry of the good set.

  1. theorem OAI.Falconer.normalizedCap_rotated_derivative_zero line 17
  2. theorem OAI.Falconer.capCutoffAmbient_chart_derivatives line 33